Ensuring Privacy in Cryptographic Protocols: Formal Verification Techniques 🔐

Ioana Boureanu, “Formal Verification of Privacy in Cryptographic Protocols: Theory and Practice, Part 1”, VeTSS Summer School 2024 Talk by Ioana Boureanu, University of Surrey, at the VeTSS Summer School 2024. In this tutorial we will try to understand why it is hard to formally verify privacy-like properties, such as strong secrecy, anonymity, unlinkability or lack of information flow, in well-established models for formal analysis of cryptographic protocols. We will then see how to do some approximations of this verification in state-of-the-art tools for what is called Dolev-Yao protocol analysis, such as Tamarin and a new tool called Phoebe. Finally, if time allows, we will touch upon on what privacy analysis may mean in the “sister formalisms” for proving cryptographic protocols secure or private, that is in computational models and accompanying tools such as Squirrel. To follow the examples, you may need to have the following installed in your machine: Haskell (https://www.haskell.org/) Tamarin prover (https://tamarin-prover.com/), the newest version is fine. Squirrel prover (https://squirrel-prover.github.io/)