Cleanup and commenting

Cleaned up some of the comments and actions that turned out to be
unnecessary. Also clarified some of the things that are assumed
in the current model

1 files changed, 51 insertions, 46 deletions

diff --git a/wireguard.m4 b/wireguard.m4
index 27e8e3f..7572a07 100644
--- a/wireguard.m4
+++ b/wireguard.m4
@@ -4,9 +4,9 @@ changecom(<!@,@!>)
 /*
  * Protocol:    Wireguard protocol
  * Modeler: 	Kevin Milner
- * Date: 	    February 2017
+ * Date: 	    2017
  * Source:	    Original
- * Status: 	    WIP
+ * Status: 	    Basically complete? Use the 'i' heuristic to autoprove.
  */
 
 theory WireGuard
@@ -14,26 +14,34 @@ begin
 
 builtins: hashing, diffie-hellman
 //We're not going to model the nonce in the aead, since it's always 0
-//in the handshake. Note that this can only over-approximate attacks,
-//since it would allow collisions between two AEADs with different nonces.
+//in the handshake.
 functions: aead/3, decrypt/2, verify/3, true/0
-equations: decrypt(aead(k,p,a),k) = p     //Plaintext can be recovered using 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
 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.
 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)
 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.
 define(State, L_State($*))
 
-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)"
-
 //Pre-established trust relationships
 restriction pairings_unique:
     "All id id2 ka kb #i #j.
@@ -58,7 +66,7 @@ rule PSKKeyGen:
     --[PSKey(~psk)]->
     [ !AgentPSK(~psk) ]
 
-/* Key Reveals for the eCK model */
+/* Key Reveals for our adversary model */
 rule PSK_reveal: 
    [ !AgentPSK(k) ] --[ Reveal_PSK(k) ]-> [ Out(k) ]
 
@@ -66,21 +74,22 @@ rule AgentKey_reveal:
    [ !AgentKey(k) ] --[ Reveal_AK('g'^k) ]-> [ Out(k) ]
 
 rule EphKey_reveal:
-   [ !EphKey(k) ] --[ Reveal_EphK('g'^k) ]-> [ Out(k) ]
+   [ !EphKeytoReveal(k) ] --[ Reveal_EphK('g'^k) ]-> [ Out(k) ]
 
-//Models an agent adding anothers public key out-of-band.
+//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)
     , !AgentKey(~ltkB)
     , Fr(~id)
-    ]--[
-      InEq($A,$B)
-    ]->
+    ]--[]->
     [ // 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.
+      // to this initial pairing rule. The fresh ~id is used
+      // to identify this pairing.
       State(~id, 'nopsk', 'nostate')
     , !StateInvariants(~id, ~ltkA, pkB, pkB^~ltkA)
     ]
@@ -101,7 +110,7 @@ rule Handshake_Init:
         ci1   = h(<ci0,sisr,'1'>)
         ats   = aead(ki1,$ts,hi0)
         hi1   = h(<hi0,ats>)
-        m1    = <'1',~sidI,pekI,astat,ats,$mac1,$mac2> in //TODO:Model MACs
+        m1    = <'1',~sidI,pekI,astat,ats,$mac1,$mac2> in //Note: MACs are currently not modelled
     [ //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.
@@ -109,16 +118,16 @@ rule Handshake_Init:
     , !StateInvariants(~id, ~ltkI, pkR, sisr)
     , Fr(~sidI)
     , Fr(~ekI)
+    // The pkISurrogate is used later to approximate identity hiding.
     , Fr(~pkISurrogate)
-    ]--[
-      StartHandshake(pkI,pkR,pekI,'nopsk',~sidI)
-    ]->
+    ]--[]->
     [ //We cache DH sisr to reduce variant precomputation time for tamarin.
       State(~id,'nopsk',<'init',~sidI,~ekI,ci1,ki1,hi1>)
-    , Out(m1)
-    , !EphKey(~ekI)
-    //Efficiency hack, lets us make this high priority while making state low priority
+    , !EphKeytoReveal(~ekI)
+    //This is a heuristic hack, so that the heuristic can prioritize solving for
+    //the init rule without prioritizing the State() fact.
     , F_SolveInit(~id,'nopsk',<'init',~sidI,~ekI,ci1,ki1,hi1>)
+    , Out(m1)
     ]
 
 rule Handshake_Resp:
