Style

1 files changed, 96 insertions, 87 deletions

diff --git a/wireguard.m4 b/wireguard.m4
index 8c8b073..98f0a2f 100644
--- a/wireguard.m4
+++ b/wireguard.m4
@@ -7,66 +7,70 @@ changecom(<!@,@!>)
  * Date:        2017
  * Source:      Original
  * Status:      Basically complete? Use the 'i' heuristic to autoprove.
+ *
+ * TODO:
+ * - Implement identity hiding properly using observational equivalence.
+ * - Prove indistinguishability using observational equivalence.
+ * - Model ECDH(private, NULL) = NULL
  */
 
 theory WireGuard
 begin
 
 builtins: hashing, diffie-hellman
-//We're not going to model the nonce in the aead, since it's always 0
-//in the handshake.
+/* 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
+/* The plaintext can be recovered with the key */
 equations: decrypt(aead(k,p,a),k) = p
-//The authentication can be checked with the key and AAD
+/* The authentication can be checked with the key and AAD */
 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)"
 
-//Uncomment these to prevent any adversary message modifications,
-//useful for checking exists-trace lemmas and making sure messsages
-//don't require the adversary to reorder terms etc.
+/* Uncomment these to prevent any adversary message modifications,
+ * useful for checking exists-trace lemmas and making sure messsages
+ * don't require the adversary to reorder terms etc. */
 dnl define(In, AuthenticatedMessage($*))
 dnl define(Out, AuthenticatedMessage($*))
 
-//These defines are for the heuristic goal sorting. F_ indicates that the
-//heuristic should prioritize solving it, which we use to solve for where
-//agents got various constraints (like the keys, and key relationships)
+/* These defines are for the heuristic goal sorting. F_ indicates that the
+ * heuristic should prioritize solving it, which we use to solve for where
+ * agents got various constraints (like the keys, and key relationships) */
 define(AgentKey, F_AgentKey($*))
 define(AgentPSK, F_AgentPSK($*))
 define(StateInvariants, F_StateInvariants($*))
-// L_ indicates the heuristic should deprioritize solving the goal. In this
-// case, typically agent state can come from just about anywhere so it creates
-// a ton of case distinctions when we're usually only interested in the current
-// session anyway.
+
+/* L_ indicates the heuristic should deprioritize solving the goal. In this
+ * case, typically agent state can come from just about anywhere so it creates
+ * a ton of case distinctions when we're usually only interested in the current
+ * session anyway. */
 dnl define(State, L_State($*))
 
-//Pre-established trust relationships
+/* Pre-established trust relationships */
 restriction pairings_unique:
     "All id id2 ka kb #i #j.
         Paired(id,ka,kb) @ i & Paired(id2,ka,kb) @ j
     ==> #i = #j"
 
-//Keygen is separate from pairing to allow keys to be paired
-//more than once (if they were generated fresh in the pairing
-//this would not be possible)
+/* Keygen is separate from pairing to allow keys to be paired
+ * more than once (if they were generated fresh in the pairing
+ * this would not be possible */
 rule AgentKeyGen:
     [ Fr(~ltk) ]
     --[DHKey(~ltk)]->
     [!AgentKey(~ltk), Out('g'^~ltk)]
 
-//Semi-malicious or ignorant agents might share
-//a PSK with multiple parties, so we'll overapproximate this
-//by allowing it to be shared arbitrarily. If this finds an
-//attack then it may not be a 'real' attack, but if it doesn't
-//then there is no problem with PSK reuse.
+/* Semi-malicious or ignorant agents might share a PSK with multiple
+ * parties, so we'll overapproximate this by allowing it to be shared
+ * arbitrarily. If this finds an attack then it may not be a 'real'
+ * attack, but if it doesn't then there is no problem with PSK reuse. */
 rule PSKKeyGen:
     [ Fr(~psk) ]
     --[PSKey(~psk)]->
     [ !AgentPSK(~psk) ]
 
-//Key Reveals for our adversary model
+/* Key Reveals for our adversary model */
 rule PSK_reveal: 
    [ !AgentPSK(k) ] --[ Reveal_PSK(k) ]-> [ Out(k) ]
 
