diff options
-rw-r--r-- | wireguard.m4 | 75 |
1 files changed, 49 insertions, 26 deletions
diff --git a/wireguard.m4 b/wireguard.m4 index 1c9f537..27e8e3f 100644 --- a/wireguard.m4 +++ b/wireguard.m4 @@ -156,7 +156,7 @@ rule Handshake_Resp: ]--[ RKeys(<pkI,pkR,pekI,pekR,'nopsk',cr3>) //Not actually cr3, but derived from it. , RSessionID(sidI,~sidR) - , IIdentity(pkISurrogate) + , Identity_Surrogate(pkISurrogate) ]-> [ State(~id,'nopsk',<'transport_unconfirmed',~sidR,pekI,pekR,cr3>) //Efficiency hack, lets us make this high priority while making state low priority @@ -307,7 +307,7 @@ rule Handshake_RespPSK: RKeys(<pkI,pkR,pekI,pekR,psk,cr5>) //Not actually cr, but derived from it. , UsingPSK(psk) , RSessionID(sidI,~sidR) - , IIdentity(pkISurrogate) + , Identity_Surrogate(pkISurrogate) ]-> [ State(~id,psk,<'transport_unconfirmed',~sidR,pekI,pekR,cr5>) //Efficiency hack, lets us make this high priority while making state low priority @@ -400,39 +400,54 @@ lemma exists_two_sessions: exists-trace //////// AGREEMENT PROPERTIES /////////////////////////////////////////////// -// These all autoprove, though the non-PSK ones take a while. +// These all autoprove, though the first two take a while. ///////////////////////////////////////////////////////////////////////////// lemma I_disagreement_implies_Sr_or_SiEi_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 + //but R doesn't have a matching session & not(Ex #j. #j < #i & RKeys(<pki,pkr,peki,pekr,psk,ck>) @ j) - ==> // Either R's static is compromised before the session + ==> //Then either R's static was compromised (Ex #j. Reveal_AK(pkr) @ j & #j < #i) - // Or I is hopelessly broken before the session - | (Ex #j #j2. Reveal_AK(pki) @ j & Reveal_EphK(peki) @ j2 & #j2 < #i & #j < #i)" - -lemma no_I_disagreement_without_psk_compromise[reuse]: - "All pki pkr peki pekr psk ck #i. - IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i - & not(Ex #j. #j < #i & RKeys(<pki,pkr,peki,pekr,psk,ck>) @ j) - ==> (psk = 'nopsk') | (Ex #j. #j < #i & Reveal_PSK(psk) @ j)" + //Or both I's static and ephemeral were already compromised + | (Ex #j #j2. Reveal_AK(pki) @ j & #j < #i & Reveal_EphK(peki) @ j2 & #j2 < #i)" lemma R_disagreement_implies_Si_or_SrEr_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 + //but I doesn't have a matching session & not(Ex #j. #j < #i & IKeys(<pki,pkr,peki,pekr,psk,ck>) @ j) - ==> // Either R's static is compromised before the session + ==> //Then either I's static was compromised (Ex #j. Reveal_AK(pki) @ j & #j < #i) - // Or I is hopelessly broken before the session + //Or both R's static and ephemeral were already compromised | (Ex #j #j2. Reveal_AK(pkr) @ j & Reveal_EphK(pekr) @ j2 & #j2 < #i & #j < #i)" -lemma no_R_disagreement_without_psk_compromise[reuse]: - "All pki pkr peki pekr psk ck #i. +lemma disagreement_implies_noPSK_or_compromisedPSK[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 + //but R does not have a matching session + & not(Ex #j. #j < #i & RKeys(<pki,pkr,peki,pekr,psk,ck>) @ j) + ==> //Then either they aren't in PSK mode + (psk = 'nopsk') + //Or the adversary compromised the PSK before the session + | (Ex #j. #j < #i & Reveal_PSK(psk) @ j)) + &(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 + //but I does not have a matching session & not(Ex #j. #j < #i & IKeys(<pki,pkr,peki,pekr,psk,ck>) @ j) - ==> (psk = 'nopsk') | (Ex #j. #j < #i & Reveal_PSK(psk) @ j)" - -lemma injective_agreement: + ==> //Then either they aren't in PSK mode + (psk = 'nopsk') + //Or the adversary compromised the PSK before the session + | (Ex #j. #j < #i & Reveal_PSK(psk) @ j))" + +lemma session_uniqueness: + //For both I and R, a 'confirmed session key' will always be unique (even if all keys are compromised) + //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))) @@ -446,17 +461,19 @@ lemma injective_agreement: lemma secrecy_without_psk_compromise: "(All pki pkr peki pekr psk ck #i #j. - //If the two agents agree on keys + //If the adversary ever knows a session key that I derived from a handshake IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i & K(ck) @ j - ==> (Ex #j2. Reveal_PSK(psk) @ j2) | (psk = 'nopsk')) + ==> //Then either the adversary revealed the PSK, or there was no PSK + (Ex #j2. Reveal_PSK(psk) @ j2) | (psk = 'nopsk')) + //& similarly for R &(All pki pkr peki pekr psk ck #i #j. RConfirm(<pki,pkr,peki,pekr,psk,ck>) @ i & K(ck) @ j ==> (Ex #j2. Reveal_PSK(psk) @ j2) | (psk = 'nopsk'))" lemma key_secrecy[reuse]: - "(All pki pkr peki pekr psk ck #i #j. - //If the two agents agree on keys - IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i & RKeys(<pki,pkr,peki,pekr,psk,ck>) @ j + "(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 ==> //Either the adversary doesn't know the keys not(Ex #j. K(ck) @ j) //Or a pair of keys from the same agent were revealed (at any time) @@ -464,10 +481,16 @@ lemma key_secrecy[reuse]: | (Ex #j #j2. Reveal_AK(pkr) @ j & Reveal_EphK(pekr) @ j2))" lemma identity_hiding: + //Since the public static is always symbolically known to the adversary, we represent identity + //hiding by whether the adversary could learn some other value that is put in the first message at the + //same position as the public static. "All pki pkr peki pekr ck surrogate #i #j. - RKeys(<pki,pkr,peki,pekr,ck>) @ i & IIdentity(surrogate) @ i + //If R received a handshake init with a particular identity surrogate + RKeys(<pki,pkr,peki,pekr,ck>) @ i & Identity_Surrogate(surrogate) @ i + //And the adversary knows that surrogate for the identity & K(surrogate) @ j - ==> (Ex #j. Reveal_AK(pkr) @ j) | (Ex #j. Reveal_AK(pki) @ j) | (Ex #j. Reveal_EphK(peki) @ j)" + ==> //Then the adversary compromised at least one of R's static, I's static, or I's ephemeral + (Ex #j. Reveal_AK(pkr) @ j) | (Ex #j. Reveal_AK(pki) @ j) | (Ex #j. Reveal_EphK(peki) @ j)" end // vim: ft=spthy |