Reading Tamarin Prover Output: A Visual Tutorial

Introduction

Tamarin Prover is a tool for formally verifying security protocols. You give it a model of a protocol and properties you want to verify, and it either proves the property holds for all possible executions or finds a counterexample -- a concrete attack.

Tamarin's interactive UI produces dependency graphs and proof trees that can be hard to interpret at first. This tutorial walks through them using a simple key-exchange protocol, building up from the basics.

The full interactive version of this tutorial (with step-through trace explorers, expandable proof trees, and live protocol comparison) is available as a standalone interactive page. The companion Tamarin theory files are available for download:

• tutorial.spthy -- working theory

• tutorial_broken.spthy -- broken version (for counterexample demo)

The Protocol

We use a simple encrypted message exchange:

1. Bob generates a keypair (sk, pk(sk)) and publishes the public key

2. Alice picks a fresh secret, encrypts it with Bob's public key, sends the ciphertext

3. Bob decrypts with his private key

Properties we verify:

• executable: Can this protocol actually run? (sanity check)

• secrecy: Can the adversary learn the secret? (security property)

Core Concepts

rule Alice_Send:
  [ Fr(~secret), !Pk($B, pkB) ]                  // PREMISES
  --[ Secret(~secret), Sent($A, $B, ~secret) ]->  // ACTIONS
  [ Out(aenc(~secret, pkB)) ]                     // CONCLUSIONS

The Theory

Here is the complete Tamarin theory:

theory Tutorial
begin

builtins: asymmetric-encryption

rule Generate_Keypair:
  [ Fr(~sk) ]
  --[ KeyGen($B, ~sk) ]->
  [ !Sk($B, ~sk), !Pk($B, pk(~sk)), Out(pk(~sk)) ]

rule Alice_Send:
  [ Fr(~secret), !Pk($B, pkB) ]
  --[ Secret(~secret), Sent($A, $B, ~secret) ]->
  [ Out(aenc(~secret, pkB)) ]

rule Bob_Receive:
  [ !Sk($B, skB), In(aenc(secret, pk(skB))) ]
  --[ Received($B, secret) ]->
  [ ]

lemma executable:
  exists-trace
  "Ex A B s #i #j. Sent(A, B, s) @ i & Received(B, s) @ j & i < j"

lemma secrecy:
  all-traces
  "All s #i. Secret(s) @ i ==> not(Ex #j. K(s) @ j)"

end

Reading Attack Traces

When you click an exists-trace lemma (like executable), Tamarin finds a concrete execution that satisfies the formula and displays it as a dependency graph.

How to read it:

• Time flows top to bottom. Earlier events are higher.

• Boxes are rule instances. Each box is one specific firing of a rule with concrete values bound to variables.

• Arrows are fact dependencies. An arrow from Box A to Box B means "A produced a fact that B consumed."

• Solid arrows = linear fact flow (consumed on use).

• Dashed arrows = persistent fact flow (read but not consumed).

• Red arrows = network flow (Out -> In, through the adversary).

The executable trace shows three boxes in sequence: Generate_Keypair -> Alice_Send -> Bob_Receive, connected by persistent fact arrows (!Pk, !Sk) and a network arrow (Out(aenc(...)) -> In(aenc(...))).

Reading Proof Trees

When you click an all-traces lemma that is VERIFIED (like secrecy), Tamarin shows a proof tree -- backward reasoning from the goal.

Tamarin works backwards:

1. Assume the negation: "Suppose the adversary knows the secret."

2. Case split: "What rule could have produced K(~secret)?"

3. For each case, ask what preconditions are needed.

4. Each branch either hits a contradiction (green leaf, closed) or leads to a complete attack (red leaf, property violated).

For secrecy, every branch closes:

• The adversary would need Bob's private key ~sk to decrypt

• ~sk is in !Sk (persistent) but never in any Out() fact

• The adversary only learns values on the network

• Contradiction on every branch. VERIFIED.

Introducing a Bug

What if Bob accidentally leaks the secret? Add this rule:

rule Bob_Receive:
  [ !Sk($B, skB), In(aenc(secret, pk(skB))) ]
  --[ Received($B, secret) ]->
  [ ]

rule Bob_Receive_And_Leak:
  [ !Sk($B, skB), In(aenc(secret, pk(skB))) ]
  --[ Received($B, secret) ]->
  [ Out(secret) ]

rule Bob_Receive_And_Leak:
  [ !Sk($B, skB), In(aenc(secret, pk(skB))) ]
  --[ Received($B, secret) ]->
  [ Out(secret) ]     // <-- secret in cleartext!

Now secrecy is FALSIFIED. The counterexample trace shows the same structure as an attack trace, but with an adversary derivation at the bottom:

1. Generate_Keypair -> Alice_Send -> Bob_Receive_And_Leak

2. Out(secret) puts the plaintext on the network

3. K(~secret) -- adversary learns it

The vulnerability is visible immediately: no MFA gate, no encryption, just Out(secret) in the clear.

The Adversary

Tamarin uses the Dolev-Yao adversary model:

• Sees all network messages (Out facts)

• Can inject any message it can construct (In facts)

• Can decompose, encrypt, decrypt (only with known keys)

• Cannot break cryptographic primitives

In graphs, adversary derivation nodes appear as small boxes labeled coerce, adec, pair, etc. K(x) is the terminal node: "adversary knows x."

Variable Conventions

From Here to IAMReach

The IAMReach project uses exactly the same Tamarin structure to model AWS IAM role chains:

Try It

# Install Tamarin
brew install tamarin-prover

# Automated proofs
tamarin-prover tutorial.spthy --prove

# Interactive UI (recommended)
tamarin-prover interactive tutorial.spthy
# Opens at http://127.0.0.1:3001

Or explore the interactive tutorial with step-through traces, expandable proof trees, and a live protocol comparison toggle.