Cas Cremers
Introduction
Prof. Dr. Cas Cremers
Prof. Dr. Cas Cremers is faculty member at the CISPA Helmholtz Center for Information Security 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, and became full Professor at the University of Oxford in 2015. In 2018 he joined CISPA in Germany.
His work includes co-developing the Scyther tool and the Tamarin prover for the analysis of security protocols, and working on provable foundations for secure messaging, including the first proofs of the Signal protocol. He contributed to the development of IETF's TLS 1.3 and MLS, and was a member of the DP3T team whose privacy-preserving protocols laid the foundation for the GAEN framework used in Covid proximity-tracing apps.
Areas of interest
- security protocols
- formal methods
- applied cryptography
- analysis tools
- automated verification
- protocols and standards
Open positions new
We have open phd and postdoc positions.
Research
My research involves the application of formal methods and cryptography to the analysis and development of secure systems. The resulting contributions include:
- 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.
-
Operational
Semantics and Verification of Security Protocols
-
Supportive technologies
We develop automated tools for analyzing 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 TAMARIN prover for the symbolic analysis of
security protocols
- 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.
- The Scyther Tool: Verification,
Falsification, and Analysis of
Security Protocols
- Scyther-proof
- Efficient
Construction of Machine-Checked Symbolic Protocol
Security Proofs
Journal of Computer Security, 2013.
- Efficient
Construction of Machine-Checked Symbolic Protocol
Security Proofs
A feature comparison of our tools is also available.
- The Tamarin prover
-
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.
- Automated
Analysis and Verification of TLS 1.3:
0-RTT, Resumption and Delayed Authentication
A complete list of publications, recent manuscripts, and bibtex files can be found here.