PSK Mode added, and efficiency improved by splitting out state invariants

1 files changed, 161 insertions, 123 deletions

diff --git a/wireguard.m4 b/wireguard.m4
index fe98795..c34b92c 100644
--- a/wireguard.m4
+++ b/wireguard.m4
@@ -26,14 +26,15 @@ dnl define(In, AuthenticatedMessage($*))
 dnl define(Out, AuthenticatedMessage($*))
 
 define(AgentKey, F_AgentKey($*))
+define(StateInvariants, F_StateInvariants($*))
 
 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 inj inj2 ka kb #i #j.
-        Paired(inj,ka,kb) @ i & Paired(inj2,ka,kb) @ j
+    "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
@@ -59,16 +60,16 @@ rule AddPublicKey:
     let pkB = 'g'^~ltkB in
     [ !AgentKey(~ltkA)
     , !AgentKey(~ltkB)
-    //This is for tamarin to identify State() as injective,
-    //which requires a unique fresh first term in the fact
-    , Fr(~inj)
+    , Fr(~id)
     ]--[
-      Paired(~inj,~ltkA, pkB)
-    , InEq($A,$B)
+      InEq($A,$B)
     ]->
-    [ //We cache the static-static to reduce the time needed for
-      //variant precomputations in tamarin.
-      State(~inj,~ltkA, pkB, pkB^~ltkA, 'nopsk', '0')
+    [ // 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.
+      State(~id, 'nopsk', 'nostate')
+    , !StateInvariants(~id, ~ltkA, pkB, pkB^~ltkA)
     ]
 
 /* Uncomment to allow various key compromises
@@ -85,42 +86,46 @@ rule CompromisePSK:
 
 // MESSAGE RULES
 rule Handshake_Init:
-    let eisr  = pkR^~ekI
+    let pkI   = 'g'^~ltkI
+        pekI  = 'g'^~ekI
+        eisr  = pkR^~ekI
         //Constructing the init message m1:
         cii   = h('nopsk')
-        hii   = h(<cii,'id',pkR,'g'^~ekI>)  //No PSK means no intermediate hashes necessary here
+        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,'g'^~ltkI,hii)
+        astat = aead(ki0,pkI,hii)
         hi0   = h(<hii,astat>)
         ki1   = h(<ci0,sisr,'2'>)
         ci1   = h(<ci0,sisr,'1'>)
         ats   = aead(ki1,~ts,hi0)
         hi1   = h(<hi0,ats>)
-        m1    = <'1',~sidI,'g'^~ekI,astat,ats,$mac1,$mac2> in //TODO:Model MACs
+        m1    = <'1',~sidI,pekI,astat,ats,$mac1,$mac2> in //TODO:Model MACs
     [ //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(~inj,~ltkI,pkR,sisr,'nopsk',anything)
+      State(~id, 'nopsk',anything)
+    , !StateInvariants(~id, ~ltkI, pkR, sisr)
     , Fr(~sidI)
     , Fr(~ekI)
     , Fr(~ts)
     ]--[
-      Binding(~inj,~ltkI,pkR)
-    , EphemeralKey(~ekI)
+      StartHandshake(pkI,pkR,pekI,'nopsk',~sidI)
     ]->
     [ //We cache DH sisr to reduce variant precomputation time for tamarin.
-      State(~inj,~ltkI,pkR,sisr,'nopsk',<'init',~sidI,~ekI,ci1,ki1,hi1>)
+      State(~id,'nopsk',<'init',~sidI,~ekI,ci1,ki1,hi1>)
     , Out(m1)
     ]
 
 rule Handshake_Resp:
-    let eisr  = pekI^~ltkR
+    let pkR   = 'g'^~ltkR
+        pekR  = 'g'^~ekR
+        eisr  = pekI^~ltkR
         eier  = pekI^~ekR
         sier  = pkI^~ekR
         //Reconstructing what should be in m1:
         cri   = h('nopsk')
-        hri   = h(<cri,'id','g'^~ltkR,pekI>)  //No PSK means no intermediate hashes necessary here
+        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,hri)
@@ -131,30 +136,31 @@ rule Handshake_Resp:
         hr1   = h(<hr0,ats>)
         m1    = <'1',sidI,pekI,astat,ats,$mac1,$mac2> //TODO:Model MACs
         //Constructing the response message m2:
-        hr2   = h(<hr1,'g'^~ekR>)
+        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>)
-        m2    = <'2',sidI,~sidR,'g'^~ekR,aempt,$mac1,$mac2> in
-    [ State(~inj,~ltkR,pkI,sisr,'nopsk',anything)
+        m2    = <'2',sidI,~sidR,pekR,aempt,$mac1,$mac2> in
+    [ State(~id,'nopsk',anything)
+    , !StateInvariants(~id,~ltkR,pkI,sisr)
     , Fr(~ekR)
     , Fr(~sidR)
     , In(m1)
     ]--[
-      Binding(~inj,~ltkR,pkI)
-    , EphemeralKey(~ekR)
-    , AEADIncludesKey(ats,~ltkR)
-    , RespKeys('g'^~ltkR,pkI,cr3) //Not actually cr3, but derived from it.
+      RKeys(<pkI,pkR,pekI,pekR,'nopsk',cr3>) //Not actually cr3, but derived from it.
+    , RSessionID(sidI,~sidR)
     ]->
-    [ State(~inj,~ltkR,pkI,sisr,'nopsk',<'transport',cr3>)
+    [ State(~id,'nopsk',<'transport',cr3>)
     , Out(m2)
     ]
 
 rule Handshake_Complete:
-    let eier  = pekR^~ekI
+    let pkI   = 'g'^~ltkI
+        pekI  = 'g'^~ekI
+        eier  = pekR^~ekI
         sier  = pekR^~ltkI
         //Reconstruct what should be in m2:
         hi2   = h(<hi1,pekR>)
@@ -165,167 +171,199 @@ rule Handshake_Complete:
         aempt = aead(ki3,'0',hi2)
         hi3   = h(<hi2,aempt>)
         m2    = <'2',sidI,sidR,pekR,aempt,$mac1,$mac2> in
-    [ State(~inj,~ltkI,pkR,sisr,'nopsk',<'init',sidI,~ekI,ci1,ki1,hi1>)
+    [ State(~id,'nopsk',<'init',sidI,~ekI,ci1,ki1,hi1>)
+    , !StateInvariants(~id,~ltkI,pkR,sisr)
     , In(m2)
     ]--[
-      Binding(~inj,~ltkI,pkR)
-    , AEADIncludesKey(aempt,eier)
-    , InitKeys('g'^~ltkI,pkR,ci3) //Not actually ci3, but derived from it.
+      IKeys(<pkI,pkR,pekI,pekR,'nopsk',ci3>) //Not actually ci3, but derived from it.
+    , ISessionID(sidI,sidR)
     ]->
-    [ State(~inj,~ltkI,pkR,sisr,'nopsk',<'transport',ci3>)
+    [ State(~id,'nopsk',<'transport',ci3>)
     ]
 
 /////////////////////////////////////////////////////////////////////////////
 //      PSK Mode 
-// (NYI, most of these rules are currently copy paste from above)
+// Switching mode interrupts any handshakes in progress (is this correct?)
 /////////////////////////////////////////////////////////////////////////////
-/*
+
 rule SwitchtoPSK:
-    [ State(~inj,~ltka,pkb,sisr,'nopsk',anything)
+    [ State(~id, 'nopsk', state)
+    , !StateInvariants(~id,~ltkA,pkB,sisr)
     , !AgentPSK(~psk)
     ]--[
-      Binding(~inj,~ltka,pkb)
-    , AddPSK(~ltka,pkb,~psk)
+      AddPSK(~id,~psk)
+    , InEq(state,'pskremoved') // Just so it doesn't loop forever here
     ]->
-    [ State(~inj,~ltka,pkb,sisr,~psk,anything)
+    [ State(~id,~psk,'pskadded')
     ]
 
 rule RemovePSK:
-    [ State(~inj,~ltka,pkb,sisr,~psk,anything)
+    [ State(~id,~psk,anything)
+    , !AgentPSK(~psk)
     ]--[
-      Binding(~inj,~ltka,pkb)
-    , RemovePSK(~ltka,pkb,~psk)
+      RemovePSK(~id,~psk)
     ]->
-    [ State(~inj,~ltka,pkb,sisr,'nopsk',anything)
+    [ State(~id,'nopsk','pskremoved')
     ]
 
 // MESSAGE RULES WITH PSK
 rule Handshake_InitPSK:
-    let eisr  = pkR^~ekI
+    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,'g'^~ekI>)
-        ci0   = h(<cipsk,'g'^~ekI,'1'>)
-        ki0   = h(<cipsk,'g'^~ekI,'2'>)
-        hi0   = h(<hi0,'g'^~ekI>)
+        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,'g'^~ltkI,hi0)
-        hi1   = h(<hi1,astat>)
+        astat = aead(ki1,pkI,hi0)
+        hi1   = h(<hi0,astat>)
         ci2   = h(<ci1,sisr,'1'>)
         ki2   = h(<ci1,sisr,'2'>)
-        ats   = aead(kif,~ts,hi2)
+        ats   = aead(ki2,~ts,hi1)
         hi2   = h(<hi1,ats>)
-        m1    = <'1',~sidI,'g'^~ekI,astat,ats,$mac1,$mac2> in //TODO:Model MACs
+        m1    = <'1',~sidI,pekI,astat,ats,$mac1,$mac2> in //TODO:Model MACs
     [ //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(~inj,~ltkI,pkR,sisr,~psk,anything)
+      State(~id,~psk,anything)
+    , !StateInvariants(~id,~ltkI,pkR,sisr)
+    , !AgentPSK(~psk)
     , Fr(~sidI)
     , Fr(~ekI)
     , Fr(~ts)
     ]--[
-      Binding(~inj,~ltkI,pkR)
+      StartHandshake(pkI,pkR,pekI,~psk,~sidI)
+    , UsingPSK(~psk)
     ]->
     [ //We cache DH sisr to reduce variant precomputation time for tamarin.
-      State(~inj,~ltkI,pkR,sisr,~psk,<'init',~sidI,~ekI,cif,kif,hif>)
+      State(~id,~psk,<'init',~sidI,~ekI,ci2,ki2,hi2>)
     , Out(m1)
     ]
-*/
-/*
+
 rule Handshake_RespPSK:
-    let cri = h('nopsk')
-        eisr = pekI^~ltkR
-        eier = pekI^~ekR
-        sier = pkI^~ekR
-        hr0 = h(<cri,'id','g'^~ltkR,pekI>)  //No PSK means no intermediate hashes necessary here
-        kr0 = h(<cri,eisr,'2'>)
-        cr0 = h(<cri,eisr,'1'>)
-        altk= aead(kr0,pkI,hr0)
-        hr1 = h(<hr0,altk>)
-        kr1 = h(<cr0,sisr,'2'>)
-        cr1 = h(<cr0,sisr,'1'>)
-        ats = aead(kr1,ts,hr1)
-        hr2 = h(<hr1,ats>)
-        m1  = <'1',sidI,pekI,altk,ats,$mac1,$mac2> //TODO:Model MACs
-        hr3 = h(<hr2,'g'^~ekR>)
-        kr2 = h(<cr1,eier,'2'>)
-        cr2 = h(<cr1,eier,'1'>)
-        kr3 = h(<cr2,sier,'2'>)
-        cr3 = h(<cr2,sier,'1'>)
-        aemp= aead(kr3,'0',hr3)
-        hr4 = h(<hr3,aemp>)
-        m2  = <'2',sidI,~sidR,'g'^~ekR,aemp,$mac1,$mac2> in
-    [ State(~inj,~ltkR,pkI,sisr,'nopsk',anything)
+    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,hr0)
+        hr1   = h(<hr0,astat>)
+        cr2   = h(<cr1,sisr,'1'>)
+        kr2   = h(<cr1,sisr,'2'>)
+        ats   = aead(kr2,~ts,hi2)
+        hr2   = h(<hr1,ats>)
+        m1    = <'1',sidI,pekI,astat,ats,$mac1,$mac2> //TODO:Model MACs
+        //Constructing the response message m2:
+        cr3   = h(<cr2,pekR,'1'>)
+        kr3   = h(<cr2,pekR,'2'>)
+        hr3   = h(<hr2,pekR>)
+        cr4   = h(<cr2,eier,'1'>)
+        kr4   = h(<cr2,eier,'2'>)
+        cr5   = h(<cr2,sier,'1'>)
+        kr5   = h(<cr2,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)
     ]--[
-      Binding(~inj,~ltkR,pkI)
-    , RespKeys(sisr,eier,cr3) //Not actually cr3, but derived from it.
+      RKeys(<pkI,pkR,pekI,pekR,~psk,cr5>) //Not actually cr, but derived from it.
+    , UsingPSK(~psk)
+    , RSessionID(sidI,~sidR)
     ]->
-    [ State(~inj,~ltkR,pkI,sisr,'nopsk',<'transport',cr3>)
+    [ State(~id,~psk,<'transport',cr3>)
     , Out(m2)
     ]
 
 rule Handshake_CompletePSK:
-    let eier = pekR^~ekI
-        sier = pekR^~ltkI
-        hi3 = h(<hi2,pekR>)
-        ki2 = h(<ci1,eier,'2'>)
-        ci2 = h(<ci1,eier,'1'>)
-        ki3 = h(<ci2,sier,'2'>)
-        ci3 = h(<ci2,sier,'1'>)
-        aemp= aead(ki3,'0',hi3)
-        hi4 = h(<hi3,aemp>)
-        m2  = <'2',sidI,sidR,pekR,aemp,$mac1,$mac2> in
-    [ State(~inj,~ltkI,pkR,sisr,'nopsk',<'init',sidI,~ekI,ci1,ki1,hi2>)
+    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>)
+        ci4   = h(<ci2,eier,'1'>)
+        ki4   = h(<ci2,eier,'2'>)
+        ci5   = h(<ci2,sier,'1'>)
+        ki5   = h(<ci2,sier,'2'>)
+        aempt = aead(ki5,'0',hi3)
+        hi5   = h(<hi3,aempt>)
+        m2    = <'2',sidI,sidR,pekR,aempt,$mac1,$mac2> in
+    [ State(~id,~psk,<'init',sidI,~ekI,ci2,ki2,hi2>)
+    , !StateInvariants(~id,~ltkI,pkR,sisr)
+    , !AgentPSK(~psk)
     , In(m2)
     ]--[
-      Binding(~inj,~ltkI,pkR)
-    , InitKeys(sisr,eier,ci3) //Not actually ci3, but derived from it.
+      IKeys(<pkI,pkR,pekI,pekR,~psk,ci5>) //Not actually ci, but derived from it.
+    , UsingPSK(~psk)
+    , ISessionID(sidI,sidR)
     ]->
-    [ State(~inj,~ltkI,pkR,sisr,'nopsk',<'transport',ci3>)
+    [ State(~id,~psk,<'transport',ci3>)
     ]
-*/
 
 /////////////////////////////////////////////////////////////////////////////
 
-lemma exists_session: exists-trace
-    "Ex pki pkr ck #i #j.
-        InitKeys(pki,pkr,ck) @ i & RespKeys(pkr,pki,ck) @ j & #j < #i"
+lemma exists_session_nopsk: exists-trace
+    "Ex pki pkr peki pekr ck #i #j.
+        IKeys(<pki,pkr,peki,pekr,'nopsk',ck>) @ i 
+        & RKeys(<pki,pkr,peki,pekr,'nopsk',ck>) @ j & #j < #i"
 
-//There are only three numbers, 0, 1, and infinity. 2 isn't 0 or 1 
-//so it must be infinity. Note this takes a very long time to prove.
-lemma exists_two_sessions: exists-trace
-    "Ex pki pkr ck ck2 #i #j #i2 #j2.
-        InitKeys(pki,pkr,ck) @ i & RespKeys(pkr,pki,ck) @ j & #j < #i
-        & InitKeys(pki,pkr,ck2) @ i2 & RespKeys(pkr,pki,ck2) @ j2 & #j2 < #i2
-        & #i < #i2 & not(ck = ck2)"
+// 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.
+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
+        & RKeys(<pki,pkr,peki,pekr,psk,ck>) @ j & #j < #i"
 
-lemma state_invariant[reuse,use_induction]:
-    "All inj ka kb #i.
-        Binding(inj,ka,kb) @ i ==> Ex #j. Paired(inj,ka,kb) @ j & #j < #i"
+//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
+        & RKeys(<pki,pkr,sesskeys>) @ j & #j < #i
+        & IKeys(<pki,pkr,sesskeys2>) @ i2 & RKeys(<pki,pkr,sesskeys2>) @ j2 & #j2 < #i2
+        & #i < #i2 & not(sesskeys = sesskeys2)"
 
 lemma key_secrecy:
-    "(All pki pkr ck #i.
-        InitKeys(pki,pkr,ck) @ i ==> not(Ex #j. K(ck) @ j))
-    &(All pki pkr ck #i.
-        RespKeys(pkr,pki,ck) @ i ==> not(Ex #j. K(ck) @ j))"
+    "(All pki pkr peki pekr ck #i.
+        IKeys(<pki,pkr,peki,pekr,ck>) @ i ==> not(Ex #j. K(ck) @ j))
+    &(All pki pkr peki pekr ck #i.
+        RKeys(<pki,pkr,peki,pekr,ck>) @ i ==> not(Ex #j. K(ck) @ j))"
 
 lemma agreement[reuse]:
-    "All pki pkr ck #i.
-        InitKeys(pki,pkr,ck) @ i
-    ==> Ex #j. #j < #i & RespKeys(pkr,pki,ck) @ j"
+    "All keys #i.
+        IKeys(keys) @ i ==> Ex #j. #j < #i & RKeys(keys) @ j"
 
 //This follows immediately from agreement, since the agreed ck includes 
 //at least one fresh term
-lemma injective_agreement:
-    "All pki pkr ck #i #j.
-        InitKeys(pki,pkr,ck) @ i & RespKeys(pkr,pki,ck) @ j
-    ==> not(Ex #k. RespKeys(pkr,pki,ck) @ k & not(#k = #j))"
+lemma injective_agreement_I:
+    "All pki pkr peki pekr ck #i #j.
+        IKeys(<pki,pkr,peki,pekr,ck>) @ i & RKeys(<pki,pkr,peki,pekr,ck>) @ j
+    ==> not(Ex peki2 pekr2 #k. RKeys(<pki,pkr,peki2,pekr2,ck>) @ k & not(#k = #j))"
+
 end
 
 // vim: ft=spthy