| Title | An Interactive Prover for Protocol Verification in the Computational Model |
| Publication Type | Conference Paper |
| Year of Publication | 2021 |
| Authors | Baelde, David, Delaune, Stéphanie, Jacomme, Charlie, Koutsos, Adrien, Moreau, Solène |
| Conference Name | 2021 IEEE Symposium on Security and Privacy (SP) |
| Keywords | Cognition, Collaboration, composability, compositionality, Computational modeling, computational security, formal methods, Interactive Prover, observational equivalence, policy-based collaboration, privacy, protocol verification, Protocols, pubcrawl, security protocols, Semantics, Solids, Tools |
| 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 lacks support for proof mechanization.In this paper, we present a framework and an interactive prover allowing to mechanize proofs of security protocols 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). |
| DOI | 10.1109/SP40001.2021.00078 |
| Citation Key | baelde_interactive_2021 |
An Interactive Prover for Protocol Verification in the Computational Model