Building Confidence in Cryptographic Protocols

Why a “We Tried Hard” Argument Isn’t a Security Proof

Cryptographers are constantly building new systems, but the fact that the designers themselves can’t break their own creations doesn’t mean much. It only demonstrates that they aren’t smart enough to find the flaws. Trying all known attacks offers some confidence, but it can’t anticipate new attack families. Offering prizes for breaks suffers from the same fundamental limitation: you can’t be sure everyone would prefer the bounty over selling an exploit.

Since the late 1980s, researchers have pursued a more rigorous path: mathematical proof. The basic idea is straightforward. A proof starts from explicit assumptions and uses logical inference to reach a conclusion. If the assumptions hold, the conclusion must too. This is exactly the structure of Euclid’s geometry, where a handful of postulates support a vast body of theorems.

Security proofs for protocols work the same way, but they’re far larger than anything in The Elements. The machine-checked proof of KEMTLS, a post-quantum variant of TLS, runs to nearly 500,000 lines. That scale is only possible because computers can assist: theorem provers handle the tedious symbol manipulation while humans guide the strategy.

To reason about a protocol at all, we first need a formal description. A protocol isn’t a single program but a set of interacting processes. Process algebras provide the language for this. Just as high-school algebra replaces specific numbers with symbols, a process algebra represents programs and their values symbolically. Rules define how expressions can be transformed, much like the algebraic manipulation of equations.

The Tamarin prover implements this approach. A protocol is described by rules that operate on a “bag of facts.” Each rule has preconditions—facts that must be present—and postconditions, which are facts added to the bag. Actions recorded when a rule fires let us track what happened in a run.

rule Register_pk:
  [ Fr(~ltkA) ]
--[ GenLtk($A, ~ltkA)]->
  [ !Ltk($A, ~ltkA), !Pk($A, pk(~ltkA)), Out(pk(~ltkA)) ]

That rule, for instance, generates a fresh long-term key pair. The Fr(~ltkA) precondition is always satisfiable: Tamarin can always produce fresh values. The postconditions register the private key as !Ltk($A, ~ltkA), the public key as !Pk($A, pk(~ltkA)), and publish the public key to the network via Out(pk(~ltkA)). Tamarin follows the Dolev-Yao model, where the attacker controls the network, so publishing makes the key available to the adversary.

Applying rules in sequence simulates a protocol run. Since multiple rules may be applicable at any point, all possible executions form a tree. If we can show no branch of that tree reaches a “bad” state, the protocol is secure with respect to our stated goals. A reachability lemma captures such questions: does there exist a path where the attacker learns the session key?

Formal Analysis and Its Limits

The workflow for formal analysis is therefore:

1. Define precise security goals.
2. Describe the protocol as symbols and transformation rules.
3. Build the tree of all possible runs.
4. Verify no branch violates the security goals.

This methodology proved its worth during TLS 1.3 development, where it uncovered serious flaws that were fixed before standardization. But it has pitfalls. Proofs can contain mistakes, and they can prove something other than what you think. The Needham-Schroeder protocol was proven secure in BAN logic before Lowe found an attack the logic didn’t cover. Similarly, the initial TLS 1.3 proof assumed no one uses the same certificate for client and server roles—a gap that led to the “Selfie” vulnerability.

Formal analysis also says nothing about whether an implementation matches the specification. It operates on a model, not on code.

Why Prove KEMTLS in Tamarin

KEMTLS replaces the signature-based authentication in TLS handshakes with key encapsulation. Instead of signing to prove possession of a private key, the client encapsulates a shared secret to the server’s KEM public key. Only the holder of the corresponding private key can decapsulate it and derive the traffic keys.

A pen-and-paper proof of KEMTLS already exists. Why bother with a machine-checked one? Because hand-written proofs are extremely hard to get right. After the KEMTLS paper was published at a top-tier conference, mistakes were found in its model definitions. Human readers tend to infer intended meaning even where it isn’t strictly stated. Computers don’t.

One “war story” from the KEMTLS modeling effort: the authors initially assumed an IND-CPA-secure KEM sufficed for the ephemeral key exchange. Only after writing out all simulations in pseudo-code did it become clear that an additional oracle for a single decapsulation query was needed—requiring IND-1CCA security instead. An IND-CPA-only KEM would not have been secure.

Machine proofs are also extensible. The “pre-distributed keys” extension of KEMTLS had only been proven on paper in isolation. Tamarin makes it possible to prove that extension alongside the main protocol, ruling out cross-functional attacks, even though the combined proof is exponentially more complex.

Finally, the two proof styles are complementary. The computational model used in the pen-and-paper proof gives tight bounds on security but requires simplifications, such as ignoring TLS message formats. The symbolic model used in Tamarin provides a binary yes/no answer while capturing those format details.

Modeling KEMTLS

Modeling KEMTLS in Tamarin began by reusing the TLS 1.3 model built by Cremers et al. during the standardization effort. The Diffie-Hellman operations were replaced with KEM operations, and the certificate-handling messages were modified: instead of sending a signature, the client sends back an encapsulated ciphertext.

