A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols - Laboratoire Méthodes Formelles Accéder directement au contenu
Communication Dans Un Congrès Année : 2022

A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols

Résumé

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 [7] and its mechanization in the Squirrel [5] 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 post-quantum variant of Signal’s X3DH protocol. Additionally, we use PQ-Squirrel to prove that several classical Squirrel case studies are already post-quantum sound.
Fichier principal
Vignette du fichier
pqbc-eprint.pdf (1.19 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03620358 , version 1 (25-03-2022)
hal-03620358 , version 2 (28-03-2022)
hal-03620358 , version 3 (07-04-2022)

Identifiants

  • HAL Id : hal-03620358 , version 3

Citer

Cas Cremers, Caroline Fontaine, Charlie Jacomme. A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols. S&P 2022 - 43rd IEEE Symposium on Security and Privacy, May 2022, San Francisco / Virtual, United States. ⟨hal-03620358v3⟩
353 Consultations
272 Téléchargements

Partager

Gmail Facebook X LinkedIn More