Cas Cremers

Introduction

Research

My research involves the application of formal methods and cryptography to the analysis and development of secure systems. The resulting contributions include:

1. Formal foundations of security

   How to mathematically define secure systems and their properties, and how to reason about them. For example:

   • Operational Semantics and Verification of Security Protocols
     Information Security and Cryptography series, Springer, 2012.
   • Know your Enemy: Compromising Adversaries in Protocol Analysis
     ACM Transactions on Information and System Security (TISSEC), 2014.
   • Post-Compromise Security
     IEEE Computer Security Foundations Symposium (CSF), 2016.
2. Supportive technologies

   We develop automated tools for analysing security protocols:

   • The Tamarin prover
     • The TAMARIN prover for the symbolic analysis of security protocols
       International Conference on Computer Aided Verification (CAV) 2013.
     • Automated verification of group key agreement protocols
       IEEE Symposium on Security and Privacy (Oakland) 2014.
     • Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
       IEEE Computer Security Foundations Symposium (CSF) 2012.
   • The Scyther tool
     • The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols
       International Conference on Computer Aided Verification (CAV) 2008.
     • Unbounded Verification, Falsification, and Characterization of Security Protocols by Pattern Refinement
       ACM conference on Computer and communications security (CCS) 2008.
   • Scyther-proof
     • Efficient Construction of Machine-Checked Symbolic Protocol Security Proofs
       Journal of Computer Security, 2013.

   A feature comparison of our tools is also available.

3. Application example: Improving security standards

   We have used our analysis methods and tools in many real-world case studies, yielding direct impact. For example:

   • Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication
     IEEE Symposium on Security and Privacy (Oakland), 2016.
   • A Formal Security Analysis of the Signal Messaging Protocol
     Journal of Cryptology, 2020 (first report in 2016).
   • Provably Repairing the ISO/IEC 9798 Standard for Entity Authentication
     Journal of Computer Security, 2013.

A complete list of publications, recent manuscripts, and bibtex files can be found here.

Short bio

Prof. Dr. Cas Cremers is a tenured faculty at the CISPA Helmholtz Center for Information Security and Honorary Professor at Saarland University, in Saarbruecken, Germany.

He obtained his PhD in 2006 from Eindhoven University of Technology in the Netherlands. From 2006 to 2013 he was a postdoctoral researcher, and senior researcher and lecturer, at ETH Zurich in Switzerland. In 2013 he moved to the University of Oxford as an Associate Professor. In 2015 he became Professor of Information security at the University of Oxford. In 2018 he joined the CISPA Helmholtz Center for Information Security in Germany.