rule client_recv_server_cert_emit_kex:
let
  // … snip
  ss = kemss($k, ~saseed)
  ciphertext = kemencaps($k, ss, certpk)
  // NOTE: the TLS model uses M4 preprocessor macros for notation
  // We also made some edits for clarity
in
  [
    State(C2d, tid, $C, $S, PrevClientState),
    In(senc{<'certificate', certpk>}hs_keys),
    !Pk($S, certpk),
    Fr(~saseed)
  ]
  --[
    C2d(tid),
    KemEncap($k, certpk, ss)
  ]->
  [
    State(C3, tid, $C, $S, ClientState),
    Out(senc{<'encaps', ciphertext>}hs_keyc)
  ]

That rule represents the client receiving the server’s certificate and encapsulating a fresh key to it. The preconditions include the client having reached stage C2d, receiving an encrypted message from the network, the server’s permanent public key fact !Pk(S, certpk), and a fresh random seed. The postconditions advance the client to state C3 and output the encapsulation encrypted under the client’s handshake key. The recorded actions let us track that the client is “running with” certain values—believing they’re correct without yet being certain.

As a sanity check, the first lemma asked whether the model can execute at all:

lemma exists_C2d:
    exists-trace
    "Ex tid #j. C2d(tid)@#j"

This exists-trace lemma only needs one valid run, not all. It confirmed Tamarin could reach the C2d state, meaning the model isn’t vacuously secure.

Modeling a Stronger Adversary

In the symbolic model, cryptography is perfect: without the right key, the adversary cannot decrypt or decapsulate. A proof against this default adversary covers message reordering and replay, but KEMTLS aims higher. The adversary is given explicit powers to reveal long-term and ephemeral keys.

rule Register_pk:
  [ Fr(~ltkA) ] 
  --[  GenLtk($A, ~ltkA)  ]->
  [ !Ltk($A, ~ltkA), 
    !Pk($A, kempk($k, ~ltkA)), 
    Out(kempk($k, ~ltkA))
  ]

That rule generates KEM key pairs for participants, publishing the public key. The adversary, however, gets a Reveal query to obtain the private key:

rule Reveal_Ltk:
   [ !Ltk($A, ~ltkA) ] --[ RevLtk($A) ]-> [ Out(~ltkA) ]

This registers a RevLtk($A) action, marking $A’s certificate as untrusted from that point on.

Key Security Lemmas

The central security property for a handshake protocol is that the session keys remain secret:

lemma secret_session_keys [/*snip*/]:
  "All tid actor peer kw kr aas #i.
      SessionKey(tid, actor, peer, <aas, 'auth'>, <kw, kr>)@#i &
      not (Ex #r. RevLtk(peer)@#r & #r < #i) &
      not (Ex tid3 esk #r. RevEKemSk(tid3, peer, esk)@#r & #r < #i) &
      not (Ex tid4 esk #r. RevEKemSk(tid4, actor, esk)@#r & #r < #i)
    ==> not Ex #j. K(kr)@#j"

The lemma quantifies over the thread id, actor, peer, read and write keys, and an authentication status. It requires that there is no RevEKemSk or RevLtk action on keys used in the session, and asserts the attacker can never learn the read key kr.

Two questions naturally arise. First: why bother modeling attacker abilities if the lemma restricts them? The answer is that those abilities aren’t restricted globally—only for keys used in the session being proved. The attacker can compromise every other key. Moreover, the lemma permits compromising session keys after the session completes. That models forward secrecy: an attacker who recorded the session and later obtains long-term keys, perhaps with a quantum computer, still can’t decrypt it.

Second: why only the read key? Because the lemma is symmetric. In a TLS session, the client’s read key is the server’s write key and vice versa. Proving the read key secret for all actors proves both keys secret.

Running the Proofs

Tamarin offers an autoprover, but it often needs guidance. Its manual interface lets you steer which goal to pursue, with proof branches displayed visually—green for proved, open cases awaiting decisions.

Helper lemmas act like factored-out functions, splitting large proofs into digestible chunks that the prover can reuse. Sometimes this makes lemmas automatable; other times, an “oracle” script encodes manual heuristics to drive the proof. The downside is that helper lemmas can distract the autoprover, sending it down irrelevant chains of reasoning. Hiding such lemmas sometimes lets the autoprover finish the job.

These strategies demand considerable intuition. One practical trick was using highly recognizable variable names in lemmas to reconstruct where goals in the Tamarin interface came from. The autoprover was nonetheless essential: every change to a lemma or the model requires re-proving everything, and manual effort at that scale would be impractical.

A case in point: after completing the proof, refactoring changes to the session_key_agreement lemma altered its meaning without any obvious syntactic error. Unraveling that took significant time. The original definition covered the right properties, so no security issue resulted, but the episode illustrates how fragile these artifacts can be.

Formal Methods in Practice

The TLS 1.3 development process showed what formal analysis can contribute to protocol design. Machine-verified proofs should accompany proposals for new security protocols. Natural language specifications are inherently ambiguous, and informal interpretations lead to vulnerabilities.

This work shouldn’t be confined to academia. Many protocols originate in industry, and tooling usability for non-experts isn’t yet where it needs to be. Making these tools accessible will require collaboration between researchers and practitioners—a direction worth pursuing for the security of future protocols.