Computationally sound protocol verification tools promise to deliver full-strength
cryptographic proofs for security protocols. Unfortunately, current tools lack either modularity …

Many proofs of interactive cryptographic protocols (eg, as in Universal Composability)
operate by proving the protocol at hand to be observationally equivalent to an idealized …

Critical and widely used cryptographic protocols have repeatedly been found to contain
flaws in their design and their implementation. A prominent class of such vulnerabilities is …

Messaging Layer Security (MLS), currently undergoing standardization at the IETF, is an
asynchronous group messaging protocol that aims to be efficient for large dynamic groups …

The formal analysis of cryptographic protocols traditionally focuses on trace and
equivalence properties, for which decision procedures in the symbolic (or Dolev-Yao, or DY) …

The building blocks for secure messaging apps, such as Signal's X3DH and Double Ratchet
(DR) protocols, have received a lot of attention from the research community. They have …

Security protocols are essential building blocks of modern IT systems. Subtle flaws in their
design or implementation may compromise the security of entire systems. It is, thus …

Data formats used for cryptographic inputs have historically been the source of many attacks
on cryptographic protocols, but their security guarantees remain poorly studied. One reason …

The Noise protocol framework defines a succinct notation and execution framework for a
large class of 59+ secure channel protocols, some of which are used in popular applications …

We present the formal verification of Apple's iMessage PQ3, a highly performant, device-to-
device messaging protocol offering strong security guarantees even against an adversary …