A research team from ETH Zurich’s Department of Computer Science (D-INFK) has received a Test-of-Time Award for work that has shaped the automated analysis of cryptographic protocols for more than a decade.
Image: D-INFK, ETH Zürich
Professor David Basin of ETH Zurich’s Department of Computer Science, Professor Cas Cremers, Dr Benedikt Schmidt and Dr Simon Meier have been honoured with a Test-of-Time Award at the 39th IEEE Computer Security Foundations Symposium (CSF’26). The award recognises their 2012 paper, “Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties”, and its lasting impact on the formal verification of cryptographic protocols. The Test-of-Time Award honours research papers that have demonstrated outstanding and enduring significance to their field. This year, the committee selected the paper as one of only two papers from the 659 papers published at CSF and its predecessor, CSFW, through 2026.
Automated analysis of cryptographic protocols
The award-winning paper introduced a general symbolic framework for the automated analysis of cryptographic protocols, with a particular focus on protocols that use modular exponentiation, such as Diffie-Hellman-based protocols. The researchers developed a formal modelling approach based on rewriting and expressed security properties using first-order formulas. A novel constraint-solving algorithm enables the automated analysis of protocols and can either establish that a protocol satisfies its specified security properties or identify a concrete witness demonstrating that a property can be violated – effectively providing an attack on the protocol. Technically, the approach combines ideas from equational unification and symbolic reasoning with techniques from strand spaces and proof normal forms. The researchers implemented the approach and demonstrated its effectiveness on challenging case studies, including the automated verification of the NAXOS protocol under a symbolic version of the eCK security model.
A lasting impact on the field
Since its publication, the work has influenced a range of subsequent developments in formal methods for security, particularly in the design of automated tools for the verification of cryptographic protocols. The techniques introduced in the paper have become an important reference point for automated reasoning about protocol security. The award also highlights the broader and lasting impact of research carried out by the D-INFK community in the field of formal security verification.
Congratulations on this outstanding accomplishment!
Read more here.