(Main topics can be selected in the top bar, further subtopics can appear in an additional menu bar.)
- May 2013 After a fantastic time at ETH, I will be joining the Computer Science department at Oxford University on October 1st, 2013.
- Dec 2012 New versions of Scyther have been released. Please consult the changelog and the updated manual (included in the distribution) for details, such as the use of macros.
- Nov 2012 We now provide a high-level comparison of our tools and a selection of protocols analysed using them.
- Nov 2012 Our book on Operational Semantics and Verification of Security Protocols is out now.
A complete list of publications, recent manuscripts, and bibtex files can be found here.
Symbolic Protocol Analysis
Operational Semantics and Verification of Security Protocols
Operational Semantics and Verification of Security Protocols
Security protocols are widely used to ensure secure communications over insecure networks, such as the internet or airwaves. These protocols use strong cryptography to prevent intruders from reading or modifying the messages. However, using cryptography is not enough to ensure their correctness. Combined with their typical small size, which suggests that one could easily assess their correctness, this often results in incorrectly designed protocols.
The authors present a methodology for formally describing security protocols and their environment. This methodology includes a model for describing protocols, their execution model, and the intruder model. The models are extended with a number of well-defined security properties, which capture the notions of correct protocols, and secrecy of data. The methodology can be used to prove that protocols satisfy these properties. Based on the model they have developed a tool set called Scyther that can automatically find attacks on security protocols or prove their correctness. In case studies they show the application of the methodology as well as the effectiveness of the analysis tool.
The methodology's strong mathematical basis, the strong separation of concerns in the model, and the accompanying tool set make it ideally suited both for researchers and graduate students of information security or formal methods and for advanced professionals designing critical security protocols.
With S. Mauw. Information Security and Cryptography series, Springer, 2012.
- Modeling and Analyzing Security in the Presence of
Modeling and Analyzing Security in the Presence of Compromising Adversaries
We present a framework for modeling adversaries in security protocol analysis, ranging from a Dolev-Yao style adversary to more powerful adversaries who can reveal different parts of principals' states during protocol execution. Our adversary models unify and generalize many existing security notions from both the computational and symbolic settings.
We extend an existing symbolic protocol-verification tool with our adversary models, resulting in the first tool that systematically supports notions such as weak perfect forward secrecy, key compromise impersonation, and adversaries capable of state-reveal queries. In case studies, we automatically find new attacks and rediscover known attacks that previously required detailed manual analysis.
With D. Basin. ESORICS 2012. See also the accompanying CSL 2010 paper that introduces protocol security hierarchies.
- A framework for compositional verification of security
A framework for compositional verification of security protocols
Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach. We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verification of large structured security protocols. Our approach is to verify properties of component protocols in a multi-protocol environment, then deduce properties about the composed protocol. To reduce the complexity of multi-protocol verification, we introduce a notion of protocol independence and prove a number of theorems that enable analysis of independent component protocols in isolation. To illustrate the applicability of our framework to real-world protocols, we study a key establishment sequence in WiMAX consisting of three subprotocols. Except for a small amount of trivial reasoning, the analysis is done using automatic tools.
With S. Andova, K. Gjosteen, S. Mauw, S. Mjolsnes, and S. Radomirovic. Information and Computation, 2008.
- Automated Analysis of Diffie-Hellman
Protocols and Advanced Security Properties
Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
We present a general approach for the symbolic analysis of security protocols that use Diffie-Hellman exponentiation to achieve advanced security properties. We model protocols as multiset rewriting systems and security properties as first-order formulas. We analyze them using a novel constraint-solving algorithm that supports both falsification and verification, even in the presence of an unbounded number of protocol sessions. The algorithm exploits the finite variant property and builds on ideas from strand spaces and proof normal forms. We demonstrate the scope and the effectiveness of our algorithm on non-trivial case studies. For example, the algorithm successfully verifies the NAXOS protocol with respect to a symbolic version of the eCK security model.
With B. Schmidt, S. Meier, and D. Basin. CSF 2012.
Construction of Machine-Checked Symbolic Protocol
Efficient Construction of Machine-Checked Symbolic Protocol Security Proofs
We embed an untyped security protocol model in the interactive theorem prover Isabelle/HOL and derive a theory for constructing proofs of secrecy and authentication properties. Our theory is based on two key ingredients. The first is a protocol-independent invariant that allows us to reason about the possible origin of messages. The second is a class of protocol-specific invariants that formalize type assertions about variables in protocol specifications. The resulting theory is well-suited for interactively constructing human-readable, protocol security proofs. We additionally give an algorithm that automatically generates Isabelle/HOL proof scripts based on this theory. In a number of case studies, we show that both interactive and automatic proof construction are efficient. The resulting proofs, constructed interactively or automatically, provide strong correctness guarantees since all proofs, including those deriving our theory from the security protocol model, are machine-checked.
With D. Basin and S. Meier. Journal of Computer Security, 2012.
- Unbounded Verification, Falsification, and Characterization
of Security Protocols by Pattern Refinement
Unbounded Verification, Falsification, and Characterization of Security Protocols by Pattern Refinement
We present a new verification algorithm for security protocols that allows for unbounded verification, falsification, and complete characterization. The algorithm provides a number of novel features, including: (1) Guaranteed termination, after which the result is either unbounded correctness, falsification, or bounded correctness. (2) Efficient generation of a finite representation of an infinite set of traces in terms of patterns, also known as a complete characterization. (3) State-of-the-art performance, which has made new types of protocol analysis feasible, such as multi-protocol analysis.
Standardization and Case Studies
- Provably Repairing the ISO/IEC 9798
Standard for Entity Authentication
Provably Repairing the ISO/IEC 9798 Standard for Entity Authentication
The ISO/IEC 9798 standard defines a family of entity authentication protocols. We formally analyze these protocols and find numerous weaknesses, including some that violate even the most basic authentication guarantees. We show how these weaknesses can be uniformly remedied by following prudent design principles and we repair the protocols using these principles. We provide automated, machine-checked proofs of the correctness of the resulting protocols by extending a state-of-the-art method for generating machine-checked protocol proofs. Our analysis and recommendations have been acknowledged by the responsible ISO working group and an update to the standard has been released.
With D. Basin and S. Meier. Journal of Computer Security, To appear.
- Key Exchange in IPsec revisited: Formal
Analysis of IKEv1 and IKEv2
Key Exchange in IPsec revisited: Formal Analysis of IKEv1 and IKEv2
The IPsec standard aims to provide application-transparent end-to-end security for the Internet Protocol. The security properties of IPsec critically depend on the underlying key exchange protocols, known as IKE (Internet Key Exchange).
We provide the most extensive formal analysis so far of the current IKE versions, IKEv1 and IKEv2. We combine recently introduced formal analysis methods for security protocols with massive parallelization, allowing the scope of our analysis to go far beyond previous formal analysis. While we do not find any significant weaknesses on the secrecy of the session keys established by IKE, we find several previously unreported weaknesses on the authentication properties of IKE.
- Distance Hijacking Attacks on Distance
Distance Hijacking Attacks on Distance Bounding Protocols
After several years of theoretical research on distance bounding protocols, the first implementations of such protocols have recently started to appear. These protocols are typically analyzed with respect to three types of attacks: Distance Fraud, Mafia Fraud, and Terrorist Fraud.
We define and analyze a fourth main type of attack on distance bounding protocols, called Distance Hijacking. This type of attack poses a serious threat in many practical scenarios. We show that many proposed distance bounding protocols are vulnerable to Distance Hijacking, and we propose solutions to make these protocols resilient to this type of attack.
We show that verifying distance bounding protocols using existing informal and formal frameworks does not guarantee the absence of Distance Hijacking attacks. We extend a formal framework for reasoning about distance bounding protocols to include overshadowing attacks. We use the resulting framework to prove the absence of all of the found attacks for protocols to which our countermeasures have been applied.
With S. Capkun, K.B. Rasmussen, and Benedikt Schmidt. IEEE Symposium on Security and Privacy 2012.
- Keeping Data Secret under Full Compromise using Porter
Keeping Data Secret under Full Compromise using Porter Devices
We address the problem of confidentiality in scenarios where the attacker is not only able to observe the communication between principals, but can also fully compromise the communicating parties (their devices, not only their long term secrets) after the confidential data has been exchanged. We formalize this problem and explore solutions that provide confidentiality after the full compromise of devices and user passwords. We propose two new solutions that use explicit key deletion and forward-secret protocols combined with key storage on porter devices. Our solutions provide the users with full control over their privacy. We analyze the proposed solutions using an automatic verification tool. We also implement a prototype using a mobile phone as porter device to illustrate how the solution can be realized on modern platforms.
With C. Pöpper, S. Capkun, and D. Basin. ACSAC 2012.
- Beyond eCK: Perfect Forward Secrecy under Actor Compromise and Ephemeral-Key Reveal
Beyond eCK: Perfect Forward Secrecy under Actor Compromise and Ephemeral-Key Reveal
In this paper we show that it is possible to achieve perfect forward secrecy in two-message key exchange (KE) protocols that satisfy even stronger security properties than provided by the extended Canetti-Krawczyk (eCK) security model. In particular, we consider perfect forward secrecy in the presence of adversaries that can reveal the long-term secret keys of the actor of a session and reveal ephemeral secret keys.
We propose two new security models for KE protocols. First, we formalize a slightly stronger variant of the eCK security model that we call eCKw. Second, we integrate perfect forward secrecy into eCKw, which gives rise to the even stronger eCK-PFS model.
We propose a security-strengthening transformation (i.e., a compiler) between our new models. Given a two-message Diffie-Hellman type protocol secure in eCKw, our transformation yields a two-message protocol that is secure in eCK-PFS. As an example, we show how our transformation can be applied to the NAXOS protocol.
With M. Feltz. ESORICS 2012.
- Examining Indistinguishability-Based Security Models
for Key Exchange Protocols: The case of CK, CK-HMQV, and eCK
Examining Indistinguishability-Based Security Models for Key Exchange Protocols: The case of CK, CK-HMQV, and eCK
Many recent key exchange (KE) protocols have been proven secure in the CK, CK-HMQV, or eCK security models. The exact relation between these security models, and hence the relation between the security guarantees provided by the protocols, is unclear. We show first that the CK, CK-HMQV, and eCK security models are formally incomparable. Second, we show that these models are also practically incomparable, by providing for each model attacks on protocols from the literature that are not considered by the other models. Third, our analysis enables us to find previously unreported flaws in protocol security proofs from the literature. We identify the causes of these flaws and show how they can be avoided.
- Session-state Reveal is stronger than eCK's Ephemeral Key
Reveal: Using automatic analysis to attack the NAXOS
Session-state Reveal is stronger than eCK's Ephemeral Key Reveal: Using automatic analysis to attack the NAXOS protocol
In the paper Stronger Security of Authenticated Key Exchange, a new security model for authenticated key exchange protocols (eCK) is proposed. The new model is suggested to be at least as strong as previous models for key exchange protocols, such as the CK model. The model includes a new notion of an ephemeral-key reveal adversary query, which is claimed to be at least as strong as the session-state reveal query.
We investigate the relation between the two models by focusing on the difference in adversary queries. We formally model the NAXOS protocol and a variant of the eCK model, called eCK', in which the ephemeral-key reveal query is replaced by the session-state reveal query. Using Scyther, a formal protocol analysis tool, we automatically find attacks on the protocol, showing that the protocol is insecure in the eCK' model.
Our attacks prove that the session-state reveal query is stronger than the ephemeral-key reveal query and that the eCK security model is incomparable to the CK model, disproving several claims made in the literature.
International Journal of Applied Cryptography, 2010.
For a high-level comparison, read the tool overview table.
To see some of the protocols we have analysed using these tools, please check the protocol models.