350 lines
10 KiB
Text
350 lines
10 KiB
Text
theory LO_NegativeTests
|
|
begin
|
|
|
|
/*
|
|
* Negative Tests (Expected Falsifications)
|
|
* =========================================
|
|
*
|
|
* Each lemma SHOULD be falsified. If any verifies, the model is
|
|
* over-constraining the adversary or making incorrect assumptions.
|
|
* These confirm the model correctly represents attack paths.
|
|
*
|
|
* ALL EXPECTED: FALSIFIED
|
|
*
|
|
* neg_auth_ik_corrupt: IK corruption → auth forged
|
|
* neg_auth_rng_corrupt: RNG corruption → auth forged
|
|
* neg_ratchet_no_fs_0step: Corrupt immediately → current ek revealed
|
|
* neg_ratchet_recv_1step: 1-step recv FS fails (prev_ek_r retains)
|
|
* neg_call_rk_plus_rng: rk + RNG corruption → call key derivable
|
|
* neg_stream_key_corrupt: Key corruption → forgery possible
|
|
* neg_reflect_self_session: Self-session → reflection succeeds
|
|
*/
|
|
|
|
builtins: hashing, signing, asymmetric-encryption
|
|
|
|
functions: kem_pk/1, kem_c/2, kem_ss/2, kem_decaps/2, mac/2
|
|
equations: kem_decaps(sk, kem_c(kem_pk(sk), r)) = r
|
|
|
|
functions: aead_enc/4, aead_verify/4, accept/0
|
|
equations: aead_verify(k, n, aad, aead_enc(k, n, m, aad)) = accept()
|
|
|
|
functions: kdf_call_a/3
|
|
|
|
restriction Eq:
|
|
"All x y #i. Eq(x,y) @i ==> x = y"
|
|
|
|
|
|
/* =========== NEG 1-2: LO-Auth corruption =========== */
|
|
|
|
rule NAuth_GenIK:
|
|
[ Fr(~sk) ] --[ NAuthGen($P) ]->
|
|
[ !NAuthLtk($P, ~sk), !NAuthPk($P, kem_pk(~sk)), Out(kem_pk(~sk)) ]
|
|
|
|
rule NAuth_CorruptIK:
|
|
[ !NAuthLtk($P, sk) ] --[ NAuthCorruptIK($P) ]-> [ Out(sk) ]
|
|
|
|
rule NAuth_CorruptRNG:
|
|
[ !NAuthRNG($S, r) ] --[ NAuthCorruptRNG($S, r) ]-> [ Out(r) ]
|
|
|
|
rule NAuth_Challenge:
|
|
let c = kem_c(pk_c, ~r)
|
|
ss = kem_ss(pk_c, ~r)
|
|
token = mac(ss, 'lo-auth-v1')
|
|
in
|
|
[ !NAuthPk($C, pk_c), Fr(~r) ]
|
|
--[ NAuthChallenge($S, $C, ~r, token) ]->
|
|
[ NAuthPending($S, $C, token), Out(c), !NAuthRNG($S, ~r) ]
|
|
|
|
rule NAuth_Verify:
|
|
[ NAuthPending($S, $C, token), In(proof) ]
|
|
--[ Eq(token, proof), NAuthAccepted($S, $C) ]->
|
|
[ ]
|
|
|
|
// NEG 1: IK corruption defeats auth
|
|
lemma neg_auth_ik_corrupt:
|
|
"All S C #v.
|
|
NAuthAccepted(S, C) @v
|
|
==> not (Ex #j. NAuthCorruptIK(C) @j)"
|
|
|
|
// NEG 2: RNG corruption defeats auth
|
|
lemma neg_auth_rng_corrupt:
|
|
"All S C r token #ch #v.
|
|
NAuthChallenge(S, C, r, token) @ch &
|
|
NAuthAccepted(S, C) @v
|
|
==> not (Ex #j. NAuthCorruptRNG(S, r) @j)"
|
|
|
|
|
|
/* =========== NEG 3-4: LO-Ratchet FS boundaries =========== */
|
|
|
|
restriction NRatchetOnce:
|
|
"All #i #j. NRInit() @i & NRInit() @j ==> #i = #j"
|
|
|
|
rule NR_Init:
|
|
[ Fr(~ek) ] --[ NRInit() ]-> [ NR1(~ek, 'nil') ]
|
|
|
|
rule NR_Recv1:
|
|
[ NR1(ek_r, prev), Fr(~ek) ] --[ NRRecv(~ek) ]-> [ NR2(~ek, ek_r) ]
|
|
|
|
rule NR_Adv1:
|
|
[ NR2(ek_r, prev) ] --> [ NR3(ek_r, prev) ]
|
|
|
|
rule NR_Recv2:
|
|
[ NR3(ek_r, prev), Fr(~ek) ] --[ NRRecv(~ek) ]-> [ NR4(~ek, ek_r) ]
|
|
|
|
rule NR_Corrupt:
|
|
[ NR1(ek, p) ] --[ NRCorrupt(), NRRevealed(ek) ]-> [ ]
|
|
|
|
rule NR_Corrupt2:
|
|
[ NR2(ek, p) ] --[ NRCorrupt(), NRRevealed(ek), NRRevealed(p) ]-> [ ]
|
|
|
|
rule NR_Corrupt3:
|
|
[ NR3(ek, p) ] --[ NRCorrupt(), NRRevealed(ek), NRRevealed(p) ]-> [ ]
|
|
|
|
rule NR_Corrupt4:
|
|
[ NR4(ek, p) ] --[ NRCorrupt(), NRRevealed(ek), NRRevealed(p) ]-> [ ]
|
|
|
|
// NEG 3: Corrupt with 0 subsequent recvs → current ek revealed
|
|
lemma neg_ratchet_no_fs_0step:
|
|
"All ek #r #c.
|
|
NRRecv(ek) @r & NRCorrupt() @c & r < c
|
|
==> not (Ex #rev. NRRevealed(ek) @rev)"
|
|
|
|
// NEG 4: Same as recv_fs_1step — 1 subsequent recv, ek still in prev
|
|
lemma neg_ratchet_recv_1step:
|
|
"All ek ek2 #i #j #c.
|
|
NRRecv(ek) @i & NRRecv(ek2) @j & NRCorrupt() @c &
|
|
i < j & j < c
|
|
==> not (Ex #r. NRRevealed(ek) @r)"
|
|
|
|
|
|
/* =========== NEG 5: LO-Call rk+RNG corruption =========== */
|
|
|
|
restriction NCallNeq:
|
|
"All I R rk #i. NCallSetup(I, R, rk) @i ==> not (I = R)"
|
|
|
|
rule NCall_Setup:
|
|
[ Fr(~rk) ] --[ NCallSetup($I, $R, ~rk) ]-> [ !NCallRK($I, $R, ~rk) ]
|
|
|
|
rule NCall_CorruptRK:
|
|
[ !NCallRK($I, $R, rk) ] --[ NCallCorruptRK($I, $R) ]-> [ Out(rk) ]
|
|
|
|
rule NCall_CorruptRNG:
|
|
[ !NCallRNG($P, r) ] --[ NCallCorruptRNG($P, r) ]-> [ Out(r) ]
|
|
|
|
// Step 1: initiator generates pk_eph (public), sk_eph
|
|
// Step 2: peer encapsulates to pk_eph with randomness r_eph
|
|
// Corrupt(RNG, initiator, t1) reveals sk_eph
|
|
// Corrupt(RNG, peer, t2) reveals r_eph
|
|
rule NCall_Derive:
|
|
let pk_eph = kem_pk(~sk_eph)
|
|
ss = kem_ss(pk_eph, ~r_eph)
|
|
ka = kdf_call_a(rk, ss, ~cid)
|
|
in
|
|
[ !NCallRK($I, $R, rk), Fr(~sk_eph), Fr(~r_eph), Fr(~cid) ]
|
|
--[ NCallDerived($R, ka) ]->
|
|
[ Out(pk_eph),
|
|
Out(~cid),
|
|
Out(kem_c(pk_eph, ~r_eph)),
|
|
!NCallRNG($I, ~sk_eph),
|
|
!NCallRNG($R, ~r_eph) ]
|
|
|
|
// NEG 5: Both rk and ephemeral RNG corrupted → call key derivable
|
|
lemma neg_call_rk_plus_rng:
|
|
"All R ka #d.
|
|
NCallDerived(R, ka) @d
|
|
==> not (Ex #k. K(ka) @k)"
|
|
|
|
|
|
/* =========== NEG 6: LO-Stream key corruption =========== */
|
|
|
|
functions: nonce_n/2, aad_n/2
|
|
|
|
rule NS_Init:
|
|
[ Fr(~key), Fr(~bn) ]
|
|
--[ NSInit(~key, ~bn) ]->
|
|
[ !NSSP(~key, ~bn), NSEnc(~key, ~bn, '0'), Out(~bn) ]
|
|
|
|
rule NS_CorruptKey:
|
|
[ !NSSP(key, bn) ] --[ NSCorrupt(key) ]-> [ Out(key) ]
|
|
|
|
rule NS_Enc:
|
|
let n = nonce_n(bn, idx)
|
|
aad = aad_n(bn, idx)
|
|
c = aead_enc(key, n, ~m, aad)
|
|
in
|
|
[ NSEnc(key, bn, idx), Fr(~m) ]
|
|
--[ NSEncrypted(bn, idx, c) ]->
|
|
[ Out(<c, idx>) ]
|
|
|
|
// Adversary decrypts with corrupted key
|
|
rule NS_Dec_Adversary:
|
|
let n = nonce_n(bn, idx)
|
|
aad = aad_n(bn, idx)
|
|
in
|
|
[ !NSSP(key, bn), In(<c, idx>) ]
|
|
--[ Eq(aead_verify(key, n, aad, c), accept()),
|
|
NSDecrypted(bn, idx) ]->
|
|
[ ]
|
|
|
|
// NEG 6: Key corruption → adversary can get ciphertext accepted
|
|
// (trivially true since adversary holds key and can replay honest ciphertexts)
|
|
lemma neg_stream_key_corrupt:
|
|
"All bn idx #d.
|
|
NSDecrypted(bn, idx) @d
|
|
==> not (Ex #j key. NSCorrupt(key) @j)"
|
|
|
|
|
|
/* =========== NEG 7: Anti-reflection without invariant (h) =========== */
|
|
|
|
rule NRefl_Setup:
|
|
[ Fr(~mk), Fr(~n) ]
|
|
--[ NReflSetup($A, $B, ~mk) ]->
|
|
[ !NReflKey($A, $B, ~mk), NReflSend($A, $B, ~mk, ~n) ]
|
|
|
|
// NOTE: No Neq restriction — self-sessions allowed!
|
|
|
|
rule NRefl_Send:
|
|
let aad = <'lo-dm-v1', $A, $B, ~hdr>
|
|
c = aead_enc(mk, n, ~m, aad)
|
|
in
|
|
[ NReflSend($A, $B, mk, n), Fr(~m), Fr(~hdr) ]
|
|
--[ NReflSent($A, $B, c) ]->
|
|
[ Out(<c, ~hdr, n>) ]
|
|
|
|
rule NRefl_RecvReflected:
|
|
let aad = <'lo-dm-v1', $B, $A, header>
|
|
in
|
|
[ !NReflKey($A, $B, mk), In(<c, header, n>) ]
|
|
--[ Eq(aead_verify(mk, n, aad, c), accept()),
|
|
NReflAccepted($A, $B, c) ]->
|
|
[ ]
|
|
|
|
// NEG 7: Without invariant (h), self-session allows reflection
|
|
// A sends to A, reflected back — AAD matches because fp order is same
|
|
lemma neg_reflect_self_session:
|
|
"All A c #i #j.
|
|
NReflSent(A, A, c) @i &
|
|
NReflAccepted(A, A, c) @j
|
|
==> F"
|
|
|
|
|
|
/* =========================================================
|
|
* 8. LO-KEX: OPK-absent weakens secrecy threshold (2-key)
|
|
* ========================================================= */
|
|
|
|
// KEX without OPK: IKM = ss_IK ‖ ss_SPK only.
|
|
// Corruption of IK + SPK alone suffices to derive rk.
|
|
|
|
// Reuse KEX IK generation (produces !KEXLtk and !KEXPk for NKEX2 rules)
|
|
rule NKEX2_GenIK:
|
|
[ Fr(~sk) ] --[ NKEX2_GenIK($P, ~sk) ]->
|
|
[ !KEXLtk($P, ~sk), !KEXPk($P, pk(~sk)), Out(pk(~sk)) ]
|
|
|
|
rule NKEX2_Publish:
|
|
let pk_SPK = pk(~sk_SPK)
|
|
pk_IK = pk(~sk_IK)
|
|
sig_SPK = sign(<'lo-spk-sig-v1', pk_SPK>, ~sk_IK)
|
|
in
|
|
[ !KEXLtk($B, ~sk_IK), Fr(~sk_SPK), Fr(~id_SPK) ]
|
|
--[ NKEX2_Publish($B, ~id_SPK) ]->
|
|
[ !NKEX2_SPK_Secret($B, ~id_SPK, ~sk_SPK),
|
|
!NKEX2_SPK_Pk($B, ~id_SPK, pk_SPK),
|
|
Out(<pk_IK, pk_SPK, ~id_SPK, sig_SPK>) ]
|
|
|
|
rule NKEX2_CorruptSPK:
|
|
[ !NKEX2_SPK_Secret($P, id, sk) ] --[ NKEX2_CorruptSPK($P, id) ]-> [ Out(sk) ]
|
|
|
|
rule NKEX2_Alice_NoOPK:
|
|
let pk_IK_A = pk(~sk_IK_A)
|
|
c_IK = aenc(~r_IK, pk_IK_B)
|
|
c_SPK = aenc(~r_SPK, pk_SPK_B)
|
|
ikm = <~r_IK, ~r_SPK>
|
|
rk = h(<ikm, 'rk'>)
|
|
in
|
|
[ !KEXLtk($A, ~sk_IK_A), !KEXPk($B, pk_IK_B),
|
|
!NKEX2_SPK_Pk($B, id_SPK, pk_SPK_B),
|
|
In(sig_SPK), Fr(~r_IK), Fr(~r_SPK) ]
|
|
--[ Eq(verify(sig_SPK, <'lo-spk-sig-v1', pk_SPK_B>, pk_IK_B), true),
|
|
NKEX2_Init($A, $B, rk, id_SPK) ]->
|
|
[ Out(<c_IK, c_SPK>) ]
|
|
|
|
rule NKEX2_CorruptIK:
|
|
[ !KEXLtk($P, sk) ] --[ NKEX2_CorruptIK($P) ]-> [ Out(sk) ]
|
|
|
|
// NEG 8: OPK-absent — IK + SPK corruption alone → adversary derives rk
|
|
lemma neg_kex_no_opk:
|
|
"All A B rk id_S #i.
|
|
NKEX2_Init(A, B, rk, id_S) @i
|
|
==> not (Ex #k. K(rk) @k)"
|
|
|
|
|
|
/* =========================================================
|
|
* 9. Ratchet: Duplicate message without recv_seen
|
|
* ========================================================= */
|
|
|
|
// Minimal ratchet with message counter but NO duplicate detection.
|
|
// An adversary replays a valid ciphertext → accepted twice.
|
|
|
|
rule NRDup_Init:
|
|
[ Fr(~ek) ] --[ NRDupInit() ]-> [ !NRDupKey(~ek) ]
|
|
|
|
restriction NRDupOnce:
|
|
"All #i #j. NRDupInit() @i & NRDupInit() @j ==> #i = #j"
|
|
|
|
functions: kdf_msg/2, nonce_dup/1
|
|
|
|
rule NRDup_Enc:
|
|
let mk = kdf_msg(ek, ~ctr)
|
|
n = nonce_dup(~ctr)
|
|
c = aead_enc(mk, n, ~m, 'aad')
|
|
in
|
|
[ !NRDupKey(ek), Fr(~ctr), Fr(~m) ]
|
|
--[ NRDupSent(~ctr, c) ]->
|
|
[ Out(<c, ~ctr>) ]
|
|
|
|
// Decrypt WITHOUT recv_seen — always accepts if AEAD passes
|
|
rule NRDup_Dec:
|
|
let mk = kdf_msg(ek, ctr)
|
|
n = nonce_dup(ctr)
|
|
in
|
|
[ !NRDupKey(ek), In(<c, ctr>) ]
|
|
--[ Eq(aead_verify(mk, n, 'aad', c), accept()),
|
|
NRDupAccepted(ctr, c) ]->
|
|
[ ]
|
|
|
|
// NEG 9: Without recv_seen, same ciphertext accepted twice
|
|
lemma neg_ratchet_duplicate:
|
|
"All ctr c #i #j.
|
|
NRDupAccepted(ctr, c) @i &
|
|
NRDupAccepted(ctr, c) @j
|
|
==> #i = #j"
|
|
|
|
|
|
/* =========================================================
|
|
* 10. Call: Self-session collapses role assignment
|
|
* ========================================================= */
|
|
|
|
// Without the local_fp != remote_fp guard, both parties get the
|
|
// same role — send/recv key separation collapses.
|
|
|
|
rule NCallSelf_Setup:
|
|
[ Fr(~rk) ] --[ NCallSelfSetup($A, $A, ~rk) ]->
|
|
[ !NCallSelfRK($A, $A, ~rk) ]
|
|
|
|
rule NCallSelf_Derive:
|
|
let ss = kem_ss(kem_pk(~sk_eph), ~r_eph)
|
|
// With fp_lo = fp_hi (same party), canonical ordering produces
|
|
// identical role assignment for both sides
|
|
ka = kdf_call_a(rk, ss, ~cid)
|
|
in
|
|
[ !NCallSelfRK($A, $A, rk), Fr(~sk_eph), Fr(~r_eph), Fr(~cid) ]
|
|
--[ NCallSelfDerived($A, ka) ]->
|
|
[ Out(kem_pk(~sk_eph)), Out(~cid), Out(kem_c(kem_pk(~sk_eph), ~r_eph)) ]
|
|
|
|
// NEG 10: Self-session is reachable (no guard prevents it)
|
|
// This confirms the guard is necessary — without it, A initiates a call with itself
|
|
lemma neg_call_self_session:
|
|
exists-trace
|
|
"Ex A ka #i. NCallSelfDerived(A, ka) @i"
|
|
|
|
end
|