Skip to Main content Skip to Navigation
Conference papers

An Interactive Prover for Protocol Verification in the Computational Model

Abstract : Given the central importance of designing secure protocols, providing solid mathematical foundations and computer-assisted methods to attest for their correctness is becoming crucial. Here, we elaborate on the formal approach introduced by Bana and Comon in [10], [11], which was originally designed to analyze protocols for a fixed number of sessions and which more importantly lacks support for proof mechanization. In this paper, we present a framework and an interactive prover allowing to mechanize proofs of security protocol for an arbitrary number of sessions in the computational model. More specifically, we develop a meta-logic as well as a proof system for deriving security properties. Proofs in our system only deal with high-level, symbolic representations of protocol executions, similar to proofs in the symbolic model, but providing security guarantees at the computational level. We have implemented our approach within a new interactive prover, the SQUIRREL prover, taking as input protocols specified in the applied pi-calculus, and we have performed a number of case studies covering a variety of primitives (hashes, encryption, signatures, Diffie-Hellman exponentiation) and security properties (authentication, strong secrecy, unlinkability).
Document type :
Conference papers
Complete list of metadata
Contributor : Solène Moreau <>
Submitted on : Wednesday, March 17, 2021 - 2:49:47 PM
Last modification on : Friday, April 16, 2021 - 1:42:17 PM


Files produced by the author(s)


  • HAL Id : hal-03172119, version 1


David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, Solène Moreau. An Interactive Prover for Protocol Verification in the Computational Model. SP 2021 - 42nd IEEE Symposium on Security and Privacy, May 2021, San Fransisco / Virtual, United States. ⟨hal-03172119⟩



Record views


Files downloads