PSK mode readded

1 files changed, 72 insertions, 50 deletions

diff --git a/wireguard.m4 b/wireguard.m4
index 9123eff..dfe23ee 100644
--- a/wireguard.m4
+++ b/wireguard.m4
@@ -66,6 +66,9 @@ rule PSKKeyGen:
     --[PSKey(~psk)]->
     [ !AgentPSK(~psk) ]
 
+rule NoPSKMode:
+    []--[PSKey('nopsk')]->[!AgentPSK('nopsk')]
+
 /* Key Reveals for our adversary model */
 rule PSK_reveal: 
    [ !AgentPSK(k) ] --[ Reveal_PSK(k) ]-> [ Out(k) ]
@@ -83,6 +86,7 @@ rule AddPublicKey:
     let pkB = 'g'^~ltkB in
     [ !AgentKey(~ltkA)
     , !AgentKey(~ltkB)
+    , !AgentPSK('nopsk')
     , Fr(~id)
     ]--[]->
     [ // For search efficiency, state is divided into
@@ -90,10 +94,17 @@ rule AddPublicKey:
       // allows tamarin to immediately bind the keys back
       // to this initial pairing rule. The fresh ~id is used
       // to identify this pairing.
-      State(~id, 'nopsk', 'nostate')
+      State(~id,'nopsk','NoMessageState')
     , !StateInvariants(~id, ~ltkA, pkB, pkB^~ltkA)
     ]
 
+rule ChangePSK:
+    [ State(~id,oldpsk,anything)
+    , !AgentPSK(psk)
+    ]--[]->
+    [ State(~id,psk,'NoMessageState')
+    ]
+
 // MESSAGE RULES
 rule Handshake_Init:
     let pkI   = 'g'^~ltkI
