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]
Preview
 Text
longversion.pdf
Download (1MB) | Preview
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).

Item Type: Conference or Workshop Item (A Paper) (Paper)
Additional Information: To appear
Divisions: Cas Cremers (CC)
Conference: SP IEEE Symposium on Security and Privacy
Depositing User: Jacqueline Brendel
Date Deposited: 10 May 2021 21:09
Last Modified: 10 May 2021 21:09
Primary Research Area: NRA2: Reliable Security Guarantees
URI: https://publications.cispa.saarland/id/eprint/3416

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
CISPA is powered by EPrints 3 which is developed by the School of Electronics and Computer Science at the University of Southampton. More information and software credits.