@@ -138,7 +147,7 @@ rule Handshake_Resp:
         cr1   = h(<cr0,sisr,'1'>)
         ats   = aead(kr1,$ts,hr0)
         hr1   = h(<hr0,ats>)
-        m1    = <'1',sidI,pekI,astat,ats,$mac1,$mac2> //TODO:Model MACs
+        m1    = <'1',sidI,pekI,astat,ats,$mac1,$mac2> //Note: MACs are currently not modelled
         //Constructing the response message m2:
         hr2   = h(<hr1,pekR>)
         kr2   = h(<cr1,eier,'2'>)
@@ -155,14 +164,14 @@ rule Handshake_Resp:
     , In(m1)
     ]--[
       RKeys(<pkI,pkR,pekI,pekR,'nopsk',cr3>) //Not actually cr3, but derived from it.
-    , RSessionID(sidI,~sidR)
     , 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
+    //This is a heuristic hack, so that the heuristic can prioritize solving for
+    //the resp rule without prioritizing the State() fact.
     , F_SolveResp(~id,'nopsk',<'transport_unconfirmed',~sidR,pekI,pekR,cr3>)
+    , !EphKeytoReveal(~ekR)
     , Out(m2)
-    , !EphKey(~ekR)
     ]
 
 rule Handshake_Complete:
@@ -183,13 +192,11 @@ rule Handshake_Complete:
         //in it are public except the key used to encrypt.
         mtr   = <'4',sidR,aead(ci3,'message','0')> in
     [ State(~id,'nopsk',<'init',sidI,~ekI,ci1,ki1,hi1>)
-    //Efficiency hack, lets us make this high priority while making state low priority
     , F_SolveInit(~id,'nopsk',<'init',sidI,~ekI,ci1,ki1,hi1>)
     , !StateInvariants(~id,~ltkI,pkR,sisr)
     , In(m2)
     ]--[
       IKeys(<pkI,pkR,pekI,pekR,'nopsk',ci3>) //Not actually ci3, but derived from it.
-    , ISessionID(sidI,sidR)
     ]->
     [ State(~id,'nopsk',<'transport',sidI,ci3>)
     , Out(mtr)
@@ -197,7 +204,14 @@ rule Handshake_Complete:
 
 /////////////////////////////////////////////////////////////////////////////
 //      PSK Mode 
-// Switching mode interrupts any handshakes in progress (is this correct?)
+// Switching mode interrupts any handshakes in progress
+// This is modeled by resetting agent state to the 'pskadded' state.
+//
+// The additional !AgentPSK() constraint allows us to backwards solve for
+// the PSK generation, which sets up the key and a way for the adversary to
+// reveal it. This means that the PSK was necessarily generated fresh at some
+// point, so we are implicitly assuming that the adversary doesn't have a
+// chance to control the value of the PSK.
 /////////////////////////////////////////////////////////////////////////////
 
 rule SwitchtoPSK:
@@ -206,7 +220,6 @@ rule SwitchtoPSK:
     , !AgentPSK(~psk)
     ]--[
       AddPSK(~id,~psk)
-    , InEq(state,'pskremoved') // Just so it doesn't loop forever here
     ]->
     [ State(~id,~psk,'pskadded')
     ]
@@ -241,7 +254,7 @@ rule Handshake_InitPSK:
         ki2   = h(<ci1,sisr,'2'>)
         ats   = aead(ki2,$ts,hi1)
         hi2   = h(<hi1,ats>)
