Stéphanie Delaune: Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the SQUIRREL Proof Assistant

Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the SQUIRREL Proof Assistant

David Baelde, Stéphanie Delaune, Adrien Koutsos, and Solène Moreau. Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the SQUIRREL Proof Assistant. In Proceedings of the 35th IEEE Computer Security Foundations Symposium (CSF'22), pp. 289–304, IEEE Computer Society Press, Haifa, Israel, August 2022.

Download

[PDF]

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.

BibTeX

@inproceedings{BDKM-csf22,
  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.
},
  address =       {Haifa, Israel},
  author =        {Baelde, David and  Delaune, St{\'e}phanie and Koutsos, Adrien and Moreau, Sol{\`e}ne},
  booktitle =     {{P}roceedings of the 35th {IEEE} {C}omputer
                   {S}ecurity {F}oundations {S}ymposium ({CSF}'22)},
  month =         aug,
  pages =         {289--304},
  publisher =     {{IEEE} Computer Society Press},
  title =         {Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the SQUIRREL Proof Assistant},
  year =          {2022},
  acronym =       {{CSF}'22},
  nmonth =        {8},
  lsv-category =  {intc},
  wwwpublic =     {public and ccsb},
}