Skip to content

Commit 118665b

Browse files
Nicola-Ceorneaclaude
Nicola-Ceornea
and
claude
committed
fv(tamarin): stateful model of the three-way PIN-attempt lockstep reconcile
The stateful companion to the ProVerif secrecy model — proves the reachable- state counter property ProVerif cannot. Tamarin 1.12 + Maude 3.5.1 (prebuilt binaries; no sudo/GHC). `make tamarin`. contracts/verification/tamarin/pin_lockstep.spthy models the three failed- attempt counters (MCU page-124 / OPTIGA F1E1 / SE050 UserID), the attacker's single-counter reset (S-1 OPTIGA glitch / SE050 delete / TZ MCU-erase), and the boot reconcile that wipes on disagreement. All 4 lemmas verified: * honest_boot_possible (anti-vacuity): a provisioned device boots and survives -> the model is not trivially always-wipe. * fresh_synced_means_no_reset (CORE): a surviving 'fresh' boot => NO counter was ever reset. * zero_synced_means_all_reset (CORE): a surviving 'zero' boot => ALL THREE were reset. Together with the above: a surviving boot is reachable ONLY via no-reset or all-three-reset, so a PARTIAL reset (one/two counters) can NEVER survive a boot -> every single-side reset is caught by reconcile. * full_reset_bypass (residual): all-three reset survives -> the documented limitation the hardware-monotonic OPTIGA counter (ship-blocker S-3) closes by removing Reset_OPT, dropping the attacker to "reset 1 of 3" (caught). Honest scope (README): counter value abstracted to status fresh/zeroed (the exact <=10 numeric cap is the per-SE silicon premise this reconcile DEFENDS, not re-proves — Tamarin natural-number arithmetic over the unbounded attempt loop is intractable, confirmed across value/status/loop-free variants); boot is terminal (per-boot reconcile). The tunnel key-establishment handshake stays the one open protocol-verification gap. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 34b09ca commit 118665b

4 files changed

Lines changed: 201 additions & 1 deletion

File tree

‎Makefile‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3534,3 +3534,12 @@ miri:
35343534
proverif:
35353535
@command -v proverif >/dev/null 2>&1 || { echo "ERROR: proverif not found. Install: opam install --assume-depexts proverif (CLI build needs no GTK)"; exit 1; }
35363536
proverif contracts/verification/proverif/dual_se_unlock.pv
3537+
3538+
# Stateful symbolic model (Tamarin) of the three-way PIN-attempt lockstep:
3539+
# a single-counter reset is always caught by the boot reconcile (CORE), an
3540+
# all-three reset is the documented residual. Companion to the ProVerif secrecy
3541+
# model. See contracts/verification/tamarin/README.md.
3542+
.PHONY: tamarin
3543+
tamarin:
3544+
@command -v tamarin-prover >/dev/null 2>&1 || { echo "ERROR: tamarin-prover not found. Install the prebuilt linux64 binary + the maude backend (both need no sudo/GHC; see contracts/verification/tamarin/README.md)"; exit 1; }
3545+
tamarin-prover --prove contracts/verification/tamarin/pin_lockstep.spthy