@@ -76,9 +80,9 @@ rule AgentKey_reveal:
 rule EphKey_reveal:
    [ !EphKeytoReveal(k) ] --[ Reveal_EphK('g'^k) ]-> [ Out(k) ]
 
-//Models an agent adding anothers public key out-of-band, we assume that
-//all relationships set up this way are 'sane' and both of the keys involved
-//were generated fresh.
+/* Models an agent adding anothers public key out-of-band, we assume that
+ * all relationships set up this way are 'sane' and both of the keys involved
+ * were generated fresh. */
 rule AddPublicKey:
     let pkB = 'g'^~ltkB in
     [ !AgentKey(~ltkA)
@@ -86,21 +90,22 @@ rule AddPublicKey:
     , !AgentPSK(~psk)
     , Fr(~id)
     ]-->
-    [ // For search efficiency, state is divided into
-      // an invariant portion and a variant portion. This
-      // allows tamarin to immediately bind the keys back
-      // to this initial pairing rule. The fresh ~id is used
-      // to identify this pairing.
+    [ /* For search efficiency, state is divided into
+       * an invariant portion and a variant portion. This
+       * 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)
     ]
 
-// MESSAGE RULES
+/* === Message Rules === */
+
 rule Handshake_Init:
     let pkI   = 'g'^~ltkI
         pekI  = 'g'^~ekI
         eisr  = pkR^~ekI
-        //Constructing the init message m1:
+        /* Constructing the init message m1: */
         cii   = h('noise')
         hii   = h(<cii,'id',pkR,pekI>)
         ci0   = h(<cii,pekI,'1'>)
@@ -112,18 +117,18 @@ rule Handshake_Init:
         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.
+        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)
     , Fr(~sidI)
     , Fr(~ekI)
-    // The pkISurrogate is used later to approximate identity hiding.
+    /* The pkISurrogate is used later to approximate identity hiding. */
     , Fr(~pkISurrogate)
     ]-->
-    [ //We cache DH sisr to reduce variant precomputation time for tamarin.
+    [ /* We cache DH sisr to reduce variant precomputation time for tamarin. */
       State(~id,<'init',~sidI,~ekI,ci2,ki2,hi1>)
     , !EphKeytoReveal(~ekI)
     , Out(m1)
@@ -135,7 +140,7 @@ rule Handshake_Resp:
         eisr  = pekI^~ltkR
         eier  = pekI^~ekR
         sier  = pkI^~ekR
-        //Reconstructing what should be in m1:
+        /* Reconstructing what should be in m1: */
         cri   = h('noise')
         hri   = h(<cri,'id',pkR,pekI>)
         cr0   = h(<cri,pekI,'1'>)
@@ -147,8 +152,8 @@ rule Handshake_Resp:
         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:
+        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'>)
@@ -159,15 +164,17 @@ rule Handshake_Resp:
         hr3   = h(<hr2,hrt>)
         aempt = aead(kr6,'e',hr3)
         hr4   = h(<hr3,aempt>)
-        m2    = <'2',sidI,~sidR,pekR,aempt,$mac1,$mac2> in
+        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)
     ]--[
-      RKeys(<pkI,pkR,pekI,pekR,~psk,cr6>) //Not actually cr6, but derived from it.
-    , Identity_Surrogate(pkISurrogate)
+        /* 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>)
+      , Identity_Surrogate(pkISurrogate)
     ]->
     [ State(~id,<'transport_unconfirmed',~sidR,pekI,pekR,cr6>)
     , !EphKeytoReveal(~ekR)
@@ -179,7 +186,7 @@ rule Handshake_Complete:
         pekI  = 'g'^~ekI
         eier  = pekR^~ekI
         sier  = pekR^~ltkI
-        //Reconstruct what should be in m2:
+        /* Reconstruct what should be in m2: */
         ci3   = h(<ci2,pekR,'1'>)
         hi2   = h(<hi1,pekR>)
         ci4   = h(<ci3,eier,'1'>)
@@ -191,26 +198,27 @@ rule Handshake_Complete:
         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.
+        /* 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)
     , In(m2)
     ]--[
-      IKeys(<pkI,pkR,pekI,pekR,~psk,ci6>) //Not actually ci6, but derived from it.
+      /* 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>)
     ]->
     [ State(~id,<'transport',sidI,ci6>)
     , Out(mtr)
     ]
 
-/////////////////////////////////////////////////////////////////////////////
-//      Key confirmation (both modes) 
-// For proving agreement properties after the first transport message
-// This is not faithfully modelled, since we don't care about the contents
-// of the transport message--instead it's generically 'anything encrypted
-// with the transport key I just set up'
-/////////////////////////////////////////////////////////////////////////////
+/* === Key Confirmation ===
+ *
+ * For proving agreement properties after the first transport message
+ * This is not faithfully modelled, since we don't care about the contents
+ * of the transport message--instead it's generically 'anything encrypted
+ * with the transport key I just set up'. */
 
 rule R_ConfirmedTransportMessage:
     let mtr = <'4',sid,data> in
@@ -225,14 +233,16 @@ rule R_ConfirmedTransportMessage:
     ]->
     [ State(~id,<'transport',sidR,cr>) ]
     
