HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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

https://hal.archives-ouvertes.fr/hal-03172119
Contributor : Solène Moreau Connect in order to contact the contributor
Submitted on : Wednesday, March 17, 2021 - 2:49:47 PM
Last modification on : Monday, April 4, 2022 - 9:28:32 AM
Long-term archiving on: : Monday, June 21, 2021 - 8:55:39 AM

File

longversion.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03172119, version 1

Citation

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⟩

Share

Metrics

Record views

913

Files downloads

504