diff options
Diffstat (limited to 'wireguard.m4')
| -rw-r--r-- | wireguard.m4 | 168 |
1 files changed, 84 insertions, 84 deletions
diff --git a/wireguard.m4 b/wireguard.m4 index 98f0a2f..661ea06 100644 --- a/wireguard.m4 +++ b/wireguard.m4 @@ -21,12 +21,12 @@ builtins: hashing, diffie-hellman /* We're not going to model the nonce in the aead, since it's always 0 in the handshake. */ functions: aead/3, decrypt/2, verify/3, true/0 /* The plaintext can be recovered with the key */ -equations: decrypt(aead(k,p,a),k) = p +equations: decrypt(aead(k, p, a), k) = p /* The authentication can be checked with the key and AAD */ -equations: verify(aead(k,p,a),a,k) = true +equations: verify(aead(k, p, a), a, k) = true -restriction Eq_testing: "All x y #i. Eq(x,y) @ i ==> x = y" -restriction InEq_testing: "All x y #i. InEq(x,y) @ i ==> not(x = y)" +restriction Eq_testing: "All x y #i. Eq(x, y) @ i ==> x = y" +restriction InEq_testing: "All x y #i. InEq(x, y) @ i ==> not(x = y)" /* Uncomment these to prevent any adversary message modifications, * useful for checking exists-trace lemmas and making sure messsages @@ -50,7 +50,7 @@ dnl define(State, L_State($*)) /* Pre-established trust relationships */ restriction pairings_unique: "All id id2 ka kb #i #j. - Paired(id,ka,kb) @ i & Paired(id2,ka,kb) @ j + Paired(id, ka, kb) @ i & Paired(id2, ka, kb) @ j ==> #i = #j" /* Keygen is separate from pairing to allow keys to be paired @@ -95,8 +95,8 @@ rule AddPublicKey: * allows tamarin to immediately bind the keys back * to this initial pairing rule. The fresh ~id is used * to identify this pairing. */ - State(~id,'no_message_state') - , !StateInvariants(~id,~psk,~ltkA,pkB,pkB^~ltkA) + State(~id, 'no_message_state') + , !StateInvariants(~id, ~psk, ~ltkA, pkB, pkB^~ltkA) ] /* === Message Rules === */ @@ -107,29 +107,29 @@ rule Handshake_Init: eisr = pkR^~ekI /* Constructing the init message m1: */ cii = h('noise') - hii = h(<cii,'id',pkR,pekI>) - ci0 = h(<cii,pekI,'1'>) - ci1 = h(<ci0,eisr,'1'>) - ki1 = h(<ci0,eisr,'2'>) - astat = aead(ki1,<pkI,~pkISurrogate>,hii) - hi0 = h(<hii,astat>) - ci2 = h(<ci1,sisr,'1'>) - ki2 = h(<ci1,sisr,'2'>) - ats = aead(ki2,$ts,hi0) - hi1 = h(<hi0,ats>) - m1 = <'1',~sidI,pekI,astat,ats,$mac1,$mac2> in //NOTE: MACs are currently not modeled + hii = h(<cii, 'id', pkR, pekI>) + ci0 = h(<cii, pekI, '1'>) + ci1 = h(<ci0, eisr, '1'>) + ki1 = h(<ci0, eisr, '2'>) + astat = aead(ki1, <pkI, ~pkISurrogate>, hii) + hi0 = h(<hii, astat>) + ci2 = h(<ci1, sisr, '1'>) + ki2 = h(<ci1, sisr, '2'>) + ats = aead(ki2, $ts, hi0) + hi1 = h(<hi0, ats>) + m1 = <'1', ~sidI, pekI, astat, ats, $mac1, $mac2> in //NOTE: MACs are currently not modeled [ /* Init can be triggered at any time, even when currently performing * another role or on another stage. This could happen e.g. because of a timeout. * As such we bind the previous state as 'anything' and discard it. */ - State(~id,anything) - , !StateInvariants(~id,~psk,~ltkI,pkR,sisr) + State(~id, anything) + , !StateInvariants(~id, ~psk, ~ltkI, pkR, sisr) , Fr(~sidI) , Fr(~ekI) /* The pkISurrogate is used later to approximate identity hiding. */ , Fr(~pkISurrogate) ]--> [ /* We cache DH sisr to reduce variant precomputation time for tamarin. */ - State(~id,<'init',~sidI,~ekI,ci2,ki2,hi1>) + State(~id, <'init', ~sidI, ~ekI, ci2, ki2, hi1>) , !EphKeytoReveal(~ekI) , Out(m1) ] @@ -142,41 +142,41 @@ rule Handshake_Resp: sier = pkI^~ekR /* Reconstructing what should be in m1: */ cri = h('noise') - hri = h(<cri,'id',pkR,pekI>) - cr0 = h(<cri,pekI,'1'>) - cr1 = h(<cr0,eisr,'1'>) - kr1 = h(<cr0,eisr,'2'>) - astat = aead(kr1,<pkI,pkISurrogate>,hri) - hr0 = h(<hri,astat>) - cr2 = h(<cr1,sisr,'1'>) - kr2 = h(<cr1,sisr,'2'>) - ats = aead(kr2,$ts,hr0) - hr1 = h(<hr0,ats>) - m1 = <'1',sidI,pekI,astat,ats,$mac1,$mac2> //NOTE: MACs are currently not modeled + hri = h(<cri, 'id', pkR, pekI>) + cr0 = h(<cri, pekI, '1'>) + cr1 = h(<cr0, eisr, '1'>) + kr1 = h(<cr0, eisr, '2'>) + astat = aead(kr1, <pkI, pkISurrogate>, hri) + hr0 = h(<hri, astat>) + cr2 = h(<cr1, sisr, '1'>) + kr2 = h(<cr1, sisr, '2'>) + ats = aead(kr2, $ts, hr0) + hr1 = h(<hr0, ats>) + m1 = <'1', sidI, pekI, astat, ats, $mac1, $mac2> //NOTE: MACs are currently not modeled /* Constructing the response message m2: */ - cr3 = h(<cr2,pekR,'1'>) - hr2 = h(<hr1,pekR>) - cr4 = h(<cr3,eier,'1'>) - cr5 = h(<cr4,sier,'1'>) - cr6 = h(<cr5,~psk,'1'>) - hrt = h(<cr5,~psk,'2'>) - kr6 = h(<cr5,~psk,'3'>) - hr3 = h(<hr2,hrt>) - aempt = aead(kr6,'e',hr3) - hr4 = h(<hr3,aempt>) - m2 = <'2',sidI,~sidR,pekR,aempt,$mac1,$mac2> in //NOTE: MACs are currently not modeled - [ State(~id,anything) - , !StateInvariants(~id,~psk,~ltkR,pkI,sisr) + cr3 = h(<cr2, pekR, '1'>) + hr2 = h(<hr1, pekR>) + cr4 = h(<cr3, eier, '1'>) + cr5 = h(<cr4, sier, '1'>) + cr6 = h(<cr5, ~psk, '1'>) + hrt = h(<cr5, ~psk, '2'>) + kr6 = h(<cr5, ~psk, '3'>) + hr3 = h(<hr2, hrt>) + aempt = aead(kr6, 'e', hr3) + hr4 = h(<hr3, aempt>) + m2 = <'2', sidI, ~sidR, pekR, aempt, $mac1, $mac2> in //NOTE: MACs are currently not modeled + [ State(~id, anything) + , !StateInvariants(~id, ~psk, ~ltkR, pkI, sisr) , Fr(~ekR) , Fr(~sidR) , In(m1) ]--[ /* In the real protocol, this isn't actually cr6, but is rather derived from it * via some more hashing, but it doesn't make a difference here. */ - RKeys(<pkI,pkR,pekI,pekR,~psk,cr6>) + RKeys(<pkI, pkR, pekI, pekR, ~psk, cr6>) , Identity_Surrogate(pkISurrogate) ]-> - [ State(~id,<'transport_unconfirmed',~sidR,pekI,pekR,cr6>) + [ State(~id, <'transport_unconfirmed', ~sidR, pekI, pekR, cr6>) , !EphKeytoReveal(~ekR) , Out(m2) ] @@ -187,29 +187,29 @@ rule Handshake_Complete: eier = pekR^~ekI sier = pekR^~ltkI /* Reconstruct what should be in m2: */ - ci3 = h(<ci2,pekR,'1'>) - hi2 = h(<hi1,pekR>) - ci4 = h(<ci3,eier,'1'>) - ci5 = h(<ci4,sier,'1'>) - ci6 = h(<ci5,~psk,'1'>) - hit = h(<ci5,~psk,'2'>) - ki6 = h(<ci5,~psk,'3'>) - hi3 = h(<hi2,hit>) - aempt = aead(ki6,'e',hi3) - hi4 = h(<hi3,aempt>) - m2 = <'2',sidI,sidR,pekR,aempt,$mac1,$mac2> + ci3 = h(<ci2, pekR, '1'>) + hi2 = h(<hi1, pekR>) + ci4 = h(<ci3, eier, '1'>) + ci5 = h(<ci4, sier, '1'>) + ci6 = h(<ci5, ~psk, '1'>) + hit = h(<ci5, ~psk, '2'>) + ki6 = h(<ci5, ~psk, '3'>) + hi3 = h(<hi2, hit>) + aempt = aead(ki6, 'e', hi3) + hi4 = h(<hi3, aempt>) + m2 = <'2', sidI, sidR, pekR, aempt, $mac1, $mac2> /* We assume the first transport message is 'as weak as possible', that is all values * in it are public except the key used to encrypt. */ - mtr = <'4',sidR,aead(ci6,'message','0')> in - [ State(~id,<'init',sidI,~ekI,ci2,ki2,hi1>) - , !StateInvariants(~id,~psk,~ltkI,pkR,sisr) + mtr = <'4', sidR, aead(ci6, 'message', '0')> in + [ State(~id, <'init', sidI, ~ekI, ci2, ki2, hi1>) + , !StateInvariants(~id, ~psk, ~ltkI, pkR, sisr) , In(m2) ]--[ /* In the real protocol, this isn't actually ci6, but is rather derived from it * via some more hashing, but it doesn't make a difference here. */ - IKeys(<pkI,pkR,pekI,pekR,~psk,ci6>) + IKeys(<pkI, pkR, pekI, pekR, ~psk, ci6>) ]-> - [ State(~id,<'transport',sidI,ci6>) + [ State(~id, <'transport', sidI, ci6>) , Out(mtr) ] @@ -221,17 +221,17 @@ rule Handshake_Complete: * with the transport key I just set up'. */ rule R_ConfirmedTransportMessage: - let mtr = <'4',sid,data> in - [ State(~id,<'transport_unconfirmed',sidR,pekI,pekR,cr>) - , !StateInvariants(~id,~psk,~ltkR,pkI,sisr) + let mtr = <'4', sid, data> in + [ State(~id, <'transport_unconfirmed', sidR, pekI, pekR, cr>) + , !StateInvariants(~id, ~psk, ~ltkR, pkI, sisr) , In(mtr) ]--[ - RConfirm(<pkI,'g'^~ltkR,pekI,pekR,~psk,cr>) + RConfirm(<pkI, 'g'^~ltkR, pekI, pekR, ~psk, cr>) //We manually verify this instead of the typical recomputation, since //morally R may not know the contents of 'data'. - , Eq(verify(data,'0',cr),true) + , Eq(verify(data, '0', cr), true) ]-> - [ State(~id,<'transport',sidR,cr>) ] + [ State(~id, <'transport', sidR, cr>) ] /* === Session Traces === * @@ -239,15 +239,15 @@ rule R_ConfirmedTransportMessage: lemma exists_session: exists-trace "Ex pki pkr peki pekr psk ck #i #j. - IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i - & RConfirm(<pki,pkr,peki,pekr,psk,ck>) @ j & #i < #j" + IKeys(<pki, pkr, peki, pekr, psk, ck>) @ i + & RConfirm(<pki, pkr, peki, pekr, psk, ck>) @ j & #i < #j" /* There are only three numbers, 0, 1, and infinity. So 2 == infinity */ lemma exists_two_sessions: exists-trace "Ex pki pkr sesskeys sesskeys2 #i #j #i2 #j2. - IKeys(<pki,pkr,sesskeys>) @ i - & RConfirm(<pki,pkr,sesskeys>) @ j & #i < #j - & IKeys(<pki,pkr,sesskeys2>) @ i2 & RConfirm(<pki,pkr,sesskeys2>) @ j2 & #i2 < #j2 + IKeys(<pki, pkr, sesskeys>) @ i + & RConfirm(<pki, pkr, sesskeys>) @ j & #i < #j + & IKeys(<pki, pkr, sesskeys2>) @ i2 & RConfirm(<pki, pkr, sesskeys2>) @ j2 & #i2 < #j2 & #i < #i2 & not(sesskeys = sesskeys2)" @@ -256,9 +256,9 @@ lemma exists_two_sessions: exists-trace lemma I_disagreement_implies_Sr_or_SiEi_compromise_and_PSK_compromise[reuse]: "All pki pkr peki pekr psk ck #i. /* If I believes they have completed a handshake with R */ - IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i + IKeys(<pki, pkr, peki, pekr, psk, ck>) @ i /* but R doesn't have a matching session */ - & not(Ex #j. #j < #i & RKeys(<pki,pkr,peki,pekr,psk,ck>) @ j) + & not(Ex #j. #j < #i & RKeys(<pki, pkr, peki, pekr, psk, ck>) @ j) ==> /* Then the PSK was compromised (or not in use) and */ (Ex #j. Reveal_PSK(psk) @ j & #j < #i) & ( /* either R's static was compromised */ @@ -270,9 +270,9 @@ lemma I_disagreement_implies_Sr_or_SiEi_compromise_and_PSK_compromise[reuse]: lemma R_disagreement_implies_Si_or_SrEr_compromise_and_PSK_compromise[reuse]: "All pki pkr peki pekr psk ck #i. /* If R believes they have a confirmed session with I */ - RConfirm(<pki,pkr,peki,pekr,psk,ck>) @ i + RConfirm(<pki, pkr, peki, pekr, psk, ck>) @ i /* but I doesn't have a matching session */ - & not(Ex #j. #j < #i & IKeys(<pki,pkr,peki,pekr,psk,ck>) @ j) + & not(Ex #j. #j < #i & IKeys(<pki, pkr, peki, pekr, psk, ck>) @ j) ==> /* Then the PSK was compromised (or not in use) and */ (Ex #j. Reveal_PSK(psk) @ j & #j < #i) & ( /* either I's static was compromised */ @@ -286,18 +286,18 @@ lemma session_uniqueness: * This follows from I and R generating random ephemeral values. Note that this could be violated if the * RNG can be controlled instead of just revealed, which we do not model. */ "(All pki pkr peki pekr psk ck #i. - IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i - ==> not(Ex peki2 pekr2 #k. IKeys(<pki,pkr,peki2,pekr2,psk,ck>) @ k & not(#k = #i))) + IKeys(<pki, pkr, peki, pekr, psk, ck>) @ i + ==> not(Ex peki2 pekr2 #k. IKeys(<pki, pkr, peki2, pekr2, psk, ck>) @ k & not(#k = #i))) &(All pki pkr peki pekr psk ck #i. - RConfirm(<pki,pkr,peki,pekr,psk,ck>) @ i - ==> not(Ex peki2 pekr2 psk2 #k. RConfirm(<pki,pkr,peki2,pekr2,psk2,ck>) @ k & not(#k = #i)))" + RConfirm(<pki, pkr, peki, pekr, psk, ck>) @ i + ==> not(Ex peki2 pekr2 psk2 #k. RConfirm(<pki, pkr, peki2, pekr2, psk2, ck>) @ k & not(#k = #i)))" /* === Secrecy Properties === */ lemma key_secrecy[reuse]: "(All pki pkr peki pekr psk ck #i #i2. /* If I and R agree on keys */ - IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i & RKeys(<pki,pkr,peki,pekr,psk,ck>) @ i2 + IKeys(<pki, pkr, peki, pekr, psk, ck>) @ i & RKeys(<pki, pkr, peki, pekr, psk, ck>) @ i2 ==> /* Either the adversary doesn't know the keys */ not(Ex #j. K(ck) @ j) /* or the psk was compromised (or not in use) */ @@ -313,7 +313,7 @@ lemma identity_hiding: * same position as the public static. */ "All pki pkr peki pekr ck surrogate #i #j. /* If R received a handshake init with a particular identity surrogate */ - RKeys(<pki,pkr,peki,pekr,ck>) @ i & Identity_Surrogate(surrogate) @ i + RKeys(<pki, pkr, peki, pekr, ck>) @ i & Identity_Surrogate(surrogate) @ i /* And the adversary knows that surrogate for the identity */ & K(surrogate) @ j ==> /* Then the adversary compromised at least one of R's static, I's static, or I's ephemeral */ |