+/* === Session Traces ===
+ *
+ * We show that at least the protocol works. */
 
-/////////////////////////////////////////////////////////////////////////////
 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"
 
-//There are only three numbers, 0, 1, and infinity. So 2 == infinity
+/* 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
@@ -241,41 +251,40 @@ lemma exists_two_sessions: exists-trace
         & #i < #i2 & not(sesskeys = sesskeys2)"
 
 
-//////// AGREEMENT PROPERTIES ///////////////////////////////////////////////
-// These all autoprove, though the first two take a while.
-/////////////////////////////////////////////////////////////////////////////
+/* === Agreement Properties === */
+
 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
+        /* 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
+        /* but R doesn't have a matching session */
         & not(Ex #j. #j < #i & RKeys(<pki,pkr,peki,pekr,psk,ck>) @ j)
-    ==> //Then the PSK was compromised (or not in use) and
+    ==> /* Then the PSK was compromised (or not in use) and */
         (Ex #j. Reveal_PSK(psk) @ j & #j < #i) & (
-        //either R's static was compromised
+        /* either R's static was compromised */
         (Ex #j. Reveal_AK(pkr) @ j & #j < #i)
-        //or both I's static and ephemeral were already compromised
+        /* 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_and_PSK_compromise[reuse]:
     "All pki pkr peki pekr psk ck #i.
-        //If R believes they have a confirmed session with 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
+        /* but I doesn't have a matching session */
         & not(Ex #j. #j < #i & IKeys(<pki,pkr,peki,pekr,psk,ck>) @ j)
-    ==> //Then the PSK was compromised (or not in use) and
+    ==> /* Then the PSK was compromised (or not in use) and */
         (Ex #j. Reveal_PSK(psk) @ j & #j < #i) & (
-        //either I's static was compromised
+        /* either I's static was compromised */
         (Ex #j. Reveal_AK(pki) @ j & #j < #i)
-        //or both R's static and ephemeral were already compromised
+        /* 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 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.
+    /* 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)))
@@ -283,33 +292,33 @@ lemma session_uniqueness:
         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 //////////////////////////////////////////////////
-// All autoprove, but key_secrecy takes forever
-/////////////////////////////////////////////////////////////////////////////
+/* === Secrecy Properties === */
 
 lemma key_secrecy[reuse]:
     "(All pki pkr peki pekr psk ck #i #i2.
-        //If I and R agree on keys
+        /* 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
+    ==> /* Either the adversary doesn't know the keys */
         not(Ex #j. K(ck) @ j) 
-        //or the psk was compromised (or not in use) and pair of keys from the same agent was revealed (at any time)
+        /* or the psk was compromised (or not in use) */
         | ((Ex #j. Reveal_PSK(psk) @ j) & (
+           /* and pair of keys from the same agent was revealed (at any time) */
            (Ex #j #j2. Reveal_AK(pki) @ j & Reveal_EphK(peki) @ j2)
          | (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.
+    /* 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.
-        //If R received a handshake init with a particular identity surrogate
+        /* 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
+        /* 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
+    ==> /* 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