A Logic and an Interactive Prover for the Computational Post-Quantum Security of 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 [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.