Additional documentation of properties

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