New psk model

In the psk rework, we're now keeping the same protocol for PSK and for
non-PSK. The only difference, therefore, will be whether or not the PSK
is revealed. That is to say -- non-PSK mode is simply an all NULL PSK.
To make this happen, a few other aspects of the protocol were changed,
so this commit changes some fundumental calculations.

1 files changed, 51 insertions, 208 deletions

diff --git a/wireguard.m4 b/wireguard.m4
index 7572a07..665b589 100644
--- a/wireguard.m4
+++ b/wireguard.m4
@@ -3,10 +3,10 @@ changequote(<!,!>)
 changecom(<!@,@!>)
 /*
  * Protocol:    Wireguard protocol
- * Modeler: 	Kevin Milner
- * Date: 	    2017
- * Source:	    Original
- * Status: 	    Basically complete? Use the 'i' heuristic to autoprove.
+ * Modeler:     Kevin Milner & Jason Donenfeld
+ * Date:        2017
+ * Source:      Original
+ * Status:      Basically complete? Use the 'i' heuristic to autoprove.
  */
 
 theory WireGuard
@@ -100,21 +100,22 @@ rule Handshake_Init:
         pekI  = 'g'^~ekI
         eisr  = pkR^~ekI
         //Constructing the init message m1:
-        cii   = h('nopsk')
-        hii   = h(<cii,'id',pkR,pekI>)  //No PSK means no intermediate hashes necessary here
-        ki0   = h(<cii,eisr,'2'>)
-        ci0   = h(<cii,eisr,'1'>)
-        astat = aead(ki0,<pkI,~pkISurrogate>,hii)
+        cii   = h('noise')
+        hii   = h(<cii,'id',pkR,pekI>)
+        ci0   = h(<cii,pekI,'1'>)
+        ci1   = h(<ci0,eisr,'1'>)
+        ki1   = h(<ci0,eisr,'2'>)
+        astat = aead(ki1,<pkI,~pkISurrogate>,hii)
         hi0   = h(<hii,astat>)
-        ki1   = h(<ci0,sisr,'2'>)
-        ci1   = h(<ci0,sisr,'1'>)
-        ats   = aead(ki1,$ts,hi0)
+        ci2   = h(<ci1,sisr,'1'>)
+        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 modelled
+        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, 'nopsk',anything)
+      State(~id,'nopsk',anything)
     , !StateInvariants(~id, ~ltkI, pkR, sisr)
     , Fr(~sidI)
     , Fr(~ekI)
@@ -122,11 +123,11 @@ rule Handshake_Init:
     , Fr(~pkISurrogate)
     ]--[]->
     [ //We cache DH sisr to reduce variant precomputation time for tamarin.
-      State(~id,'nopsk',<'init',~sidI,~ekI,ci1,ki1,hi1>)
+      State(~id,'nopsk',<'init',~sidI,~ekI,ci2,ki2,hi1>)
     , !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>)
+    , F_SolveInit(~id,'nopsk',<'init',~sidI,~ekI,ci2,ki2,hi1>)
     , Out(m1)
     ]
 
@@ -137,25 +138,28 @@ rule Handshake_Resp:
         eier  = pekI^~ekR
         sier  = pkI^~ekR
         //Reconstructing what should be in m1:
-        cri   = h('nopsk')
-        hri   = h(<cri,'id',pkR,pekI>)  //No PSK means no intermediate hashes necessary here
-        kr0   = h(<cri,eisr,'2'>)
-        cr0   = h(<cri,eisr,'1'>)
-        astat = aead(kr0,<pkI,pkISurrogate>,hri)
+        cri   = h('noise')
+        hri   = h(<cri,'id',pkR,pekI>)
+        cr0   = h(<cri,pekI,'1'>)
+        cr1   = h(<cr0,eisr,'1'>)
+        kr1   = h(<cr0,eisr,'2'>)
+        astat = aead(kr1,<pkI,pkISurrogate>,hri)
         hr0   = h(<hri,astat>)
