• Home
• News
• Research
• Publications
• People
• Analysis tools
• Protocol Models
• Contact

Our research involves formal methods and cryptography for the analysis and development of secure systems. The pages below describe selected research areas and provide links to papers, tools, and protocol models.

• Formal verification of security protocols

  How can we model security protocols, find attacks, and establish their security properties using automated tools?

  Methods and tools for security protocol verification, including Tamarin, Scyther, symbolic models, automated analysis, and machine-checked proofs.

• Secure messaging

  How can we establish security guarantees for messaging protocols and the conversations built from them?

  Security analysis of messaging protocols, from Signal's Double Ratchet to session handling, asynchronous group messaging, and MLS.

• Post-compromise security

  Under which conditions can communication become secure again after a party's secrets have been compromised?

  Definitions, constructions, and limits of post-compromise security, including clone detection, healing in group messaging, and resilience to state loss.

• Security protocol standards

  How can formal analysis help identify weaknesses in security protocol standards and establish guarantees for their designs?

  Analysis and improvement of security protocol standards, including TLS 1.3, MLS, SPDM, and ISO/IEC authentication and key establishment protocols.

• Cryptographic primitives

  Which properties do cryptographic protocols require from their primitives, and what happens when those properties do not hold?

  Security properties of signatures, key encapsulation mechanisms, Diffie-Hellman groups, authenticated encryption, and hash functions, and their consequences for protocol security.

• Applied cryptography

  How can we define and prove the security of cryptographic protocols under explicit assumptions about their primitives and adversaries?

  Computational security definitions and proofs for key exchange, secure messaging, password-based authentication, cryptographic primitives, and post-quantum protocols.

• Protocol composition

  When do protocols that are secure in isolation remain secure when combined or run alongside other protocols?

  Conditions for securely combining protocols, including multi-protocol attacks, compositional verification, dynamic corruption, and the composition of key exchange with symmetric-key protocols.

• Key exchange and group key establishment

  How can two parties or a group establish and update shared keys securely, even when some secrets are compromised?

  Security definitions, constructions, and analysis of key exchange, including TLS, Signal's handshake, ART, MLS, password-authenticated key exchange, and post-quantum protocols.

For all works and bibliographic details, see the complete chronological publication list.