An Interactive Prover for Protocol Verification in the Computational Model

Baelde, David and Delaune, Stephanie and Jacomme, Charlie and Koutsos, Adrien and Moreau, Solene
(2021) An Interactive Prover for Protocol Verification in the Computational Model.
In: 42nd IEEE Symposium on Security and Privacy (S&P'21), May 24-28, Virtual.
Conference: SP IEEE Symposium on Security and Privacy

This is the latest version of this item.

[img] Text
longversion.pdf

Download (1MB)
Official URL: https://hal.archives-ouvertes.fr/hal-03172119

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).

Available Versions of this Item

  • An Interactive Prover for Protocol Verification in the Computational Model. (deposited 10 May 2021 21:09) [Currently Displayed]

Actions

Actions (login required)

View Item View Item