-        kr1   = h(<cr0,sisr,'2'>)
-        cr1   = h(<cr0,sisr,'1'>)
-        ats   = aead(kr1,$ts,hr0)
+        cr2   = h(<cr1,sisr,'1'>)
+        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 modelled
+        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>)
-        kr2   = h(<cr1,eier,'2'>)
-        cr2   = h(<cr1,eier,'1'>)
-        kr3   = h(<cr2,sier,'2'>)
-        cr3   = h(<cr2,sier,'1'>)
-        aempt = aead(kr3,'0',hr2)
-        hr3   = h(<hr2,aempt>)
+        cr4   = h(<cr3,eier,'1'>)
+        cr5   = h(<cr4,sier,'1'>)
+        cr6   = h(<cr5,'nopsk','1'>) //TODO: replace 'nopsk' with actual psk, maybe revealed maybe not
+        hr3   = h(<cr5,hr2,'nopsk','2'>)
+        kr6   = h(<cr5,'nopsk','3'>)
+        aempt = aead(kr6,'e',hr3)
+        hr4   = h(<hr3,aempt>)
         m2    = <'2',sidI,~sidR,pekR,aempt,$mac1,$mac2> in
     [ State(~id,'nopsk',anything)
     , !StateInvariants(~id,~ltkR,pkI,sisr)
@@ -163,13 +167,13 @@ rule Handshake_Resp:
     , Fr(~sidR)
     , In(m1)
     ]--[
-      RKeys(<pkI,pkR,pekI,pekR,'nopsk',cr3>) //Not actually cr3, but derived from it.
+      RKeys(<pkI,pkR,pekI,pekR,'nopsk',cr6>) //Not actually cr6, but derived from it.
     , Identity_Surrogate(pkISurrogate)
     ]->