‎contracts/verification/tamarin/README.md‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
# Tamarin — three-way PIN-attempt lockstep model
2+
3+
Stateful symbolic proof that the three-way PIN-attempt reconcile (MCU page-124
4+
+ OPTIGA F1E1 + SE050 UserID) catches any single/double counter reset, so the
5+
per-counter "≤10 attempts" silicon cap cannot be reset-bypassed without
6+
resetting **all three** counters. This is the **stateful** companion to the
7+
ProVerif secrecy model (`../proverif/`): ProVerif proves the message-level
8+
secrecy/authentication, Tamarin proves the reachable-state counter property
9+
ProVerif (and the impl-proofs / SCA-FI sweeps) cannot.
10+
11+
## Run
12+
13+
```sh
14+
make tamarin # from the repo root
15+
# or directly:
16+
tamarin-prover --prove contracts/verification/tamarin/pin_lockstep.spthy
17+
```
18+
19+
Install (no sudo, no GHC build): drop the prebuilt **tamarin-prover** linux64
20+
binary and the **maude** backend binary into `~/.local/bin`:
21+
22+
```sh
23+
# tamarin-prover (the GitHub release ships a static linux64 binary)
24+
curl -fsSL https://github.com/tamarin-prover/tamarin-prover/releases/download/1.12.0/tamarin-prover-1.12.0-linux64-ubuntu.tar.gz | tar xz
25+
cp tamarin-prover ~/.local/bin/
26+
# maude (Tamarin's rewriting backend)
27+
curl -fsSL -o maude.zip https://github.com/maude-lang/Maude/releases/download/Maude3.5.1/Maude-3.5.1-linux-x86_64.zip
28+
unzip maude.zip && cp maude ~/.local/bin/ # + the *.maude prelude files alongside
29+
```
30+
31+
## What is proven (all four lemmas verified)
32+
33+
| Lemma | Kind | Result | Meaning |
34+
|---|---|---|---|
35+
| `honest_boot_possible` | exists-trace | verified | anti-vacuity: a provisioned device boots and survives — the model is not trivially always-wipe |
36+
| `fresh_synced_means_no_reset` | all-traces | **verified** | a surviving "fresh" boot ⟹ **no** counter was ever reset before it |
37+
| `zero_synced_means_all_reset` | all-traces | **verified** | a surviving "zero" boot ⟹ **all three** counters were reset before it |
38+
| `full_reset_bypass` | exists-trace | verified | the residual: resetting all three together survives a boot |
39+
40+
The two all-traces lemmas **together** are the security property: a surviving
41+
boot is reachable *only* via **no reset** or **all-three reset**, so a **partial
42+
reset (one or two of the three counters) can never survive a boot** — the
43+
un-reset counter(s) desync the reset one and reconcile wipes. A single-side
44+
reset (the **S-1** OPTIGA glitch alone, an **SE050 delete** alone, or a TZ-bypass
45+
**MCU erase** alone) is therefore always caught.
46+
47+
### Maps to the threat model
48+
49+
- This is **Claim 3** (`threat-model.md §6.2`) at the protocol level: every PIN
50+
attack is online, and the three-way lockstep makes a counter rewind detectable.
51+
- The `full_reset_bypass` residual is exactly the documented limitation in
52+
`reconcile_pin_attempts` ("the attacker can reset at most two sides per
53+
campaign"). The **hardware-monotonic OPTIGA counter** (work-todo #24 /
54+
ship-blocker **S-3**) closes it by making `Reset_OPT` impossible — dropping the
55+
attacker to "reset 1 of 3", which `fresh_synced_means_no_reset` catches. So
56+
this model also *quantifies the value of S-3*.
57+
58+
## Out of frame (deliberate — stated, not discovered)
59+
60+
- **Exact ≤10 count**: each counter's value is abstracted to a STATUS — `fresh`
61+
(in lockstep) or `zeroed` (reset). Faithful for the reconcile property
62+
(lockstep counters agree; a reset desyncs one), but it does NOT prove the
63+
numeric "10" cap — that is enforced inside each SE's silicon and is the
64+
per-counter premise this model's reconcile *defends*, not re-proves.
65+
- **One boot per trace**: the boot rule is terminal, so the state space is
66+
finite and the safety lemmas are decidable. reconcile runs at *every* boot, so
67+
the per-boot guarantee proven here is the operative one; the model does not
68+
chain multiple boots in a single trace.
69+
- **Tunnel crypto / message secrecy**: that is the ProVerif model's job
70+
(`../proverif/`). This model is purely about the counter/reconcile state.

‎contracts/verification/tamarin/pin_lockstep.spthy‎

