Learn to interpret attack traces, proof trees, and counterexample graphs in Tamarin's interactive UI — using a simple key-exchange protocol. No prior Tamarin knowledge required.
Tamarin Prover is a tool for formally verifying security protocols. It either proves a property holds for all possible executions, or finds a concrete attack that violates it. This tutorial teaches you to read its visual output.
Alice wants to send Bob a secret. Bob publishes a public key, Alice encrypts with it, Bob decrypts with his private key.
executable
Can this protocol actually complete? (Sanity check — the answer should be yes.)
secrecy
Can the adversary learn the secret? (No — the encryption protects it.)
Hover over highlighted elements for explanations.
Every rule has three parts. Click each zone to learn what it does.
Each rule has premises (consumed), actions (logged), and conclusions (produced).
When you load a theory in the interactive UI, you see rules on the left and lemmas on the right. Badges show proof status.
For exists-trace lemmas, Tamarin finds a concrete execution and displays it as a dependency graph. Time flows top to bottom. Boxes are rule firings, arrows show which facts flow between them.
Click "Step Through" to walk through the trace one rule at a time.
!Sk, !Pk — read by many rules)For all-traces lemmas that are VERIFIED, Tamarin shows a proof tree — backward reasoning that exhaustively closes all possible attacks. Click nodes to expand.
Click any node to expand or collapse it. Green leaves are contradictions — the adversary fails. When all leaves are green, the property holds.
What if Bob accidentally leaks the secret after decrypting it? Toggle between the clean and broken protocol to see what changes.
When an all-traces lemma is FALSIFIED, the graph shows a concrete attack — the same format as an attack trace, but with an adversary derivation showing how the secret leaks.
Click "Step Through" to see how the adversary learns the secret.
Quick reference for the visual elements in Tamarin graphs.
IAMReach uses exactly the same Tamarin structure. Here's how concepts map:
| Tutorial | IAMReach |
|---|---|
Generate_Keypair | LegitLambdaInit — entity gets role credentials |
Alice_Send | Assume_X_to_Y — sts:AssumeRole call |
!Pk($B, pk(~sk)) | !ExternalId('Vendor', 'Target', id) — shared secret |
MFAAuth(e, token) as premise | MFA gate on a trust relationship |
!LegitMarker(e) | Entity is legitimate (not an adversary) |
K(~secret) | Adversary reaches a target role |
| Counterexample trace | The IAM role chain violating a property |
| Proof tree | Exhaustive proof that isolation holds |
When a FALSIFIED lemma appears in an IAMReach theory, read the counterexample trace the same way: boxes are role assumptions, arrows are credential flows, and the adversary derivation shows the attack path.