Below is a selection of protocol models for our analysis tools. Several people were involved of the construction of these models, including:

The selection below is by no means complete. Additional models can be found included in the distributions of the tools, as well as other in papers not listed here.

Legend
file PDF file / paper
file Input file for the Scyther tool or for the compromising adversaries version
file Scyther-proof input file
file Tamarin prover input file

IKE (IKEv1 and IKEv2) protocol suites

Using the compromising adversaries version of Scyther tool, we performed a large-scale analysis of the IKE protocol suite, which included all variations of the handshake protocols. A full report can be found in the ESORICS 2011 paper.

IKEv1 and IKEv2 protocol suites
Scyther models: IKE model directory
Analysed in: Key Exchange in IPsec revisited: Formal Analysis of IKEv1 and IKEv2
Protocol origin: RFC 4306 and RFC 5996

What's missing? The current models approximate Diffie-Hellman behaviour, and it would be interesting to perform a more precise analysis with the Tamarin prover. Furthermore, parameter negotiation is currently abstracted away, and this could be modeled more precisely.

ISO/IEC 9798 authentication protocols

We analyzed the family of authentication protocols defined in the ISO/IEC 9798 standard. We found a large number of weaknesses using the Scyther tool. We then proposed fixes and verified the correctness of our fixes using Scyther-proof. The results are described in the POST 2012 paper. Based on our recommendations, the ISO/IEC 9798 standard has been updated.

ISO/IEC 9798 authentication protocols
Scyther models: model directory for the original protocols
Scyther-proof models: project page for the original and repaired protocols
Analysed in: Provably repairing the ISO/IEC 9798 standard for entity authentication
Protocol origin: ISO/IEC 9798 standard for entity authentication

IEEE 802.16e (WIMAX) PKM protocols

Scyther has been used to analyze the PKM protocols that are part of the IEEE 802.16e (WIMAX) standard.

IEEE 802.16e (WIMAX) PKM protocols
Scyther models:PKM models
Analysed in:A framework for compositional verification of security protocols
Protocol origin: IEEE 802.16e (WIMAX) standard

Authenticated Key Exchange (AKE) protocols

We used our tools to analyze several Authenticated Key Exchange (AKE) protocols with respect to their intended adversary models.

Scyther models

The protocols in the table below that have Scyther models were analyzed using the compromising-adversaries variant of Scyther tool. The underlying theory, which extends the original operational semantics underlying Scyther, and the analysis results are described in the ESORICS 2010 paper. In the accompanying CSL 2010 paper, we introduced the concept of a protocol security hierarchy and analyzed the other protocols with Scyther models, determining their relative strengths.

During initial analysis, we automatically discovered an attack on HMQV that uses the session-state reveal query. (Such attacks are of theoretical interest but not apply to most current deployments.)

The Scyther models for these protocols are part of the Scyther (compromise version) distribution and can be found in the Protocols/AdversaryModels/ directory. Alternatively, the relevant protocol models can be directly accessed here.

Tamarin models

One drawback of some of the Scyther models is their relatively coarse modeling of the adversary's capabilities with respect to Diffie-Hellman exponentiation. More precise models can be analysed using the Tamarin prover, as presented in the Tamarin paper. In that paper we perform a large case study, which involves all the protocols in the below table that have Tamarin models. The complete list of Tamarin models in this case study can be found here.

HMQV
Scyther models:HMQV
Analysed in:Modeling and Analyzing Security in the Presence of Compromising Adversaries
Protocol origin: HMQV: A High-Performance Secure Diffie-Hellman Protocol
DHKE-1
Scyther models:DHKE-1
Analysed in: Modeling and Analyzing Security in the Presence of Compromising Adversaries
Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries
Protocol origin:On formal models for secure key exchange (version 4)
Bilateral Key Exchange
Scyther models:BKE
Analysed in:Modeling and Analyzing Security in the Presence of Compromising Adversaries
BCNP-1 and BCNP-2
Scyther models: BCNP-1, BCNP-2
Analysed in:Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries
Protocol origin:One-round key exchange in the standard model
Signed Diffie-Hellman
Scyther models:Signed-DH
Analysed in: Modeling and Analyzing Security in the Presence of Compromising Adversaries
Tamarin models: Signed-DH
Analysed in:Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
KEA+
Scyther models:KEA+
Analysed in:Modeling and Analyzing Security in the Presence of Compromising Adversaries
Tamarin models: Tamarin
Analysed in:Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
Protocol origin:Security Analysis of KEA Authenticated Key Exchange Protocol
TS1, TS2, and TS3 (2004 and 2008 versions)
Scyther models:model directory
Analysed in: Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries
Tamarin models: model directory
Analysed in:Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
Protocol origin:One-Round Protocols for Two-Party Authenticated Key Exchange (2004)
Updated version (2008)
NAXOS
Scyther models:NAXOS
Analysed in: Modeling and Analyzing Security in the Presence of Compromising Adversaries
Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries
Tamarin models: NAXOS
Analysed in:Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
Protocol origin: Stronger security of authenticated key exchange
KAS1 and KAS2
Tamarin models: KAS1, KAS2
Analysed in:Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
Protocol origin: A Generic Variant of NIST's KAS2 Key Agreement Protocol
STS-MAC (Station-to-Station) and fixed variants
Tamarin models:model directory
Analysed in:Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
Protocol origin: Authentication and authenticated key exchanges
UM (Unified Model)
Tamarin models:UM
Analysed in:Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties
Protocol origin:Authenticated Diffe-Hellman Key Agreement Protocols

Yubikey and YubiHSM

Tamarin was used to analyse the Yubikey and YubiHSM protocols.