Send email Copy Email Address
Research Group

Cremers

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, supportive technologies and improving security standards.

Head of Group

Cas Cremers

Email

Address

Stuhlsatzenhaus 5
66123 Saarbrücken (Germany)

Areas of interest

  • security protocols

  • formal methods

  • applied cryptography

  • analysis tools

  • automated verification

  • protocols and standards 

Most Recent Publications

Year 2024

Conference / Medium

SP
IEEE S&PIEEE Symposium on Security and Privacy

Conference / Medium

SP
IEEE Symposium on Security and PrivacyIEEE Symposium on Security and Privacy

Year 2023

Conference / Medium

USENIX-Security
Usenix SecurityUSENIX Security Symposium 2023

Conference / Medium

USENIX-Security
Proceedings of USENIX 2023USENIX 2023

ANALYSIS TOOLS

Security protocol analysis tools

We have developed several tools for the symbolic analysis of security protocols. 

The executive summary is: for standard analysis with respect to various adversary models, or learning about security protocols, use Scyther. If you want machine-checked proofs, use scyther-proof. For advanced analysis and cutting-edge features, use Tamarin.

A high-level overview of their differentiating features you find here.

PROTOCOL MODELS

Selected protocol models for our analysis tools

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.

 

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.

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

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

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-1BCNP-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: KAS1KAS2
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

Tamarin was used to analyse the Yubikey and YubiHSM protocols.

Yubikey and YubiHSM
Tamarin models: Yubikey and YubiHSM
Analysed in: YubiSecure? Formal Security Analysis Results for the Yubikey and YubiHSM

MISC PROJECTS

pdfdiff.py

pdfdiff.py is a small python script that can be used to view the difference between two PDF or PS files.

 

Download

Download pdfdiff.py 0.92, released on October 4, 2007.

After downloading, either run it through python or make it executable (chmod +x pdfdiff.py) to use it directly from the commandline.

Requirements

  • pdftotext, which is part of the xpdf package.
  • Python
  • A diff viewer, preferably one that supports unicode, like kdiff3 or meld. If these don't work for you, you can use xxdifftkdiffopendiffvimdiff, or even good old diff. You only need one of these to use pdfdiff.py.

Note that for most Linux distributions, installing xpdf is usually sufficient to get it working. (Afterwards one might want to upgrade to a better diff viewer though).

Development

pdfdiff.py is now hosted on Github: please visit the pdfdiff project page.

Use cases

  • (Scientific) Reviews: you reviewed version A of a paper, and receive version B, and wonder what the changes are.

(Feel free to invent your own cases, and let me know.)

What pdfdiff does

pdfdiff takes two arguments, each being the filename of a PDF file, and generates a textual diff between the two. It visualises this diff using the first diff-viewer it finds on the system.

pdfdiff relies on pdftotext to extract the plaintext from a PDF file. However, small changes in the text between two PDF files can make a huge difference in the resulting extracted text. More often than not, the difference is so large that doing a diff on the output does not yield a sensible result.

The main function of this program, pdfdiff, is to normalize the output of pdftotext, such that the result is suitable for diff viewing. To achieve this, it attempts to detect sentence endings to reformat paragraphs and lines. Along the way, it removes some ligature encodings to give diff viewers an easier time. After this normalisation procedure, diff viewers commonly yield a substantially better comparison between the contents of the files.

Note that if a single file is provided as input, pdfdiff will directly output the normalised text, enabling its use as a preprocessor for other tools.