David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, and Solène Moreau. An Interactive Prover for Protocol Verification in the Computational Model. In Proceedings of the 42nd IEEE Symposium on Security and Privacy (S&P'21), IEEE Computer Society Press, San Francisco, California, USA, May 2021.
Given the central importance of designing secureprotocols, providing solid mathematical foundations andcomputer-assisted methods to attest for their correctnessis becoming crucial.Here, we elaborate on the formal approach introduced by Bana andComon, which wasoriginally designedto analyze protocols for a fixed number of sessions,and lacks support forproof mechanization.In this paper, we present a framework and an interactive proverallowing to mechanizeproofs 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 systemfor deriving security properties. Proofs in our system only dealwith high-level, symbolic representations of protocol executions,similar to proofs in the symbolic model, but providing security guaranteesat 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 ofprimitives (hashes, encryption, signatures, Diffie-Hellmanexponentiation) and security properties (authentication, strongsecrecy, unlinkability).
@inproceedings{BDJKS-sp21,
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, 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).
},
address = {San Francisco, California, USA},
author = {Baelde, David and
Delaune, St{\'e}phanie and Jacomme, Charlie and Koutsos, Adrien and Moreau, Sol{\`e}ne},
booktitle = {{P}roceedings of the 42nd {IEEE} {S}ymposium on
{S}ecurity and {P}rivacy ({S\&P}'21)},
editor = {Oprea, Alina and Holz, Thorsten},
month = may,
OPTnote = {To appear},
publisher = {IEEE Computer Society Press},
title = {An Interactive Prover for Protocol Verification in the Computational Model},
year = {2021},
acronym = {{S\&P}'21},
nmonth = {5},
lsv-category = {intc},
OPTlsv-status = {apar},
wwwpublic = {public},
}