Updated comments for additional explanations and clarity

1 files changed, 40 insertions, 21 deletions

diff --git a/wireguard.m4 b/wireguard.m4
index e48b7f3..83046a2 100644
--- a/wireguard.m4
+++ b/wireguard.m4
@@ -9,7 +9,7 @@ changecom(<!@,@!>)
  * Status:      Basically complete? Use the 'i' heuristic to autoprove.
  *
  * TODO:
- * - Implement identity hiding properly using observational equivalence.
+ * - Implement identity hiding using observational equivalence, instead of the weaker surrogate-based property.
  * - Prove indistinguishability using observational equivalence.
  * - Model ECDH(private, NULL) = NULL
  */
@@ -18,15 +18,23 @@ 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. */
+/* Normally an aead would be arity 4, but in the handshake the nonce is always
+ * the fixed value 0 so for legibility we do not include it */
 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
 /* The authentication can be checked with the key and AAD */
 equations: verify(aead(k, p, a), a, k) = true
 
+/* This restriction tells Tamarin that whenever an Eq( ) fact occurs,
+ * the terms in it must be equal. This allows us to model rules that
+ * only trigger if e.g. the AEAD correctly verifies */
 restriction Eq_testing: "All x y #i. Eq(x, y) @ i ==> x = y"
 
+/* === m4 Definitions ===
+ * These are mostly used to influence Tamarin's heuristics. They can be
+ * commented out by prefixing them with 'dnl'. */
+
 /* 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. */
@@ -44,7 +52,9 @@ define(StateInvariants, F_StateInvariants($*))
  * 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. */
-define(State, L_State($*)) /* HACK: This is a heuristic hack that should be removed by prefixing with m4 comment - d n l. */
+define(State, L_State($*))
+
+/* === Setup and key reveal rules === */
 
 /* Keygen is separate from pairing to allow keys to be paired
  * more than once (if they were generated fresh in the pairing
@@ -55,7 +65,7 @@ rule AgentKeyGen:
     [!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
+ * parties, so we overapproximate this by allowing the same PSK to be reused
  * 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:
@@ -63,7 +73,9 @@ rule PSKKeyGen:
     --[PSKey(~psk)]->
     [ !AgentPSK(~psk) ]
 
-/* Key Reveals for our adversary model */
+/* Key Reveals for our adversary model. These allow the adversary to reveal
+ * any of the keys below at any time, unless restricted in the lemma we wish
+ * to prove. */
 rule PSK_reveal: 
    [ !AgentPSK(k) ] --[ Reveal_PSK(k) ]-> [ Out(k) ]
 
@@ -87,7 +99,8 @@ rule AddPublicKey:
        * 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. */
+       * to identify this pairing. We cache the SiSr in the
+       * invariant to reduce Tamarin's variant precomputation time. */
       State(~id, 'no_message_state')
     , !StateInvariants(~id, ~psk, ~ltkA, pkB, pkB^~ltkA)
     ]
@@ -110,7 +123,9 @@ 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. */
+        /* NOTE: MACs used in the DDoS protection are not modeled, so we assume they are
+         * some arbitrary public values (i.e. known to the adversary, like a fixed string). */
+        m1    = <'1', ~sidI, pekI, astat, ats, $mac1, $mac2> in
     [ /* 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. */
@@ -121,9 +136,12 @@ rule Handshake_Init:
     /* 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>)
-    , F_SolveInit(~id, ~psk, <'init', ~sidI, ~ekI, ci2, ki2, hi1>) /* HACK: This is a heuristic hack that should be removed. */
+    [ State(~id, <'init', ~sidI, ~ekI, ci2, ki2, hi1>)
+      /* F_SolveInit is a bit of a hack to help with Tamarin's heuristics. It allows Tamarin to
+       * prioritize solving backwards from the Handshake_Complete rule even though the State
+       * fact is deprioritized by the m4 definitions above. This will not be necessary in a
+       * future version of Tamarin. */
+    , F_SolveInit(~id, ~psk, <'init', ~sidI, ~ekI, ci2, ki2, hi1>)
     , !EphKeytoReveal(~ekI)
     , Out(m1)
     ]
@@ -146,7 +164,7 @@ 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. */
+        m1    = <'1', sidI, pekI, astat, ats, $mac1, $mac2> /* NOTE: MACs used in DDoS protection are not modeled. */
         /* Constructing the response message m2: */
         cr3   = h(<cr2, pekR, '1'>)
         hr2   = h(<hr1, pekR>)
@@ -158,7 +176,7 @@ 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 /* NOTE: MACs are currently not modeled. */
+        m2    = <'2', sidI, ~sidR, pekR, aempt, $mac1, $mac2> in /* NOTE: MACs used in DDoS protection are not modeled. */
     [ State(~id, anything)
     , !StateInvariants(~id, ~psk, ~ltkR, pkI, sisr)
     , Fr(~ekR)
@@ -166,12 +184,13 @@ rule Handshake_Resp:
     , 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. */
+         * via some more hashing, but it doesn't make a difference here -- if the adversary knows cr6,
+         * it can compute the derived key. */
         RKeys(<pkI, pkR, pekI, pekR, ~psk, cr6>)
       , Identity_Surrogate(pkISurrogate)
     ]->
     [ State(~id, <'transport_unconfirmed', ~sidR, pekI, pekR, cr6>)
-    , F_SolveResp(~id, ~psk, <'transport_unconfirmed', ~sidR, pekI, pekR, cr6>) /* HACK: This is a heuristic hack that should be removed. */
+    , F_SolveResp(~id, ~psk, <'transport_unconfirmed', ~sidR, pekI, pekR, cr6>) /* This is used for the same purpose as F_SolveInit above */
     , !EphKeytoReveal(~ekR)
     , Out(m2)
     ]
@@ -193,16 +212,16 @@ 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 other than the key used to encrypt. */
         mtr   = <'4', sidR, aead(ci6, 'message', '0')> in
     [ State(~id, <'init', sidI, ~ekI, ci2, ki2, hi1>)
-    , F_SolveInit(~id, ~psk, <'init', sidI, ~ekI, ci2, ki2, hi1>) /* HACK: This is a heuristic hack that should be removed. */
+    , F_SolveInit(~id, ~psk, <'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. */
+       * via some more hashing, but it doesn't make a difference here (as with cr6 above). */
       IKeys(<pkI, pkR, pekI, pekR, ~psk, ci6>)
     ]->
     [ State(~id, <'transport', sidI, ci6>)
@@ -219,13 +238,13 @@ rule Handshake_Complete:
 rule R_ConfirmedTransportMessage:
     let mtr = <'4', sid, data> in
     [ State(~id, <'transport_unconfirmed', sidR, pekI, pekR, cr>)
-    , F_SolveResp(~id, ~psk, <'transport_unconfirmed', sidR, pekI, pekR, cr>) /* HACK: This is a heuristic hack that should be removed. */
+    , F_SolveResp(~id, ~psk, <'transport_unconfirmed', sidR, pekI, pekR, cr>)
     , !StateInvariants(~id, ~psk, ~ltkR, pkI, sisr)
     , In(mtr)
     ]--[
       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'.
+      //We manually verify this instead of the recomputation used for other terms above, since
+      //morally R may not know the contents of the message.
     , Eq(verify(data, '0', cr), true)
     ]->
     [ State(~id, <'transport', sidR, cr>) ]