Benedikt Schmidt


I'm working on production security at Google since January 2017. This is my (now outdated) academic homepage from when I was at IMDEA.

I’m a researcher at the IMDEA Software Institute, Madrid. I received a Computer Science degree from University of Karlsruhe (Germany) and a Ph.D. degree in Computer Science from ETH Zurich (Switzerland), under the supervision of David Basin.

Research Interests


Journal Publications

  1. Formal Reasoning about Physical Properties of Security Protocols. David Basin, Srdjan Capkun, Patrick Schaller, and Benedikt Schmidt. ACM Transactions on Information and System Security (TISSEC), 14(2), 16. (PDF, official PDF, Isabelle Formalization)

Conference Publications

  1. Key Confirmation in Key Exchange: A Formal Treatment and Implications for TLS 1.3. Marc Fischlin, Felix Günther, Benedikt Schmidt, and Bogdan Warinschi. S&P 2016.(PDF)
  2. Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model. Miguel Ambrona, Gilles Barthe, Benedikt Schmidt. EuroCrypt 2016.(eprint)
  3. Automated Proofs of Pairing-Based Cryptography. Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt. CCS 2015. (PDF,Tool)
  4. Mind the Gap: Modular Machine-checked Proofs of One-Round Key Exchange Protocols. Gilles Barthe and Juan Manuel Crespo and Yassine Lakhnech and Benedikt Schmidt. EuroCrypt 2015. (eprint)
  5. Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds. Gilles Barthe and Edvard Fagerholm and Dario Fiore and Andre Scedrov and Benedikt Schmidt and Mehdi Tibouchi. PKC 2015. (eprint)
  6. Automated Analysis of Cryptographic Assumptions in Generic Group Models. Gilles Barthe, Dario Fiore, Edvard Fagerholm, John Mitchell, Andre Scedrov, Benedikt Schmidt. Crypto 2014. (eprint)
  7. Certified synthesis of efficient batch verifiers. J. A. Akinyele, G. Barthe, B. Grégoire, B. Schmidt, P. Strub. CSF 2014. (PDF)
  8. Automated Verification of Group Key Agreement Protocols. Benedikt Schmidt, Ralf Sasse, Cas Cremers, David Basin. S&P 2014. (PDF)
  9. Fully automated analysis of padding-based encryption in the computational model. G. Barthe, J. Crespo, B. Grégoire, C. Kunz, Y. Lakhnech, B. Schmidt, S. Zanella-Béguelin. CCS 2013. (PDF)
  10. The TAMARIN Prover for the Symbolic Analysis of Security Protocols (Tool Paper). Simon Meier, Benedikt Schmidt, Cas Cremers, David Basin. Computer Aided Verification 2013.(PDF,Tool)
  11. Automated analysis of Diffie-Hellman protocols and advanced security properties. Benedikt Schmidt, Simon Meier, Cas Cremers, and David Basin. Proceedings of the 25rd IEEE Computer Security Foundations Symposium, CSF, 25–27.(PDF, official PDF, Tool)
  12. Distance hijacking attacks on distance bounding protocols. Cas Cremers, Kasper Bonne Rasmussen, Benedikt Schmidt, Srdjan Capkun. Security and Privacy (SP), 2012 IEEE Symposium on, 113–127.(PDF, official PDF, Isabelle Formalization)
  13. Impossibility Results for Secret Establishment. Benedikt Schmidt, Patrick Schaller, David Basin. Computer Security Foundations Symposium (CSF), 2010 23rd IEEE, 261–273. (PDF, official PDF)
  14. Modeling and verifying physical properties of security protocols for wireless networks. Patrick Schaller, Benedikt Schmidt, David Basin, Srdjan Capkun. Computer Security Foundations Symposium, 2009. CSF’09. 22nd IEEE, 109–123. (PDF, official PDF, Isabelle Formalization)

Invited Publications and Book Chapters

  1. Computer-Aided Proofs in Cryptography: An Overview. Gilles Barthe, François Dupressoir, Benjamin Grégoire, Benedikt Schmidt, and Pierre-Yves Strub. All about Proofs, Proofs for All. Vol 55. Mathematical Logic and Foundations, 2015.
  2. EasyCrypt: A Tutorial. Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, and Pierre-Yves Strub. Foundations of Security Analysis and Design VII. Vol. 8604, 2013.
  3. Let’s get physical: Models and methods for real-world security protocols David Basin, Srdjan Capkun, Patrick Schaller, Benedikt Schmidt. Theorem Proving in Higher Order Logics, 2009. Pages 1–22 (invited paper). (PDF, official PDF, Isabelle Formalization)


  1. Formal Analysis of Key Exchange Protocols and Physical Protocols. Ph.D. Thesis, ETH Zurich, December 2012.
  2. A Cryptographically Sound Proof of an Electronic Payment System in Isabelle/HOL. Master Thesis (Diplomarbeit), Universität Karlsruhe.