Presenters and Affiliations

Prashant Agrawal — Max Planck Institute for Security and Privacy, Bochum, Germany

Overview / Abstract

Cryptographers prove security through games and reductions to hardness assumptions, while symbolic-verification researchers model cryptography through equations and automated deduction. These communities offer different guarantees, and tools that mechanise game-based proofs introduce their own trade-offs in automation and generality. This half-day tutorial teaches these approaches and how they connect: a hand-built game-based proof, automated symbolic protocol analysis with ProVerif, mechanised game-based proofs, and recent work repurposing symbolic attack-finders to synthesise computationally valid reductions.

Target Audience

• Graduate students, advanced undergraduates, and early-career researchers in security, cryptography, or formal methods seeking an entry into computer-aided cryptography.
• Cryptographers curious about symbolic tools and formal-methods researchers curious about cryptographic proofs.
• Practitioners designing or reviewing authentication, payment, or messaging protocols who want machine-checked assurance beyond manual review.

Prerequisites

Participants should know introductory security-course cryptography: symmetric and public-key encryption, digital signatures, and hash functions. No background in formal methods or logic, and no prior experience with the tools, is assumed. No advance reading is required.

Learning Outcomes

• Read and write a game-based security definition and explain a reduction.
• Model a simple protocol in ProVerif, state secrecy and authentication queries, and interpret attack derivations.
• Place ProVerif, Tamarin, CryptoVerif, EasyCrypt, and Squirrel on the automation-versus-generality spectrum and choose a tool for a problem.
• Explain what a symbolic guarantee does and does not mean computationally.
• Describe the research frontier in automated synthesis of cryptographic proofs and identify entry points in the literature.

Tutorial Structure / Technical Details

Half-day tutorial organized as two 90-minute sessions. Each session mixes lecture segments with live tool demonstrations, using related examples across the segments. Participants may follow along on a laptop; setup instructions will be circulated before the tutorial. A laptop is optional, and the material also works as a demonstration.

Session 1: Games, Reductions and Symbolic Analysis (90 minutes)

Session 2: Mechanised Proofs and Reduction Synthesis (90 minutes)

Tools and scope

• Symbolic protocol tools discussed: ProVerif and Tamarin.
• Mechanised game-based proof tools discussed: EasyCrypt, Squirrel, and CryptoVerif.
• The tutorial distinguishes what symbolic guarantees mean from computational security guarantees.

Materials / Demonstration

Slides and all example models will be published in a public repository before the conference and remain available afterwards. Participants with laptops can follow the demonstrations; setup instructions will be circulated before the tutorial.

Biography

Not provided in the source proposal.

References

1. D. Baelde, S. Delaune, J. Jacomme, A. Koutsos, and S. Moreau. “An interactive prover for protocol verification in the computational model.” IEEE Symposium on Security and Privacy (S&P), pp. 537–554, 2021.
2. D. Baelde, A. Koutsos, and J. Sauvage. “Foundations for cryptographic reductions in CCSA logics.” ACM Conference on Computer and Communications Security (CCS), pp. 2814–2828, 2024.
3. M. Barbosa et al. “SoK: Computer-aided cryptography.” IEEE Symposium on Security and Privacy (S&P), pp. 777–795, 2021.
4. G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin. “Computer-aided security proofs for the working cryptographer.” Advances in Cryptology—CRYPTO, LNCS 6841, pp. 71–90, 2011.
5. D. Basin et al. “A formal analysis of 5G authentication.” ACM CCS, pp. 1383–1396, 2018.
6. D. Basin, R. Sasse, and J. Toro-Pozo. “The EMV standard: Break, fix, verify.” IEEE S&P, pp. 1766–1781, 2021.
7. K. Bhargavan, B. Blanchet, and N. Kobeissi. “Verified models and reference implementations for the TLS 1.3 standard candidate.” IEEE S&P, pp. 483–502, 2017.
8. B. Blanchet. “An efficient cryptographic protocol verifier based on Prolog rules.” IEEE Computer Security Foundations Workshop, pp. 82–96, 2001.
9. B. Blanchet. “A computationally sound mechanized prover for security protocols.” IEEE S&P, pp. 140–154, 2006.
10. B. Blanchet, B. Smyth, C. Cheval, and M. Sylvestre. ProVerif 2.05: Automatic cryptographic protocol verifier, user manual and tutorial, 2023. https://bblanche.gitlabpages.inria.fr/proverif/manual.pdf
11. D. Boneh and V. Shoup. A Graduate Course in Applied Cryptography, 2023. https://toc.cryptobook.us/
12. C. Cremers, M. Horvat, S. Scott, and T. van der Merwe. “Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication.” IEEE S&P, pp. 470–485, 2016.
13. D. Dolev and A. C. Yao. “On the security of public key protocols.” IEEE Transactions on Information Theory 29(2), 198–208, 1983.
14. S. Meier, B. Schmidt, C. Cremers, and D. A. Basin. “The TAMARIN prover for the symbolic analysis of security protocols.” Computer Aided Verification, LNCS 8044, pp. 696–701, 2013.
15. V. Shoup. “Sequences of games: A tool for taming complexity in security proofs.” Cryptology ePrint Archive, Paper 2004/332, 2004. https://eprint.iacr.org/2004/332