Manuscripts

  1. On the Limits of Authenticated Key Exchange Security with an Application to Bad Randomness

    On the Limits of Authenticated Key Exchange Security with an Application to Bad Randomness

    State-of-the-art authenticated key exchange (AKE) protocols are proven secure in game-based security models. These models have considerably evolved in strength from the original Bellare-Rogaway model. However, so far only informal impossibility results, which suggest that no protocol can be secure against stronger adversaries, have been sketched. At the same time, there are many diffㄦent security models being used, all of which aim to model the strongest possible adversary. In this paper we provide the first systematic analysis of the limits of game-based security models. Our analysis reveals that diffㄦent security goals can be achieved in diffㄦent relevant classes of AKE protocols. From our formal impossibility results, we derive strong security models for these protocol classes and give protocols that are secure in them. In particular, we analyse the security of AKE protocols in the presence of adversaries who can perform attacks based on chosen randomness, in which the adversary controls the randomness used in protocol sessions. Protocols that do not modify memory shared among sessions, which we call stateless protocols, are insecure against chosen-randomness attacks. We propose novel stateful protocols that provide resilience even against this worst case randomness failure, thereby weakening the security assumptions required on the random number generator.


    With M. Feltz.
    [ePrint]

Books

  1. 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.
  2. Book chapter: Model Checking Security Protocols
    With D. Basin and C. Meadows.
    To appear in: Handbook of Model Checking, Springer.
    [preprint] [bibtex]