@@ -115,19 +126,21 @@ rule Handshake_Init:
     [ //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,psk,anything)
     , !StateInvariants(~id, ~ltkI, pkR, sisr)
     , Fr(~sidI)
     , Fr(~ekI)
     // The pkISurrogate is used later to approximate identity hiding.
     , Fr(~pkISurrogate)
-    ]--[]->
+    ]--[
+      UsingPSK(psk)
+    ]->
     [ //We cache DH sisr to reduce variant precomputation time for tamarin.
-      State(~id,'nopsk',<'init',~sidI,~ekI,ci2,ki2,hi1>)
+      State(~id,psk,<'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,ci2,ki2,hi1>)
+    , F_SolveInit(~id,psk,<'init',~sidI,~ekI,ci2,ki2,hi1>)
     , Out(m1)
     ]
 
@@ -155,26 +168,27 @@ rule Handshake_Resp:
         hr2   = h(<hr1,pekR>)
         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
-        hrt   = h(<cr5,'nopsk','2'>)
-        kr6   = h(<cr5,'nopsk','3'>)
+        cr6   = h(<cr5,psk,'1'>) //TODO: replace 'nopsk' with actual psk, maybe revealed maybe not
+        hrt   = h(<cr5,psk,'2'>)
+        kr6   = h(<cr5,psk,'3'>)
         hr3   = h(<hr2,hrt>)
         aempt = aead(kr6,'e',hr3)
         hr4   = h(<hr3,aempt>)
         m2    = <'2',sidI,~sidR,pekR,aempt,$mac1,$mac2> in
-    [ State(~id,'nopsk',anything)
+    [ State(~id,psk,anything)
     , !StateInvariants(~id,~ltkR,pkI,sisr)
     , Fr(~ekR)
     , Fr(~sidR)
     , In(m1)
     ]--[
-      RKeys(<pkI,pkR,pekI,pekR,'nopsk',cr6>) //Not actually cr6, but derived from it.
+      RKeys(<pkI,pkR,pekI,pekR,psk,cr6>) //Not actually cr6, but derived from it.
     , Identity_Surrogate(pkISurrogate)
+    , UsingPSK(psk)
     ]->
-    [ State(~id,'nopsk',<'transport_unconfirmed',~sidR,pekI,pekR,cr6>)
+    [ State(~id,psk,<'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,cr6>)
+    , F_SolveResp(~id,psk,<'transport_unconfirmed',~sidR,pekI,pekR,cr6>)
     , !EphKeytoReveal(~ekR)
     , Out(m2)
     ]
@@ -189,9 +203,9 @@ rule Handshake_Complete:
         hi2   = h(<hi1,pekR>)
         ci4   = h(<ci3,eier,'1'>)
         ci5   = h(<ci4,sier,'1'>)
-        ci6   = h(<ci5,'nopsk','1'>) //TODO: see note above about using real psk instead of 'nopsk'
-        hit   = h(<ci5,'nopsk','2'>)
-        ki6   = h(<ci5,'nopsk','3'>)
+        ci6   = h(<ci5,psk,'1'>) //TODO: see note above about using real psk instead of 'nopsk'
+        hit   = h(<ci5,psk,'2'>)
+        ki6   = h(<ci5,psk,'3'>)
         hi3   = h(<hi2,hit>)
         aempt = aead(ki6,'e',hi3)
         hi4   = h(<hi3,aempt>)
@@ -199,14 +213,15 @@ rule Handshake_Complete:
         //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,'nopsk',<'init',sidI,~ekI,ci2,ki2,hi1>)
-    , F_SolveInit(~id,'nopsk',<'init',sidI,~ekI,ci2,ki2,hi1>)
+    [ State(~id,psk,<'init',sidI,~ekI,ci2,ki2,hi1>)
+    , F_SolveInit(~id,psk,<'init',sidI,~ekI,ci2,ki2,hi1>)
     , !StateInvariants(~id,~ltkI,pkR,sisr)
     , In(m2)
     ]--[
-      IKeys(<pkI,pkR,pekI,pekR,'nopsk',ci6>) //Not actually ci6, but derived from it.
+      IKeys(<pkI,pkR,pekI,pekR,psk,ci6>) //Not actually ci6, but derived from it.
+    , UsingPSK(psk)
     ]->
-    [ State(~id,'nopsk',<'transport',sidI,ci3>)
+    [ State(~id,psk,<'transport',sidI,ci3>)
     , Out(mtr)
     ]
 
@@ -274,26 +289,6 @@ lemma R_disagreement_implies_Si_or_SrEr_compromise[reuse]:
         //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 disagreement_implies_noPSK_or_compromisedPSK[reuse]:
-    "(All pki pkr peki pekr psk ck #i.
-        //If I believes they have completed a handshake with R
-        IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i
-        //but R does not have a matching session
-        & not(Ex #j. #j < #i & RKeys(<pki,pkr,peki,pekr,psk,ck>) @ j)
-    ==> //Then either they aren't in PSK mode
-        (psk = 'nopsk')
-        //Or the adversary compromised the PSK before the session 
-        | (Ex #j. #j < #i & Reveal_PSK(psk) @ j))
-    &(All pki pkr peki pekr psk ck #i.
-        //If R believes they have a confirmed session with I 
-        RConfirm(<pki,pkr,peki,pekr,psk,ck>) @ i
-        //but I does not have a matching session
-        & not(Ex #j. #j < #i & IKeys(<pki,pkr,peki,pekr,psk,ck>) @ j)
-    ==> //Then either they aren't in PSK mode
-        (psk = 'nopsk')
-        //Or the adversary compromised the PSK before the session 
-        | (Ex #j. #j < #i & Reveal_PSK(psk) @ j))"
-
 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
@@ -309,17 +304,6 @@ lemma session_uniqueness:
 // All autoprove, but key_secrecy takes forever
 /////////////////////////////////////////////////////////////////////////////
 
-lemma secrecy_without_psk_compromise:
-   "(All pki pkr peki pekr psk ck #i #j.
-        //If the adversary ever knows a session key that I derived from a handshake
-        IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i & K(ck) @ j
-    ==> //Then either the adversary revealed the PSK, or there was no PSK
-        (Ex #j2. Reveal_PSK(psk) @ j2) | (psk = 'nopsk'))
-    //& similarly for R
-    &(All pki pkr peki pekr psk ck #i #j.
-        RConfirm(<pki,pkr,peki,pekr,psk,ck>) @ i & K(ck) @ j
-    ==> (Ex #j2. Reveal_PSK(psk) @ j2) | (psk = 'nopsk'))"
-
 lemma key_secrecy[reuse]:
     "(All pki pkr peki pekr psk ck #i #i2.
         //If I and R agree on keys
@@ -342,5 +326,43 @@ lemma identity_hiding:
     ==> //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)"
 
+//////// PSK PROPERTIES /////////////////////////////////////////////////////
+// These require a helper lemma that slows down the things above.
+/////////////////////////////////////////////////////////////////////////////
+
+lemma psk_invariant_helper[reuse,use_induction]:
+    "All psk #i. UsingPSK(psk) @ i ==> Ex #j. #j < #i & PSKey(psk) @ j"
+
+lemma disagreement_implies_noPSK_or_compromisedPSK[reuse]:
+    "(All pki pkr peki pekr psk ck #i.
+        //If I believes they have completed a handshake with R
+        IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i
+        //but R does not have a matching session
+        & not(Ex #j. #j < #i & RKeys(<pki,pkr,peki,pekr,psk,ck>) @ j)
+    ==> //Then either they aren't in PSK mode
+        (psk = 'nopsk')
+        //Or the adversary compromised the PSK before the session 
+        | (Ex #j. #j < #i & Reveal_PSK(psk) @ j))
+    &(All pki pkr peki pekr psk ck #i.
+        //If R believes they have a confirmed session with I 
+        RConfirm(<pki,pkr,peki,pekr,psk,ck>) @ i
+        //but I does not have a matching session
+        & not(Ex #j. #j < #i & IKeys(<pki,pkr,peki,pekr,psk,ck>) @ j)
+    ==> //Then either they aren't in PSK mode
+        (psk = 'nopsk')
+        //Or the adversary compromised the PSK before the session 
+        | (Ex #j. #j < #i & Reveal_PSK(psk) @ j))"
+
+lemma secrecy_without_psk_compromise:
+   "(All pki pkr peki pekr psk ck #i #j.
+        //If the adversary ever knows a session key that I derived from a handshake
+        IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i & K(ck) @ j
+    ==> //Then either the adversary revealed the PSK, or there was no PSK
+        (Ex #j2. Reveal_PSK(psk) @ j2) | (psk = 'nopsk'))
+    //& similarly for R
+    &(All pki pkr peki pekr psk ck #i #j.
+        RConfirm(<pki,pkr,peki,pekr,psk,ck>) @ i & K(ck) @ j
+    ==> (Ex #j2. Reveal_PSK(psk) @ j2) | (psk = 'nopsk'))"
+
 end
 // vim: ft=spthy