Download PDFOpen PDF in browser

Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols Using the Squirrel Proof Assistant

EasyChair Preprint 8631

21 pagesDate: August 10, 2022

Abstract

Bana and Comon have proposed a logical approach to proving protocols in the computational model, which they call the Computationally Complete Symbolic Attacker (CCSA). The proof assistant Squirrel implements a verification technique that elaborates on this approach, building on a meta-logic over the CCSA base logic. In this paper, we show that this meta-logic can naturally be extended to handle protocols with mutable states (key updates, counters, \etc.) and we extend Squirrel's proof system to be able to express the complex proof arguments that are sometimes required for these protocols. Our theoretical contributions have been implemented in Squirrel and validated on a number of case studies, including a proof of the YubiKey and YubiHSM protocols.

Keyphrases: computational security, formal methods, interactive theorem proving, logic, security protocols

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@booklet{EasyChair:8631,
  author    = {David Baelde and Stephanie Delaune and Adrien Koutsos and Solène Moreau},
  title     = {Cracking the Stateful Nut -- Computational Proofs of Stateful Security Protocols Using the Squirrel Proof Assistant},
  howpublished = {EasyChair Preprint 8631},
  year      = {EasyChair, 2022}}
Download PDFOpen PDF in browser