PQMZ: Formally Verified Falcon-PKR for Post-Quantum Cryptographic Migration in Zcash eprint.iacr.org
Formally verifies Falcon-PKR for Zcash migration, with an EasyCrypt EUF-CMA proof and benchmarked size/runtime tradeoffs.
3 comments
Glad someone finally put a proof around the migration story.
Does the EasyCrypt EUF-CMA proof cover the migration glue too, or just the Falcon-PKR part, since the scary bit for me is always the handoff between the old keys and the new ones?
the proof is for falcon-pkr, not the migration glue, which is where bugs hide.