Lines changed: 121 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,121 @@
1+
theory DualSE_PinLockstep
2+
begin
3+
4+
/* ===========================================================================
5+
PQ-Signer — three-way PIN-attempt lockstep, stateful model (Tamarin)
6+
===========================================================================
7+
8+
Companion to the ProVerif secrecy model (contracts/verification/proverif/).
9+
ProVerif proves message-level secrecy/authentication; this proves the
10+
STATEFUL reconcile property it cannot reason about (counter resets +
11+
reachable-state safety).
12+
13+
Mechanism (threat-model.md §6.2 / secure/src/nsc/mod.rs::reconcile_pin_attempts):
14+
three failed-attempt counters — MCU page-124, OPTIGA F1E1, SE050 UserID —
15+
move in LOCKSTEP (every wrong PIN bumps all three). At boot, reconcile()
16+
WIPES the device if the three counters DISAGREE (tamper signal). An attacker
17+
can RESET one counter (OPTIGA via the S-1 glitch / SE050 delete-recreate /
18+
a TZ-bypass MCU-erase) to try to win back attempts.
19+
20+
PROVEN (see lemmas): a surviving boot is reachable ONLY when either NO
21+
counter was reset, or ALL THREE were. Equivalently, a PARTIAL reset (one or
22+
two of the three) can NEVER survive a boot — the un-reset counter(s) desync
23+
the reset one and reconcile wipes. A single-side reset (S-1 alone, SE050
24+
delete alone, MCU erase alone) is always caught. The all-three reset is the
25+
documented residual that the hardware-monotonic OPTIGA counter (work-todo
26+
#24 / ship-blocker S-3) closes by making Reset_OPT impossible — dropping the
27+
attacker from "reset 2 of 3" to "reset 1 of 3", which is caught here.
28+
29+
ABSTRACTIONS (stated, not discovered):
30+
* Each counter's value is abstracted to a STATUS: 'fresh' (in lockstep) or
31+
'zeroed' (attacker-reset). This is faithful for the RECONCILE property:
32+
lockstep counters always agree, a reset desyncs one. It deliberately drops
33+
the exact "<= 10" per-counter silicon cap (enforced inside each SE; out of
34+
this model's frame) — what is proven is that the reconcile DEFENDS that cap
35+
against resets, not the cap value itself.
36+
* The boot rule is TERMINAL (one boot per trace) so the state space is finite
37+
and the safety lemmas are decidable. reconcile runs at EVERY boot, so the
38+
per-boot property proven here is exactly the per-boot guarantee; it does
39+
not model a device continuing across multiple boots in one trace.
40+
=========================================================================== */
41+
42+
/* provisioning: all three counters synced ('fresh'); device Live. */
43+
rule Provision:
44+
[ Fr(~sid) ]
45+
--[ Provision(~sid) ]->
46+
[ MCU(~sid, 'fresh'), OPT(~sid, 'fresh'), SE(~sid, 'fresh'), Live(~sid) ]
47+
48+
/* attacker resets ONE counter to 'zeroed' (powered-off; no Live needed). */
49+
rule Reset_MCU: [ MCU(sid, st) ] --[ Reset(sid, 'MCU') ]-> [ MCU(sid, 'zeroed') ]
50+
rule Reset_OPT: [ OPT(sid, st) ] --[ Reset(sid, 'OPT') ]-> [ OPT(sid, 'zeroed') ]
51+
rule Reset_SE: [ SE(sid, st) ] --[ Reset(sid, 'SE') ]-> [ SE(sid, 'zeroed') ]
52+
53+
/* boot reconcile (TERMINAL). Outcome split by the agreed status so the safety
54+
lemmas avoid a disjunctive conclusion:
55+
- all three 'fresh' => survive (SyncedFresh)
56+
- all three 'zeroed' => survive (SyncedZero)
57+
- any disagreement => Wipe. */
58+
rule Boot_Fresh:
59+
[ MCU(sid, 'fresh'), OPT(sid, 'fresh'), SE(sid, 'fresh'), Live(sid) ]
60+
--[ Boot(sid), SyncedFresh(sid) ]->
61+
[ Survived(sid) ]
62+
63+
rule Boot_Zero:
64+
[ MCU(sid, 'zeroed'), OPT(sid, 'zeroed'), SE(sid, 'zeroed'), Live(sid) ]
65+
--[ Boot(sid), SyncedZero(sid) ]->
66+
[ Survived(sid) ]
67+
68+
rule Boot_Wipe:
69+
[ MCU(sid, m), OPT(sid, o), SE(sid, s), Live(sid) ]
70+
--[ Boot(sid), Wipe(sid), Differ(m, o, s) ]->
71+
[ Wiped(sid) ]
72+
73+
/* Boot_Wipe fires only on genuine disagreement. */
74+
restriction differ:
75+
"All m o s #i. Differ(m, o, s) @ i ==> (not(m = o)) | (not(o = s)) | (not(m = s))"
76+
77+
/* ===========================================================================
78+
LEMMAS (all four verified by `tamarin-prover --prove`)
79+
=========================================================================== */
80+
81+
/* ANTI-VACUITY: a provisioned device can boot and SURVIVE without a wipe. If
82+
this fails the model is trivially always-wipe and the safety lemmas below
83+
are meaningless. */
84+
lemma honest_boot_possible:
85+
exists-trace
86+
"Ex sid #b. SyncedFresh(sid) @ b & not (Ex #w. Wipe(sid) @ w)"
87+
88+
/* CORE (A): a surviving FRESH boot implies NO counter was EVER reset before it.
89+
(The un-reset counters can only stay 'fresh'; any reset would desync them.) */
90+
lemma fresh_synced_means_no_reset:
91+
all-traces
92+
"All sid #b.
93+
SyncedFresh(sid) @ b
94+
==> not (Ex c #r. Reset(sid, c) @ r & r < b)"
95+
96+
/* CORE (B): a surviving ZERO boot implies ALL THREE counters were reset before
97+
it. Together with (A): a surviving boot is reachable ONLY via no-reset or
98+
all-three-reset, so a PARTIAL (one/two) reset can never survive — the
99+
three-way reconcile catches every single-side reset. */
100+
lemma zero_synced_means_all_reset:
101+
all-traces
102+
"All sid #b.
103+
SyncedZero(sid) @ b
104+
==> ( Ex #rm #ro #rs.
105+
Reset(sid, 'MCU') @ rm & rm < b
106+
& Reset(sid, 'OPT') @ ro & ro < b
107+
& Reset(sid, 'SE') @ rs & rs < b )"
108+
109+
/* RESIDUAL (documented limitation): resetting ALL THREE counters together does
110+
survive a boot — reconcile cannot see an all-zero agreement. This is the gap
111+
the hardware-monotonic OPTIGA counter closes (it removes Reset_OPT). */
112+
lemma full_reset_bypass:
113+
exists-trace
114+
"Ex sid #rm #ro #rs #b.
115+
Reset(sid, 'MCU') @ rm & rm < b
116+
& Reset(sid, 'OPT') @ ro & ro < b
117+
& Reset(sid, 'SE') @ rs & rs < b
118+
& SyncedZero(sid) @ b
119+
& not (Ex #w. Wipe(sid) @ w)"
120+
121+
end

0 commit comments

Comments
 (0)