Paper 2022/401

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

Cas Cremers, Caroline Fontaine, and Charlie Jacomme

Abstract

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 [Bana,Comon,CCS14] and its mechanization in the Squirrel prover [BDJKM,S&P21]. 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. We provide the sources of PQ-Squirrel and all our models for reproducibility, as well as a long version of this paper with full details.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. Major revision. S&P 2022
Keywords
Security ProtocolsPost QuantumFormal MethodsObservational EquivalenceComputational SecurityInteractive Prover.
Contact author(s)
charlie jacomme @ cispa de
History
2022-03-28: received
Short URL
https://ia.cr/2022/401
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2022/401,
      author = {Cas Cremers and Caroline Fontaine and Charlie Jacomme},
      title = {A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols},
      howpublished = {Cryptology ePrint Archive, Paper 2022/401},
      year = {2022},
      note = {\url{https://eprint.iacr.org/2022/401}},
      url = {https://eprint.iacr.org/2022/401}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.