-        m1    = <'1',~sidI,pekI,astat,ats,$mac1,$mac2> in //TODO:Model MACs
+        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.
@@ -251,16 +264,11 @@ rule Handshake_InitPSK:
     , Fr(~sidI)
     , Fr(~ekI)
     , Fr(~pkISurrogate)
-    ]--[
-      StartHandshake(pkI,pkR,pekI,psk,~sidI)
-    , UsingPSK(psk)
-    ]->
-    [ //We cache DH sisr to reduce variant precomputation time for tamarin.
-      State(~id,psk,<'initpsk',~sidI,~ekI,ci2,ki2,hi2>)
-    //Efficiency hack, lets us make this high priority while making state low priority
+    ]--[]->
+    [ State(~id,psk,<'initpsk',~sidI,~ekI,ci2,ki2,hi2>)
     , F_SolveInit(~id,psk,<'initpsk',~sidI,~ekI,ci2,ki2,hi2>)
+    , !EphKeytoReveal(~ekI)
     , Out(m1)
-    , !EphKey(~ekI)
     ]
 
 rule Handshake_RespPSK:
@@ -285,7 +293,7 @@ rule Handshake_RespPSK:
         kr2   = h(<cr1,sisr,'2'>)
         ats   = aead(kr2,$ts,hr1)
         hr2   = h(<hr1,ats>)
-        m1    = <'1',sidI,pekI,astat,ats,$mac1,$mac2> //TODO:Model MACs
+        m1    = <'1',sidI,pekI,astat,ats,$mac1,$mac2>
         //Constructing the response message m2:
         cr3   = h(<cr2,pekR,'1'>)
         kr3   = h(<cr2,pekR,'2'>)
@@ -306,14 +314,12 @@ rule Handshake_RespPSK:
     ]--[
       RKeys(<pkI,pkR,pekI,pekR,psk,cr5>) //Not actually cr, but derived from it.
     , UsingPSK(psk)
-    , RSessionID(sidI,~sidR)
     , 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
     , F_SolveResp(~id,psk,<'transport_unconfirmed',~sidR,pekI,pekR,cr5>)
+    , !EphKeytoReveal(~ekR)
     , Out(m2)
-    , !EphKey(~ekR)
     ]
 
 rule Handshake_CompletePSK:
@@ -336,7 +342,6 @@ rule Handshake_CompletePSK:
         //in it are public except the key used to encrypt.
         mtr   = <'4',sidR,aead(ci5,'message','0')> in
     [ State(~id,psk,<'initpsk',sidI,~ekI,ci2,ki2,hi2>)
-    //Efficiency hack, lets us make this high priority while making state low priority
     , F_SolveInit(~id,psk,<'initpsk',sidI,~ekI,ci2,ki2,hi2>)
     , !StateInvariants(~id,~ltkI,pkR,sisr)
     , !AgentPSK(psk)
@@ -344,7 +349,6 @@ rule Handshake_CompletePSK:
     ]--[
       IKeys(<pkI,pkR,pekI,pekR,psk,ci5>) //Not actually ci, but derived from it.
     , UsingPSK(psk)
-    , ISessionID(sidI,sidR)
     ]->
     [ State(~id,psk,<'transport',sidI,ci3>)
     , Out(mtr)
@@ -361,12 +365,13 @@ rule Handshake_CompletePSK:
 rule R_ConfirmedTransportMessage:
     let mtr = <'4',sid,data> in
     [ State(~id,psk,<'transport_unconfirmed',sidR,pekI,pekR,cr>)
-    //Efficiency hack, lets us make this high priority while making state low priority
     , F_SolveResp(~id,psk,<'transport_unconfirmed',sidR,pekI,pekR,cr>)
     , !StateInvariants(~id,~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'.
     , Eq(verify(data,'0',cr),true)
     ]->
     [ State(~id,psk,<'transport',sidR,cr>) ]