-    [ State(~id,'nopsk',<'transport_unconfirmed',~sidR,pekI,pekR,cr3>)
+    [ State(~id,'nopsk',<'transport_unconfirmed',~sidR,pekI,pekR,cr6>)
     //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>)
+    , F_SolveResp(~id,'nopsk',<'transport_unconfirmed',~sidR,pekI,pekR,cr6>)
     , !EphKeytoReveal(~ekR)
     , Out(m2)
     ]
@@ -180,177 +184,27 @@ rule Handshake_Complete:
         eier  = pekR^~ekI
         sier  = pekR^~ltkI
         //Reconstruct what should be in m2:
-        hi2   = h(<hi1,pekR>)
-        ki2   = h(<ci1,eier,'2'>)
-        ci2   = h(<ci1,eier,'1'>)
-        ki3   = h(<ci2,sier,'2'>)
-        ci3   = h(<ci2,sier,'1'>)
-        aempt = aead(ki3,'0',hi2)
-        hi3   = h(<hi2,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.
-        mtr   = <'4',sidR,aead(ci3,'message','0')> in
-    [ State(~id,'nopsk',<'init',sidI,~ekI,ci1,ki1,hi1>)
-    , 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.
-    ]->
-    [ State(~id,'nopsk',<'transport',sidI,ci3>)
-    , Out(mtr)
-    ]
-
-/////////////////////////////////////////////////////////////////////////////
-//      PSK Mode 
-// 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:
-    [ State(~id, 'nopsk', state)
-    , !StateInvariants(~id,~ltkA,pkB,sisr)
-    , !AgentPSK(~psk)
-    ]--[
-      AddPSK(~id,~psk)
-    ]->
-    [ State(~id,~psk,'pskadded')
-    ]
-
-rule RemovePSK:
-    [ State(~id,~psk,anything)
-    , !AgentPSK(~psk)
-    ]--[
-      RemovePSK(~id,~psk)
-    ]->
-    [ State(~id,'nopsk','pskremoved')
-    ]
-
-// MESSAGE RULES WITH PSK
-rule Handshake_InitPSK:
-    let pkI   = 'g'^~ltkI
-        pekI  = 'g'^~ekI
-        eisr  = pkR^~ekI
-        //Construct init message m1:
-        cii   = h(<'psk'>)
-        cipsk = h(<cii,psk,'1'>)
-        kipsk = h(<cii,psk,'2'>)
-        hii   = h(<cipsk,'id',kipsk,pkR,pekI>)
-        ci0   = h(<cipsk,pekI,'1'>)
-        ki0   = h(<cipsk,pekI,'2'>)
-        hi0   = h(<hii,pekI>)
-        ci1   = h(<ci0,eisr,'1'>)
-        ki1   = h(<ci0,eisr,'2'>)
-        astat = aead(ki1,<pkI,~pkISurrogate>,hi0)
-        hi1   = h(<hi0,astat>)
-        ci2   = h(<ci1,sisr,'1'>)
-        ki2   = h(<ci1,sisr,'2'>)
-        ats   = aead(ki2,$ts,hi1)
-        hi2   = h(<hi1,ats>)
-        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.
-      State(~id,psk,anything)
-    , !StateInvariants(~id,~ltkI,pkR,sisr)
-    , !AgentPSK(psk)
-    , Fr(~sidI)
-    , Fr(~ekI)
-    , Fr(~pkISurrogate)
-    ]--[]->
-    [ State(~id,psk,<'initpsk',~sidI,~ekI,ci2,ki2,hi2>)
-    , F_SolveInit(~id,psk,<'initpsk',~sidI,~ekI,ci2,ki2,hi2>)
-    , !EphKeytoReveal(~ekI)
-    , Out(m1)
-    ]
-
-rule Handshake_RespPSK:
-    let pkR   = 'g'^~ltkR
-        pekR  = 'g'^~ekR
-        eisr  = pekI^~ltkR
-        eier  = pekI^~ekR
-        sier  = pkI^~ekR
-        //Reconstruct init message m1 to validate it
-        cri   = h(<'psk'>)
-        crpsk = h(<cri,psk,'1'>)
-        krpsk = h(<cri,psk,'2'>)
-        hri   = h(<crpsk,'id',krpsk,pkR,pekI>)
-        cr0   = h(<crpsk,pekI,'1'>)
-        kr0   = h(<crpsk,pekI,'2'>)
-        hr0   = h(<hri,pekI>)
-        cr1   = h(<cr0,eisr,'1'>)
-        kr1   = h(<cr0,eisr,'2'>)
-        astat = aead(ki1,<pkI,pkISurrogate>,hr0)
-        hr1   = h(<hr0,astat>)
-        cr2   = h(<cr1,sisr,'1'>)
-        kr2   = h(<cr1,sisr,'2'>)
-        ats   = aead(kr2,$ts,hr1)
-        hr2   = h(<hr1,ats>)
-        m1    = <'1',sidI,pekI,astat,ats,$mac1,$mac2>
-        //Constructing the response message m2:
-        cr3   = h(<cr2,pekR,'1'>)
-        kr3   = h(<cr2,pekR,'2'>)
-        hr3   = h(<hr2,pekR>)
-        cr4   = h(<cr3,eier,'1'>)
-        kr4   = h(<cr3,eier,'2'>)
-        cr5   = h(<cr4,sier,'1'>)
-        kr5   = h(<cr4,sier,'2'>)
-        aempt = aead(kr5,'0',hr3)
-        hr5   = h(<hr3,aempt>)
-        m2    = <'2',sidI,~sidR,pekR,aempt,$mac1,$mac2> in
-    [ State(~id,psk, anything)
-    , !StateInvariants(~id,~ltkR,pkI,sisr)
-    , !AgentPSK(psk)
-    , Fr(~ekR)
-    , Fr(~sidR)
-    , In(m1)
-    ]--[
-      RKeys(<pkI,pkR,pekI,pekR,psk,cr5>) //Not actually cr, but derived from it.
-    , UsingPSK(psk)
-    , Identity_Surrogate(pkISurrogate)
-    ]->
-    [ State(~id,psk,<'transport_unconfirmed',~sidR,pekI,pekR,cr5>)
-    , F_SolveResp(~id,psk,<'transport_unconfirmed',~sidR,pekI,pekR,cr5>)
-    , !EphKeytoReveal(~ekR)
-    , Out(m2)
-    ]
-
-rule Handshake_CompletePSK:
-    let pkI   = 'g'^~ltkI
-        pekI  = 'g'^~ekI
-        eier  = pekR^~ekI
-        sier  = pekR^~ltkI
-        //Reconstructing the response message m2 to validate it
         ci3   = h(<ci2,pekR,'1'>)
-        ki3   = h(<ci2,pekR,'2'>)
-        hi3   = h(<hi2,pekR>)
+        hi2   = h(<hi1,pekR>)
         ci4   = h(<ci3,eier,'1'>)
-        ki4   = h(<ci3,eier,'2'>)
         ci5   = h(<ci4,sier,'1'>)
-        ki5   = h(<ci4,sier,'2'>)
-        aempt = aead(ki5,'0',hi3)
-        hi5   = h(<hi3,aempt>)
-        m2    = <'2',sidI,sidR,pekR,aempt,$mac1,$mac2> 
+        ci6   = h(<ci5,'nopsk','1'>) //TODO: see note above about using real psk instead of 'nopsk'
+        hi3   = h(<ci5,hi2,'nopsk','2'>)
+        ki6   = h(<ci5,'nopsk','3'>)
+        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.
-        mtr   = <'4',sidR,aead(ci5,'message','0')> in
-    [ State(~id,psk,<'initpsk',sidI,~ekI,ci2,ki2,hi2>)
-    , F_SolveInit(~id,psk,<'initpsk',sidI,~ekI,ci2,ki2,hi2>)
+        mtr   = <'4',sidR,aead(ci6,'message','0')> in
+    [ State(~id,'nopsk',<'init',sidI,~ekI,ci2,ki2,hi1>)
+    , F_SolveInit(~id,'nopsk',<'init',sidI,~ekI,ci2,ki2,hi1>)
     , !StateInvariants(~id,~ltkI,pkR,sisr)
-    , !AgentPSK(psk)
     , In(m2)
     ]--[
-      IKeys(<pkI,pkR,pekI,pekR,psk,ci5>) //Not actually ci, but derived from it.
-    , UsingPSK(psk)
+      IKeys(<pkI,pkR,pekI,pekR,'nopsk',ci6>) //Not actually ci6, but derived from it.
     ]->
-    [ State(~id,psk,<'transport',sidI,ci3>)
+    [ State(~id,'nopsk',<'transport',sidI,ci3>)
     , Out(mtr)
     ]
 
@@ -379,22 +233,11 @@ rule R_ConfirmedTransportMessage:
 
 /////////////////////////////////////////////////////////////////////////////
 
-lemma exists_session_nopsk: exists-trace
+lemma exists_session: exists-trace
     "Ex pki pkr peki pekr ck #i #j.
         IKeys(<pki,pkr,peki,pekr,'nopsk',ck>) @ i 
         & RConfirm(<pki,pkr,peki,pekr,'nopsk',ck>) @ j & #i < #j"
 
-// The following two exists-trace lemmas take a very long time to
-// autoprove, but can be proved by hand with a bit of patience.
-// The heuristic is not well-suited to completing traces instead
-// of ruling out attacks.
-// To prove manually, solve for the state facts and pick the 
-// 'SwitchToPSK case 1' options for both
-lemma exists_session_psk: exists-trace
-    "Ex pki pkr peki pekr psk ck #i #j.
-        IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i & UsingPSK(psk) @ i
-        & RConfirm(<pki,pkr,peki,pekr,psk,ck>) @ j & #i < #j"
-
 //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.