Peer-reviewed papers

  1. Know Your Enemy: Compromising Adversaries in Protocol Analysis

    Know Your Enemy: Compromising Adversaries in Protocol Analysis

    We present a symbolic framework, based on a modular operational semantics, for formalizing different notions of compromise relevant for the design and analysis of cryptographic protocols. The framework’s rules can be combined to specify different adversary capabilities, capturing different practically-relevant notions of key and state compromise. The resulting adversary models generalize the models currently used in different domains, such as security models for authenticated key exchange. We extend an existing security-protocol analysis tool, Scyther, with our adversary models. This extension systematically supports notions such as weak perfect forward secrecy, key compromise impersonation, and adversaries capable of state-reveal queries. Furthermore, we introduce the concept of a protocol-security hierarchy, which classifies the relative strength of protocols against different adversaries.

    In case studies, we use Scyther to analyse protocols and automatically construct protocol-security hierarchies in the context of our adversary models. Our analysis confirms known results and uncovers new attacks. Additionally, our hierarchies refine and correct relationships between protocols previously reported in the cryptographic literature.


    With D. Basin.
    ACM Transactions on Information and System Security, 2014.
    [preprint] [bibtex]
  2. ARPKI: Attack Resilient Public-Key Infrastructure

    ARPKI: Attack Resilient Public-Key Infrastructure

    We present ARPKI, a public-key infrastructure that ensures that certificate-related operations, such as certificate issuance, update, revocation, and validation, are transparent and accountable. ARPKI is the first such infrastructure that systematically takes into account requirements identified by previous research. Moreover, ARPKI is co-designed with a formal model, and we verify its core security property using the Tamarin prover. We present a proof-of-concept implementation providing all features required for deployment. ARPKI efficiently handles the certification process with low overhead and without incurring additional latency to TLS.

    ARPKI offers extremely strong security guarantees, where compromising n-1 trusted signing and verifying entities is insufficient to launch an impersonation attack. Moreover, it deters misbehavior as all its operations are publicly visible.


    With D. Basin, T.H-J. Kim, A. Perrig, R. Sasse, and P. Szalachowski.
    CCS 2014: Proceedings of the 21st ACM Conference on Computer and Communications Security, Scottsdale, Arizona, USA, 2014.
    [preprint] [bibtex]
  3. Improving the ISO/IEC 11770 standard for key management techniques

    Improving the ISO/IEC 11770 standard for key management techniques

    We provide the first systematic analysis of the ISO/IEC 11770 standard for key management techniques, which describes a set of key exchange, key authentication, and key transport protocols. We analyse the claimed security properties, as well as additional modern requirements on key management protocols, for 30 protocols and their variants. Our formal, tool-supported analysis of the protocols uncovers several incorrect claims in the standard. We provide concrete suggestions for improving the standard.


    With M. Horvat.
    SSR 2014: Security Standardisation Research, 2014.
    [PDF]
    To appear.
  4. Actor Key Compromise: Consequences and Countermeasures

    Actor Key Compromise: Consequences and Countermeasures

    Despite Alice's best efforts, her long-term secret keys may be revealed to an adversary. Possible reasons include weakly generated keys, compromised key storage, subpoena, and coercion. However, Alice may still be able to communicate securely with other parties, depending on the protocol used. We call the associated property resilience against Actor Key Compromise (AKC). We formalise this property in a symbolic model and identify conditions under which it can and cannot be achieved. In case studies that include TLS and SSH, we find that many protocols are not resilient against AKC. We implement a concrete AKC attack on the mutually authenticated TLS protocol.


    With D. Basin and M. Horvat.
    CSF 2014, Proc. of the 27th IEEE Computer Security Foundations Symposium, 2014.
    [preprint] [bibtex]
  5. Improving the Security of Cryptographic Protocol Standards
    With D. Basin, K. Miyazaki, S. Radomirovic, and D. Watanabe.
    IEEE Security & Privacy.
    [preprint]
    Online pre-print has been published: final editing and paper edition to appear.
  6. Automated verification of group key agreement protocols

    Automated verification of group key agreement protocols

    We advance the state-of-the-art in automated symbolic cryptographic protocol analysis by providing the first algorithm that can handle Diffie-Hellman exponentiation, bilinear pairing, and AC-operators. Our support for AC-operators enables protocol specifications to use multisets, natural numbers, and finite maps. We implement the algorithm in the TAMARIN prover and provide the first symbolic correctness proofs for group key agreement protocols that use Diffie-Hellman or bilinear pairing, loops, and recursion, while at the same time supporting advanced security properties, such as perfect forward secrecy or eCK-security. We automatically verify a set of protocols, including the STR, group Joux, and GDH protocols, thereby demonstrating the effectiveness of our approach.


    With B. Schmidt, R. Sasse, and D. Basin.
    IEEE Symposium on Security and Privacy (Oakland), San Jose, CA, May 2014.
    [preprint] [bibtex]
  7. Beyond eCK: Perfect Forward Secrecy under Actor Compromise and Ephemeral-Key Reveal

    Beyond eCK: Perfect Forward Secrecy under Actor Compromise and Ephemeral-Key Reveal

    We show that it is possible to achieve perfect forward secrecy in two-message or one-round key exchange (KE) protocols even in the presence of very strong active adversaries that can reveal random values of sessions and compromise long-term secret keys of parties.

    We provide two new game-based security models for KE protocols with increasing security guarantees, namely, eCK-w and eCK-PFS. The eCK-w model is a slightly stronger variant of the extended Canetti- Krawczyk (eCK) security model. The eCK-PFS model captures perfect forward secrecy in the presence of eCK-w adversaries. We propose a security-strengthening transformation (i.e., a compiler) from eCK-w to eCK-PFS that can be applied to protocols that only achieve security in a weaker model than eCK-w, which we call eCK-passive. We show that, given a two-message Diffie-Hellman type protocol secure in eCK-passive, our transformation yields a two-message protocol that is secure in eCK-PFS.

    We demonstrate how our transformation can be applied to concrete KE protocols. In particular, our methodology allows us to prove the security of the first known one-round protocol that achieves perfect forward secrecy under actor compromise and ephemeral-key reveal.


    With M. Feltz.
    Designs, Codes, and Cryptography, 2013.
    [preprint] [pdf] [bibtex]
  8. ASICS: Authenticated Key Exchange Security Incorporating Certification Systems

    ASICS: Authenticated Key Exchange Security Incorporating Certification Systems

    Most security models for authenticated key exchange (AKE) do not explicitly model the associated certification system, which includes the certification authority (CA) and its behaviour. However, there are several well-known and realistic attacks on AKE protocols which exploit various forms of malicious key registration and which therefore lie outside the scope of these models.

    We provide the first systematic analysis of AKE security incorporating certification systems (ASICS). We define a family of security models that, in addition to allowing different sets of standard AKE adversary queries, also permit the adversary to register arbitrary bitstrings as keys. For this model family we prove generic results that enable the design and verification of protocols that achieve security even if some keys have been produced maliciously. Our approach is applicable to a wide range of models and protocols; as a concrete illustration of its power, we apply it to the CMQV protocol in the natural strengthening of the eCK model to the ASICS setting.


    With C. Boyd, M. Feltz, K.G. Paterson, B. Poettering, and D. Stebila.
    ESORICS 2013, Proc. of the 18th European Symposium on Research in Computer Security, RHUL, Eggham, UK.
    [preprint] [pdf] [bibtex]
  9. The TAMARIN Prover for the Symbolic Analysis of Security Protocols

    The TAMARIN Prover for the Symbolic Analysis of Security Protocols

    We present the TAMARIN prover for the symbolic analysis of security protocols. TAMARIN generalizes the backwards search used by the Scyther tool to enable protocol specification using multiset rewriting rules, property specification in a guarded fragment of first-order logic that allows quantification over messages and timepoints, and reasoning modulo equational theories. These features enable use of the tool to model protocols with mutable global state and complex control flow such as loops, and to specify complex security properties such as the eCK model. Additionally, they enable reasoning with respect to equational theories such as Diffie-Hellman and user-specified subterm-convergent theories. Similar to the Scyther tool, TAMARIN can analyze protocols with respect to an unbounded number of instances and fresh values.

    TAMARIN provides an efficient, fully automatic mode to falsify or verify security protocols. Additionally, it provides a graphical, interactive mode, which enables users to explore proof states, inspect attack graphs, and combine manual proof guidance with automatic proof search.


    With S. Meier, B. Schmidt, and D. Basin.
    CAV 2013, Proc. of the 25th International Conference on Computer Aided Verification, Saint Petersburg, 2013.
    [preprint] [pdf] [bibtex]
    Download: Tamarin Prover
  10. Provably Repairing the ISO/IEC 9798 Standard for Entity Authentication

    Provably Repairing the ISO/IEC 9798 Standard for Entity Authentication

    We formally analyze the family of entity authentication protocols defined by the ISO/IEC 9798 standard and find numerous weaknesses, both old and new, including some that violate even the most basic authentication guarantees. We analyze the cause of these weaknesses, propose repaired versions of the protocols, and provide automated, machine-checked proofs of the correctness of the resulting protocols. From an engineering perspective, we propose two design principles for security protocols that suffice to prevent all the weaknesses. Moreover, we show how modern verification tools can be used for falsification and certified verification of security standards. Based on our findings, the ISO working group responsible for the ISO/IEC 9798 standard has released an updated version of the standard.


    With D. Basin and S. Meier.
    Journal of Computer Security, 2013.
    [preprint] [pdf] [bibtex]
  11. Efficient Construction of Machine-Checked Symbolic Protocol Security Proofs

    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, 2013.
    [preprint] [pdf] [bibtex]
  12. 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, 17th European Symposium on Research in Computer Security, Pisa, September 2012.
    [pdf] [bibtex] [Extended version]
  13. 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, Proc. of the 25th IEEE Computer Security Foundations Symposium, Harvard, 2012.
    [pdf] [bibtex] [Extended version]
    Tool support: Tamarin Prover
  14. Distance Hijacking Attacks on Distance Bounding Protocols

    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 B. Schmidt.
    IEEE Symposium on Security and Privacy (Oakland), San Francisco, May 2012.
    [pdf] [bibtex] [Extended version]
  15. Distance Hijacking Attacks on Distance Bounding Protocols (Abstract)

    Distance Hijacking Attacks on Distance Bounding Protocols (Abstract)

    Distance bounding protocols are typically analyzed with respect to three types of attacks: Distance Fraud, Mafia Fraud, and Terrorist Fraud. We define a fourth main type of attacks on distance bounding protocols, called Distance Hijacking attacks. We show that many proposed distance bounding protocols are vulnerable to these attacks, and we propose solutions to make these protocols resilient to Distance Hijacking. Additionally, we generalize Distance Hijacking to Location Hijacking, to which location verification protocols may be vulnerable.


    With S. Capkun and K.B. Rasmussen
    Chair's invited session, NDSS 2012, San Diego, February 2012.
    One-page abstract.
    [pdf]
  16. 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 will be released.


    With D. Basin and S. Meier.
    POST 2012 (Part of ETAPS), Tallin, Estonia, April 2012.
    [pdf] [bibtex]
  17. 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.


    ESORICS 2011, 16th European Symposium on Research in Computer Security, Leuven, September 2011.
    [pdf] [bibtex]
  18. 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.


    ASIACCS 2011, Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security, Hong Kong, China.
    [pdf] [bibtex]
  19. Session-state Reveal is stronger than eCK's Ephemeral Key Reveal: Using automatic analysis to attack the NAXOS protocol

    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 (IJACT), 2010.
    [preprint] [pdf] [bibtex]
  20. Keeping Data Secret under Full Compromise using Porter Devices

    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 2010, 26th Annual Computer Security Applications Conference, 2010, Austin, Texas.
    [pdf] [bibtex]
  21. Modeling and Analyzing Security in the Presence of Compromising Adversaries

    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 2010, 15th European Symposium on Research in Computer Security, 2010, Athens, Greece.
    [pdf] [bibtex]
  22. Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries

    Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries

    (This paper builds on the adversary models presented in the ESORICS 2010 paper.)

    We introduce the concept of a protocol-security hierarchy, which classifies the relative strength of protocols against different forms of compromise. In case studies, we use Scyther to automatically construct protocol-security hierarchies that refine and correct relationships between protocols previously reported in the cryptographic literature.


    With D. Basin
    CSL 2010, 19th EACSL Annual Conference on Computer Science Logic, 2010, Brno, Czech Republic.
    [pdf] [bibtex]
  23. Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs

    Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs

    We embed an operational semantics for security protocols in the interactive theorem prover Isabelle/HOL and derive two strong protocol-independent invariants. These invariants allow us to reason about the possible origin of messages and justify a local typing assumption for the otherwise untyped protocol variables. The two rules form the core of a theory that is well-suited for interactively constructing natural, human-readable, correctness proofs. Moreover, we develop an algorithm that automatically generates proof scripts based on these invariants. Both interactive and automatic proof construction are faster than competing approaches. Moreover, we have strong correctness guarantees since all proofs, including those deriving the underlying theory from the semantics, are machine checked.


    With D. Basin and S. Meier
    CSF 2010, 23rd IEEE Computer Security Foundations Symposium, 2010, Edinburgh, Scotland.
    [pdf] [bibtex]
  24. Session-state Reveal is stronger than Ephemeral Key Reveal: Attacking the NAXOS key exchange protocol

    Session-state Reveal is stronger than Ephemeral Key Reveal: Attacking the NAXOS key exchange protocol

    In the paper Stronger Security of Authenticated Key Exchange [1, 2], 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. 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 show that Session-state Reveal is stronger than Ephemeral Key Reveal, implying that the eCK security model is incomparable to the CK model [5, 6]. In particular we show that the proposed NAXOS protocol from [1, 2] does not meet its security requirements if the Session-state Reveal query is allowed in the eCK model. We discuss the implications of our result for some related protocols proven correct in the eCK model, and discuss the interaction between Session-state Reveal and protocol transformations.


    ACNS '09, proceedings of Applied Cryptography and Network Security, 7th International Conference, Paris-Rocquencourt, France
    [pdf] [bibtex]
  25. Comparing State Spaces in Automatic Security Protocol Analysis

    Comparing State Spaces in Automatic Security Protocol Analysis

    There are several automatic tools available for the symbolic analysis of security protocols. The models underlying these tools differ in many aspects. Some of the differences have already been formally related to each other in the literature, such as difference in protocol execution models or definitions of security properties. However, there is an important difference between analysis tools that has not been investigated in depth before: the explored state space. Some tools explore all possible behaviors, whereas others explore strict subsets, often by using so-called scenarios.

    We identify several types of state space explored by protocol analysis tools, and relate them to each other. We find previously unreported differences between the various approaches. Using combinatorial results, we determine the requirements for emulating one type of state space by combinations of another type.

    We apply our study of state space relations in a performance comparison of several well-known automatic tools for security protocol analysis. We model a set of protocols and their properties as homogeneously as possible for each tool. We analyze the performance of the tools over comparable state spaces. This work enables us to effectively compare these automatic tools, i.e., using the same protocol description and exploring the same state space. We also propose some explanations for our experimental results, leading to a better understanding of the tools.


    With P. Lafourcade and P. Nadeau.
    Formal to Practical Security (LNCS 5458/2009), Springer.
    [pdf] [bibtex]
    Test reproduction archive containing all scripts, the used test data, and protocol description generators: [gzipped tar file]
  26. 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.


    CCS '08: Proceedings of the 15th ACM conference on Computer and communications security, Alexandria, Virginia, USA.
    [pdf] [bibtex]
  27. The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols

    The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols

    CAV tool paper that provides an overview of the Scyther tool.


    CAV 2008, Proceedings of the 20th International Conference on Computer Aided Verification, Princeton, USA, 2008.
    [pdf] [bibtex]
  28. On the Protocol Composition Logic PCL

    On the Protocol Composition Logic PCL

    A recent development in formal security protocol analysis is the Protocol Composition Logic (PCL). We identify a number of problems with this logic as well as with extensions of the logic, as defined in [9, 13, 14, 17, 20, 21]. The identified problems imply strong restrictions on the scope of PCL, and imply that some claimed PCL proofs cannot be proven within the logic, or make use of unsound axioms. This includes the proofs of the CR protocol from [13, 14] and the SSL/TLS and IEEE 802.11i protocols from [20, 21]. Where possible, we propose solutions for these problems.


    ASIACCS'08: Proceedings of the ACM Symposium on Information, Computer and Communications Security, Tokyo, Japan, 2008.
    [pdf] [bibtex]
  29. Comparing State Spaces in Security Protocol Analysis

    Comparing State Spaces in Automatic Security Protocol Verification

    Many tools exist for automatic security protocol verification, and most of them have their own particular language for specifying protocols and properties. Several protocol specification models and security properties have been already formally related to each other. However, there is an important difference between verification tools, which has not been investigated in depth before: the explored state space. Some tools explore all possible behaviors, whereas others explore strict subsets, often by using so-called scenarios. Ignoring such differences can lead to wrong interpretations of the output of a tool. We relate the explored state spaces to each other and find previously unreported differences between the various approaches. We apply our study of state space relations in a performance comparison of several well-known automatic tools for security protocol verification. We model a set of protocols and their properties as homogeneously as possible for each tool. We analyze the performance of the tools over comparable state spaces. This work enables us to effectively compare these automatic tools, i.e. using the same protocol description and exploring the same state space. We also propose some explanations for our experimental results, leading to a better understanding of the tools.

    (This paper is subsumed by the 2009 LNCS article Comparing State Spaces in Automatic Security Protocol Analysis with P. Lafourcade and P. Nadeau, found above.)


    With P. Lafourcade.
    AVoCS'07, ENTCS, 2007.
    [pdf] [bibtex]
    Test reproduction archive containing all scripts, the used test data, and protocol description generators: [gzipped tar file]
  30. A framework for compositional verification of security protocols

    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, Special issue on Computer Security: Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459, Elsevier, 2008.
    [pdf] [bibtex]
  31. Injective synchronisation: an extension of the authentication hierarchy

    Injective synchronisation: an extension of the authentication hierarchy

    Authentication is one of the foremost goals of many security protocols. It is most often formalised as a form of agreement, which expresses that the communicating partners agree on the values of a number of variables. In this paper we formalise and study an intensional form of authentication which we call synchronisation. Synchronisation expresses that the messages are transmitted exactly as prescribed by the protocol description. Synchronisation is a strictly stronger property than agreement for the standard intruder model, because it can be used to detect pre-play attacks. In order to prevent replay attacks on simple protocols, we also define injective synchronisation. Given a synchronising protocol, we show that a sufficient syntactic criterion exists that guarantees that the protocol is injective as well.


    With S. Mauw and E.P. de Vink.
    TCS, Theoretical Computer Science, Volume 6186, Special issue on ARSPA'05, Editors: P. Degano and L. Vigano, 2006, Elsevier.
    [pdf] [bibtex]
  32. A Family of Multi-Party Authentication Protocols

    A Family of Multi-Party Authentication Protocols

    We introduce a family of multi-party authentication protocols and discuss six novel protocols, which are members of this family. The first three generalize the well-known Needham-Schroeder-Lowe public-key protocol, the Needham-Schroeder private-key protocol, and the Bilateral Key Exchange protocol. The protocols satisfy injective synchronisation, which is a strong authentication property, and establish agreement over the nonces. These protocols make use of delegated authentication to keep the protocols small and efficient. For each of these protocols we define a strengthened version that does not rely on delegated authentication. All instantiations of the protocol family consist of 2p-1 messages for p parties, which we show to be the minimal number of messages required to achieve the desired security properties in the presence of a Dolev-Yao style intruder with compromised agents.


    With S. Mauw.
    WISSec'06, First Benelux Workshop on Information and System Security, Antwerpen, Belgium, November 2006.
    [pdf]
  33. Feasibility of multi-protocol attacks

    Feasibility of multi-protocol attacks

    Formal modeling and verification of security protocols typically assumes that a protocol is executed in isolation, without other protocols sharing the network. We investigate the existence of multi-protocol attacks on protocols described in literature. Given two or more protocols, that share key structures and are executed in the same environment, are new attacks possible? Out of 30 protocols from literature, we find that 23 are vulnerable to multi-protocol attacks. We identify two likely attack patterns and sketch a tagging scheme to prevent multi-protocol attacks.


    ARES 2006, Proc. of the first international conference on availability, reliability and security, Vienna, Austria, April 2006, IEEE.
    [pdf] [bibtex]
  34. Compositionality of security protocols: a research agenda

    Compositionality of security protocols: a research agenda

    The application of formal methods to security protocol analysis has been extensively researched during the last 25 years. Several formalisms and (semi-)automatic tools for the verification of security protocols have been developed. However, their applicability is limited to relatively small protocols that run in isolation. Many of the protocols that are in use today cannot be verified using these methods. One of the main reasons for this is that these protocols are composed of several sub-protocols. Such a composition of protocols is not addressed in the majority of formalisms. In this paper we identify a number of issues that are relevant to applying formal methods to the problem of security protocol composition. Additionally, we describe what research needs to be done to meet this challenge.


    VODCA 2004, ENTCS Vol. 142(3), Bertinoro, Italy 1/2006.
    [pdf] [bibtex]
  35. Operational semantics of security protocols

    Operational semantics of security protocols

    Based on a concise domain analysis we develop a formal semantics of security protocols. Its main virtue is that it is a generic model, in the sense that it is parameterized over e.g. the intruder model. Further characteristics of the model are a straightforward handling of parallel execution of multiple protocols, locality of security claims, the binding of local constants to role instances, and explicitly defined initial intruder knowledge. We validate our framework by analysing the Needham-Schroeder-Lowe protocol.


    With S. Mauw.
    Scenarios: models, transformations and tools, international workshop, Dagstuhl castle, Germany, September 7-12, 2003, revised selected papers LNCS, Vol. 3466, 2005, Springer.
    [pdf] [bibtex]
  36. A syntactic criterion for injectivity of authentication protocols

    A syntactic criterion for injectivity of authentication protocols

    Injectivity is essential when studying the correctness of authentication protocols, because non-injective protocols may suffer from replay attacks. The standard ways of verifying injectivity either make use of a counting argument, which only seems to be applicable in a verification methodology based on model-checking, or draw conclusions on the basis of the details of the data-model used. We propose and study a property, the loop property, that can be syntactically verified and is sufficient to guarantee injectivity. Our result is generic in the sense that it holds for a wide range of security protocol models, and does not depend on the details of message contents or nonce freshness.


    With S. Mauw and E.P. de Vink.
    ARSPA 2005, ENTCS Vol. 135(1), July 2005.
    [pdf] [bibtex]
  37. Checking secrecy by means of partial order reduction

    Checking secrecy by means of partial order reduction

    We propose a partial order reduction for model checking security protocols for the secrecy property. Based on this reduction we develop an automatic tool that can check security protocols for secrecy, given a finite execution scenario. We compare this tool to several other tools.


    With S. Mauw.
    SAM 2004: Security Analysis And modelling, 4th Workshop on SDL and MSC, LNCS 3319, Ottawa, Canada 2005, Springer.
    [pdf] [bibtex]
  38. Defining authentication in a trace model

    Defining authentication in a trace model

    In this paper we define a general trace model for security protocols which allows to reason about various formal definitions of authentication. In the model, we define a strong form of authentication which we call synchronization. We present both an injective and a non-injective version. We relate synchronization to a formulation of agreement in our trace model and contribute to the discussion on intensional vs. extensional specifications.


    With S. Mauw and E.P. de Vink.
    FAST 2003, Proceedings of the first international Workshop on Formal Aspects in Security and Trust, Pisa September 2003, IITT-CNR technical report.
    [pdf] [bibtex]

