108 lines
3.1 KiB
Text
108 lines
3.1 KiB
Text
theory LO_AntiReflection
|
|
begin
|
|
|
|
/*
|
|
* LO-Ratchet Anti-Reflection (Theorem 12)
|
|
* ========================================
|
|
*
|
|
* A message encrypted by A for B cannot be reflected back to A as if
|
|
* it were from B. The AAD uses direction-dependent fingerprint ordering:
|
|
* A→B: AAD = "lo-dm-v1" ‖ fp_A ‖ fp_B ‖ Encode(H)
|
|
* B→A: AAD = "lo-dm-v1" ‖ fp_B ‖ fp_A ‖ Encode(H)
|
|
*
|
|
* Since fp_A ≠ fp_B (invariant h), the AAD differs between directions,
|
|
* and AEAD tag verification fails on reflected messages.
|
|
*
|
|
* §9.9 known pitfall: a model using canonical (sorted) fingerprint
|
|
* ordering would NOT detect reflection — the AAD would be identical
|
|
* in both directions. This model preserves sender-first ordering.
|
|
*
|
|
* EXPECTED RESULTS:
|
|
* Reflection_Sanity: VERIFIED
|
|
* Theorem12_Anti_Reflection: VERIFIED
|
|
*/
|
|
|
|
builtins: hashing
|
|
|
|
// AEAD abstraction
|
|
functions: aead_enc/4, aead_verify/4, accept/0
|
|
equations:
|
|
aead_verify(k, n, aad, aead_enc(k, n, m, aad)) = accept()
|
|
|
|
// Constant-time equality
|
|
restriction Eq:
|
|
"All x y #i. Eq(x,y) @i ==> x = y"
|
|
|
|
// §5.1 invariant (h): local_fp ≠ remote_fp
|
|
restriction Neq:
|
|
"All x y #i. Neq(x,y) @i ==> not (x = y)"
|
|
|
|
|
|
/* ================= SESSION SETUP ================= */
|
|
|
|
rule Session_Setup:
|
|
[ Fr(~mk), Fr(~n) ]
|
|
--[ SessionSetup($A, $B, ~mk),
|
|
Neq($A, $B) ]->
|
|
[ !SessionKey($A, $B, ~mk),
|
|
SendState($A, $B, ~mk, ~n) ]
|
|
|
|
|
|
/* ================= SEND / RECEIVE (sender-first AAD ordering) ================= */
|
|
|
|
// A encrypts a message for B
|
|
// AAD = fp_sender ‖ fp_recipient ‖ header
|
|
rule Send_A_to_B:
|
|
let
|
|
aad = <'lo-dm-v1', $A, $B, ~header>
|
|
c = aead_enc(mk, n, ~m, aad)
|
|
in
|
|
[ SendState($A, $B, mk, n), Fr(~m), Fr(~header) ]
|
|
--[ Sent($A, $B, c, n) ]->
|
|
[ Out(<c, ~header, n>) ]
|
|
|
|
// B decrypts a message from A
|
|
// B reconstructs AAD with sender=A, recipient=B
|
|
rule Recv_B_from_A:
|
|
let
|
|
aad = <'lo-dm-v1', $A, $B, header>
|
|
in
|
|
[ !SessionKey($A, $B, mk), In(<c, header, n>) ]
|
|
--[ Eq(aead_verify(mk, n, aad, c), accept()),
|
|
Received($B, $A, c) ]->
|
|
[ ]
|
|
|
|
// A decrypts a "message from B" (potential reflection target)
|
|
// A reconstructs AAD with sender=B, recipient=A — REVERSED order
|
|
rule Recv_A_from_B:
|
|
let
|
|
aad = <'lo-dm-v1', $B, $A, header>
|
|
in
|
|
[ !SessionKey($A, $B, mk), In(<c, header, n>) ]
|
|
--[ Eq(aead_verify(mk, n, aad, c), accept()),
|
|
Received($A, $B, c) ]->
|
|
[ ]
|
|
|
|
|
|
/* ================= LEMMAS ================= */
|
|
|
|
// Sanity: honest A→B message exchange works
|
|
lemma Reflection_Sanity:
|
|
exists-trace
|
|
"Ex A B c n #i #j.
|
|
Sent(A, B, c, n) @i &
|
|
Received(B, A, c) @j"
|
|
|
|
// Theorem 12: A message sent by A→B cannot be accepted by A as B→A.
|
|
// The adversary captures A's ciphertext and replays it to A's receive
|
|
// rule. AEAD verification fails because the AAD differs:
|
|
// Sent: AAD = <"lo-dm-v1", A, B, header>
|
|
// Received: AAD = <"lo-dm-v1", B, A, header>
|
|
// Since A ≠ B (invariant h), these are distinct terms.
|
|
lemma Theorem12_Anti_Reflection:
|
|
"All A B c n #i #j.
|
|
Sent(A, B, c, n) @i &
|
|
Received(A, B, c) @j
|
|
==> F"
|
|
|
|
end
|