CryptoVerif and Tamarin models, minor doc updates
Signed-off-by: Kamal Tufekcic <kamal@lo.sh>
This commit is contained in:
Kamal Tufekcic
parent
9ba7ea2def
commit
3acaa0fa3f
18 changed files with 2925 additions and 8 deletions
215
tamarin/LO_Ratchet.spthy
Normal file
215
tamarin/LO_Ratchet.spthy
Normal file
|
|
@ -0,0 +1,215 @@
|
|||
theory LO_Ratchet
|
||||
begin
|
||||
|
||||
/*
|
||||
* LO-Ratchet: Forward Secrecy (Theorem 4) and Post-Compromise Security (Theorem 5)
|
||||
* =================================================================================
|
||||
*
|
||||
* Abstract model: epoch keys are Fr() (fresh names), not KDF-derived.
|
||||
* This proves FS and PCS are STRUCTURAL properties of the state machine,
|
||||
* independent of KDF/KEM security. Send and recv are modeled as separate
|
||||
* sections to avoid Tamarin non-termination on combined state machines.
|
||||
*
|
||||
* Corruption comes in two flavors:
|
||||
* - Consuming (Corrupt_S/R): reveals state, terminates session → used for FS
|
||||
* - Non-consuming (Observe_S/R): reveals state, session continues → used for PCS
|
||||
*
|
||||
* LIMITATIONS: This abstraction does NOT capture:
|
||||
* - KEM-level PCS (compromised sk_s means compromised ss for one step)
|
||||
* - Message key derivation (mk = KDF_MsgKey(ek, n)) or Theorem 3
|
||||
* - Message counters, skip handling, or replay detection
|
||||
*
|
||||
* EXPECTED RESULTS:
|
||||
* send_sanity: VERIFIED
|
||||
* send_fs: VERIFIED (Theorem 4a)
|
||||
* send_corrupt_terminates: VERIFIED
|
||||
* send_pcs: VERIFIED (Theorem 5, send)
|
||||
* recv_sanity: VERIFIED
|
||||
* recv_fs_1step: FALSIFIED (Theorem 4b, 1-step counterexample)
|
||||
* recv_fs_2step: VERIFIED (Theorem 4b, 2-step FS)
|
||||
* recv_corrupt_terminates: VERIFIED
|
||||
* recv_pcs: VERIFIED (Theorem 5, recv)
|
||||
*/
|
||||
|
||||
|
||||
/* ================= SEND SIDE (unchanged — already works) ================= */
|
||||
|
||||
restriction Once_S:
|
||||
"All #i #j. InitS() @i & InitS() @j ==> #i = #j"
|
||||
|
||||
rule Bounds_S:
|
||||
[ ] --> [ !BS('1','2'), !BS('2','3'), !BS('3','4') ]
|
||||
|
||||
rule Init_S:
|
||||
[ Fr(~ek) ]
|
||||
--[ InitS() ]->
|
||||
[ S('1', ~ek, 'pending') ]
|
||||
|
||||
rule KEM_Send:
|
||||
[ S(step, ek_s, 'pending'), !BS(step, next), Fr(~ek2) ]
|
||||
--[ Send(~ek2) ]->
|
||||
[ S(next, ~ek2, 'idle') ]
|
||||
|
||||
rule Advance_S:
|
||||
[ S(step, ek_s, 'idle'), !BS(step, next) ]
|
||||
-->
|
||||
[ S(next, ek_s, 'pending') ]
|
||||
|
||||
// Consuming corruption: reveals epoch key, terminates session (for FS proofs)
|
||||
rule Corrupt_S:
|
||||
[ S(step, ek_s, status) ]
|
||||
--[ CorruptS(), RevealedS(ek_s) ]->
|
||||
[ ]
|
||||
|
||||
// Non-consuming observation: reveals epoch key, session continues (for PCS proofs)
|
||||
rule Observe_S:
|
||||
[ S(step, ek_s, status) ]
|
||||
--[ ObserveS(), ObservedS(ek_s) ]->
|
||||
[ S(step, ek_s, status) ]
|
||||
|
||||
restriction Once_ObserveS:
|
||||
"All #i #j. ObserveS() @i & ObserveS() @j ==> #i = #j"
|
||||
|
||||
lemma send_sanity:
|
||||
exists-trace
|
||||
"Ex ek1 ek2 #i #j. Send(ek1) @i & Send(ek2) @j & i < j"
|
||||
|
||||
lemma send_fs:
|
||||
"All ek ek2 #i #j #c.
|
||||
Send(ek) @i & Send(ek2) @j & CorruptS() @c &
|
||||
i < j & j < c
|
||||
==> not (Ex #r. RevealedS(ek) @r)"
|
||||
|
||||
// Consuming corruption terminates the session: no Send can follow CorruptS.
|
||||
lemma send_corrupt_terminates:
|
||||
"All ek #s #c. Send(ek) @s & CorruptS() @c ==> s < c"
|
||||
|
||||
// Theorem 5 (PCS, send side): after non-consuming observation, one fresh
|
||||
// KEM ratchet step produces an epoch key the adversary never observed.
|
||||
// (Structurally trivial in this abstraction — Fr() is always fresh — but
|
||||
// documents that the state machine permits recovery from compromise.)
|
||||
lemma send_pcs:
|
||||
"All ek_new #obs #send.
|
||||
ObserveS() @obs &
|
||||
Send(ek_new) @send & obs < send
|
||||
==> not (Ex #r. ObservedS(ek_new) @r)"
|
||||
|
||||
|
||||
/* ================= RECV SIDE (unrolled) ================= */
|
||||
|
||||
/*
|
||||
* State machine (each node is a distinct fact):
|
||||
*
|
||||
* Init → R1(ek_r, prev) "idle"
|
||||
* ↓ Recv1
|
||||
* R2(ek_r, prev) "pending"
|
||||
* ↓ Adv1
|
||||
* R3(ek_r, prev) "idle"
|
||||
* ↓ Recv2
|
||||
* R4(ek_r, prev) "pending"
|
||||
* ↓ Adv2
|
||||
* R5(ek_r, prev) "idle"
|
||||
* ↓ Recv3
|
||||
* R6(ek_r, prev) "pending"
|
||||
*
|
||||
* Corrupt can consume any R1..R6.
|
||||
*
|
||||
* Each R_i fact has EXACTLY ONE source rule.
|
||||
* Source analysis: zero branching. Proof search: linear.
|
||||
*/
|
||||
|
||||
restriction Once_R:
|
||||
"All #i #j. InitR() @i & InitR() @j ==> #i = #j"
|
||||
|
||||
/* Init: ek_r from KEX, no previous epoch key */
|
||||
rule Init_R:
|
||||
[ Fr(~ek) ]
|
||||
--[ InitR() ]->
|
||||
[ R1(~ek, 'nil') ]
|
||||
|
||||
/* Recv steps: new ek_r, old ek_r → prev */
|
||||
rule Recv1:
|
||||
[ R1(ek_r, prev), Fr(~ek) ]
|
||||
--[ Recv(~ek) ]->
|
||||
[ R2(~ek, ek_r) ]
|
||||
|
||||
rule Adv1:
|
||||
[ R2(ek_r, prev) ]
|
||||
--[ Adv() ]->
|
||||
[ R3(ek_r, prev) ]
|
||||
|
||||
rule Recv2:
|
||||
[ R3(ek_r, prev), Fr(~ek) ]
|
||||
--[ Recv(~ek) ]->
|
||||
[ R4(~ek, ek_r) ]
|
||||
|
||||
rule Adv2:
|
||||
[ R4(ek_r, prev) ]
|
||||
--[ Adv() ]->
|
||||
[ R5(ek_r, prev) ]
|
||||
|
||||
rule Recv3:
|
||||
[ R5(ek_r, prev), Fr(~ek) ]
|
||||
--[ Recv(~ek) ]->
|
||||
[ R6(~ek, ek_r) ]
|
||||
|
||||
/* Consuming corruption: reveals ek_r and prev, terminates session */
|
||||
rule Corrupt_R1: [ R1(ek_r, prev) ] --[ CorruptR(), RevealedR(ek_r), RevealedR(prev) ]-> [ ]
|
||||
rule Corrupt_R2: [ R2(ek_r, prev) ] --[ CorruptR(), RevealedR(ek_r), RevealedR(prev) ]-> [ ]
|
||||
rule Corrupt_R3: [ R3(ek_r, prev) ] --[ CorruptR(), RevealedR(ek_r), RevealedR(prev) ]-> [ ]
|
||||
rule Corrupt_R4: [ R4(ek_r, prev) ] --[ CorruptR(), RevealedR(ek_r), RevealedR(prev) ]-> [ ]
|
||||
rule Corrupt_R5: [ R5(ek_r, prev) ] --[ CorruptR(), RevealedR(ek_r), RevealedR(prev) ]-> [ ]
|
||||
rule Corrupt_R6: [ R6(ek_r, prev) ] --[ CorruptR(), RevealedR(ek_r), RevealedR(prev) ]-> [ ]
|
||||
|
||||
/* Non-consuming observation: reveals ek_r and prev, session continues (PCS) */
|
||||
rule Observe_R1: [ R1(ek,p) ] --[ ObserveR(), ObservedR(ek), ObservedR(p) ]-> [ R1(ek,p) ]
|
||||
rule Observe_R2: [ R2(ek,p) ] --[ ObserveR(), ObservedR(ek), ObservedR(p) ]-> [ R2(ek,p) ]
|
||||
rule Observe_R3: [ R3(ek,p) ] --[ ObserveR(), ObservedR(ek), ObservedR(p) ]-> [ R3(ek,p) ]
|
||||
rule Observe_R4: [ R4(ek,p) ] --[ ObserveR(), ObservedR(ek), ObservedR(p) ]-> [ R4(ek,p) ]
|
||||
rule Observe_R5: [ R5(ek,p) ] --[ ObserveR(), ObservedR(ek), ObservedR(p) ]-> [ R5(ek,p) ]
|
||||
rule Observe_R6: [ R6(ek,p) ] --[ ObserveR(), ObservedR(ek), ObservedR(p) ]-> [ R6(ek,p) ]
|
||||
|
||||
restriction Once_ObserveR:
|
||||
"All #i #j. ObserveR() @i & ObserveR() @j ==> #i = #j"
|
||||
|
||||
|
||||
/* Recv lemmas */
|
||||
|
||||
lemma recv_sanity:
|
||||
exists-trace
|
||||
"Ex ek1 ek2 #i #j. Recv(ek1) @i & Recv(ek2) @j & i < j"
|
||||
|
||||
/* Theorem 4b part 1 (1 step): FALSIFIED
|
||||
* After 1 subsequent Recv, old ek_r is in prev — revealed on corrupt. */
|
||||
lemma recv_fs_1step:
|
||||
"All ek ek2 #i #j #c.
|
||||
Recv(ek) @i & Recv(ek2) @j & CorruptR() @c &
|
||||
i < j & j < c
|
||||
==> not (Ex #r. RevealedR(ek) @r)"
|
||||
|
||||
/* Theorem 4b part 2 (2 steps): VERIFIED
|
||||
* After 2 subsequent Recvs, prev has been overwritten — old ek_r gone. */
|
||||
lemma recv_fs_2step:
|
||||
"All ek ek2 ek3 #i #j #k #c.
|
||||
Recv(ek) @i & Recv(ek2) @j & Recv(ek3) @k & CorruptR() @c &
|
||||
i < j & j < k & k < c
|
||||
==> not (Ex #r. RevealedR(ek) @r)"
|
||||
|
||||
// Consuming corruption terminates the session: no Recv can follow CorruptR.
|
||||
lemma recv_corrupt_terminates:
|
||||
"All ek #r #c. Recv(ek) @r & CorruptR() @c ==> r < c"
|
||||
|
||||
// PCS (recv side, ABSTRACT MODEL ONLY): after non-consuming observation,
|
||||
// one fresh recv step produces an epoch key the adversary never observed.
|
||||
// NOTE: This is an artifact of the Fr()-based abstraction, NOT a Theorem 5
|
||||
// result. In the real protocol (see LO_Ratchet_PCS.spthy), recv-only PCS
|
||||
// is NOT achieved — the adversary holds sk_s from the compromise and can
|
||||
// derive ss from the peer's ciphertext. Real PCS requires a direction
|
||||
// change (send after recv). See §9.2 worked trace.
|
||||
lemma recv_pcs:
|
||||
"All ek_new #obs #recv.
|
||||
ObserveR() @obs &
|
||||
Recv(ek_new) @recv & obs < recv
|
||||
==> not (Ex #r. ObservedR(ek_new) @r)"
|
||||
|
||||
end
|
||||
Loading…
Add table
Add a link
Reference in a new issue