Misc. papers

  1. One-round Strongly Secure Key Exchange with Perfect Forward Secrecy and Deniability

    One-round Strongly Secure Key Exchange with Perfect Forward Secrecy and Deniability

    Traditionally, secure one-round key exchange protocols in the PKI setting have either achieved perfect forward secrecy, or forms of deniability, but not both. On the one hand, achieving perfect forward secrecy against active attackers seems to require some form of authentication of the messages, as in signed Diffie-Hellman style protocols, that subsequently sacrifice deniability. On the other hand, using implicit authentication along the lines of MQV and descendants sacrifices perfect forward secrecy in one round and achieves only weak perfect forward secrecy instead.

    We show that by reintroducing signatures, it is possible to satisfy both a strong key-exchange security notion as well as a strong form of deniability, in one-round key exchange protocols. Our security notion for key exchange is stronger than, e.g., the extended-CK model, and captures perfect forward secrecy. Our notion of deniability, which we call peer-and-time deniability, is stronger than that offered by, e.g., the SIGMA protocol.

    We propose a concrete protocol and prove that it satisfies our definition of key-exchange security in the random oracle model as well as peer-and-time deniability. The protocol combines a signed-Diffie-Hellman message exchange with an MQV-style key computation, and offers a remarkable combination of advanced security properties and efficiency.


    With M. Feltz
    [ePrint]
  2. Evaluation of ISO/IEC 9798 Protocols

    Evaluation of ISO/IEC 9798 Protocols

    This report provides a security evaluation of the authentication protocol families described in parts 2, 3, and 4 of the ISO-IEC 9798 standard. Our analysis includes recommended amendments to the standard.


    With D. Basin.
    CRYPTREC Technical Report, Version 2.0, April 2011.
    [pdf] [bibtex]
  3. Formal methods for security protocols: three examples of the black-box approach

    Formal methods for security protocols: three examples of the black-box approach

    Security protocols are hard to design, even under the assumption of perfect cryptography. With the "classical" Needham-Schroeder protocol as leading example, three so-called black-box approaches to the formal verification of security protocols are sketched. BAN-logic is a light-weight method under the assumption of honest agents and a passive intruder. The Casper/FDR approach translates a high-level description of a security protocol, together with its security requirements and a particular instantiation into CSP, that can be machine-verified using the FDR model checker. In this approach the intruder is in control of the network and is allowed to participate as one of the agents. The same holds for the strand space approach. By focusing on the causal dependency of actions and message passing, one aims to prove security properties of general class of protocols instantiations at the same time.


    With S. Mauw and E.P. de Vink.
    NVTI newsletter, Vol. 7 pp. 21--32, 2003, Newsletter of the Dutch Association for Theoretical Computing Scientists.
    [pdf] [bibtex]

Edited volumes

  1. Proceedings of the first international workshop on security and trust management (STM 2005)
    Edited by S. Mauw, V. Issarny, and C. Cremers, ENTCS, Vol. 157(3) pp. 1-158, September 2005, Milan, Italy. [bibtex]

Ph.D. Thesis

  1. Scyther - Semantics and Verification of Security Protocols
    Thesis, University Press Eindhoven, 2006.
    [bibtex]

Systems

More details can be found here.