CISPA
Browse
cispa_all_3416.pdf (1.05 MB)

An Interactive Prover for Protocol Verification in the Computational Model

Download (1.05 MB)
Version 2 2023-12-11, 20:13
Version 1 2023-11-29, 18:16
conference contribution
posted on 2023-12-11, 20:13 authored by David Baelde, Stephanie Delaune, Charlie Jacomme, Adrien Koutsos, Solene Moreau
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).

History

Preferred Citation

David Baelde, Stephanie Delaune, Charlie Jacomme, Adrien Koutsos and Solene Moreau. An Interactive Prover for Protocol Verification in the Computational Model. In: IEEE Symposium on Security and Privacy (S&P). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

IEEE Symposium on Security and Privacy (S&P)

Legacy Posted Date

2021-05-10

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3416, title = "An Interactive Prover for Protocol Verification in the Computational Model", author = "Baelde, David and Delaune, Stephanie and Jacomme, Charlie and Koutsos, Adrien and Moreau, Solene", booktitle="{IEEE Symposium on Security and Privacy (S&P)}", year="2021", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC