A logic and mechanization support for proving the post-quantum security of protocols

Cas Cremers (1) , Caroline Fontaine (2) , Charlie Jacomme (1, 3)

1 CISPA - Helmholtz Center for Information Security [Saarbrücken]
2 LMF - Laboratoire Méthodes Formelles
3 PESTO - Proof techniques for security protocols

We provide the first mechanized post-quantum sound security protocol proofs. We achieve this by developing PQ-BC, a computational first-order logic that is sound with respect to quantum attackers, and corresponding mechanization support in the form of the PQ-Squirrel prover. Our work builds on the classical BC logic[BCL14] and its mechanization in the Squirrel [BDJ + 21] prover. Our development of PQ-BC requires making the BC logic sound for a single interactive quantum attacker. We implement the PQ-Squirrel prover by modifying Squirrel, relying on the soundness results of PQ-BC and enforcing a set of syntactic conditions; additionally, we provide new tactics for the logic that extend the tool's scope. Using PQ-Squirrel, we perform several case studies, thereby giving the first mechanical proofs of their computational post-quantum security. These include two generic constructions of KEM based key exchange, two sub-protocols from IKEv1 and IKEv2, and a proposed postquantum variant of Signal's X3DH protocol. Additionally, we use PQ-Squirrel to prove that several classical Squirrel case studies are already post-quantum sound.

Domaines: Cryptographie et sécurité [cs.CR]

Cas Cremers, Caroline Fontaine, Charlie Jacomme. A logic and mechanization support for proving the post-quantum security of protocols. S&P 2022, May 2022, San Francisco / Virtual, United States. ⟨hal-03620358v1⟩