Minor updates to terms for ease of use, and preparation for adding PSK mode. Everything but injective agreement proves automatically

1 files changed, 120 insertions, 53 deletions

diff --git a/wireguard.m4 b/wireguard.m4
index bbc06a7..1822028 100644
--- a/wireguard.m4
+++ b/wireguard.m4
@@ -13,71 +13,101 @@ theory WireGuard
 begin
 
 builtins: hashing, diffie-hellman
-functions: aead/4, decrypt/2
-equations: decrypt(aead(k,n,p,a),k) = p     //Plaintext can be recovered using the key
-
-//Uncomment these to prevent any adversary message modifications
+//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.
+functions: aead/3, decrypt/2
+equations: decrypt(aead(k,p,a),k) = p     //Plaintext can be recovered using the key
+
+//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($*))
 
-dnl define(State,F_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 id1 id2 pka pkb #i #j.
-        Paired(id1,pka,pkb) @ i & Paired(id2,pka,pkb) @ j
+    "All inj inj2 ka pkb #i #j.
+        Paired(inj,ka,pkb) @ i & Paired(inj2,ka,pkb) @ j
     ==> #i = #j"
 
-rule KeyGen:
+//Keygen is separate from pairing to allow keys to be paired
+//more than once (if they were generated fresh in the pairing
+//this would not be possible)
+rule AgentKeyGen:
     [ Fr(~ltk) ]
-    --[Key(~ltk)]->
+    --[DHKey(~ltk)]->
     [!AgentKey(~ltk), Out('g'^~ltk)]
 
-rule ExchangePublicKeys:
+//Semi-malicious or ignorant agents might share
+//a PSK with multiple parties, so we'll overapproximate this
+//by allowing it to be shared 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:
+    [ Fr(~psk) ]
+    --[PSKey(~psk)]->
+    [ !AgentPSK(~psk) ]
+
+//Models an agent adding anothers public key out-of-band.
+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)
     ]--[
-      Paired(~inj, 'g'^~ltkA, 'g'^~ltkB)
-    , Paired(~inj, 'g'^~ltkB, 'g'^~ltkA)
+      Paired(~inj,~ltkA, pkB)
     , InEq($A,$B)
     ]->
-    [ State(~inj, ~ltkA, 'g'^~ltkB, ('g'^~ltkA)^~ltkB, '0')
-    , State(~inj, ~ltkB, 'g'^~ltkA, ('g'^~ltkA)^~ltkB, '0')
+    [ //We cache the static-static to reduce the time needed for
+      //variant precomputations in tamarin.
+      State(~inj,~ltkA, pkB, pkB^~ltkA, 'nopsk', '0')
     ]
 
-/* Uncomment to allow long term key compromise
+/* Uncomment to allow various key compromises
  rule CompromiseKey:
-      [!AgentKey($Agent,ltk)]
-      --[ Compromise($Agent,ltk) ]->
-      [Out(ltk)]
+    [!AgentKey(ltk)]
+    --[ CompromiseLTK(ltk) ]->
+    [Out(ltk)]
+
+rule CompromisePSK:
+    [!AgentPSK(psk)]
+    --[ CompromisePSK(psk) ]->
+    [Out(psk)]
 */
 
 // MESSAGE RULES
 rule Handshake_InitNoPSK:
-    let cii = h('nopsk')
+    let eisr= pkR^~ekI
+        cii = h('nopsk')
         hi0 = h(<cii,'id',pkR,'g'^~ekI>)  //No PSK means no intermediate hashes necessary here
-        ki0 = h(<cii,pkR^~ekI,'2'>)
-        ci0 = h(<cii,pkR^~ekI,'1'>)
-        altk= aead(ki0,'0','g'^~ltkI,hi0)
+        ki0 = h(<cii,eisr,'2'>)
+        ci0 = h(<cii,eisr,'1'>)
+        altk= aead(ki0,'g'^~ltkI,hi0)
         hi1 = h(<hi0,altk>)
         ki1 = h(<ci0,sisr,'2'>)
         ci1 = h(<ci0,sisr,'1'>)
-        ats = aead(ki1,'0',~ts,hi1)
+        ats = aead(ki1,~ts,hi1)
         hi2 = h(<hi1,ats>)
         m1  = <'1',~sidI,'g'^~ekI,altk,ats,$mac1,$mac2> in //TODO:Model MACs
-    [ State(inj,~ltkI,pkR,sisr,anything)
+    [ //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)
     , Fr(~sidI)
     , Fr(~ekI)
     , Fr(~ts)
     ]--[
-      Binding(inj,'g'^~ltkI,pkR)
-    , HandshakeInit('g'^~ltkI, pkR, hi2)
+      Binding(~inj,~ltkI,pkR)
+//    , HandshakeInit('g'^~ltkI, pkR, hi2)
     ]->
-    [ State(inj,~ltkI,pkR,sisr,<'init',~sidI,~ekI,ci1,ki1,hi2>)
+    [ //We cache DH sisr to reduce variant precomputation time for tamarin.
+      State(~inj,~ltkI,pkR,sisr,'nopsk',<'init',~sidI,~ekI,ci1,ki1,hi2>)
     , Out(m1)
     ]
 
@@ -89,11 +119,11 @@ rule Handshake_RespNoPSK:
         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,'0',pkI,hr0)
+        altk= aead(kr0,pkI,hr0)
         hr1 = h(<hr0,altk>)
         kr1 = h(<cr0,sisr,'2'>)
         cr1 = h(<cr0,sisr,'1'>)
-        ats = aead(kr1,'0',ts,hr1)
+        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>)
@@ -101,19 +131,18 @@ rule Handshake_RespNoPSK:
         cr2 = h(<cr1,eier,'1'>)
         kr3 = h(<cr2,sier,'2'>)
         cr3 = h(<cr2,sier,'1'>)
-        aemp= aead(kr3,'0','0',hr3)
+        aemp= aead(kr3,'0',hr3)
         hr4 = h(<hr3,aemp>)
         m2  = <'2',sidI,~sidR,'g'^~ekR,aemp,$mac1,$mac2> in
-    [ State(inj,~ltkR,pkI,sisr,anything)
+    [ State(~inj,~ltkR,pkI,sisr,'nopsk',anything)
     , Fr(~ekR)
     , Fr(~sidR)
     , In(m1)
     ]--[
-      Binding(inj,pkI,'g'^~ltkR)
-    , HandshakeResp(pkI,'g'^~ltkR,hr2,hr4)
-    , RespTransportKeys(pkI,'g'^~ltkR,cr3) //Not actually cr3, but derived from it.
+      Binding(~inj,~ltkR,pkI)
+    , RespKeys(sisr,eier,cr3) //Not actually cr3, but derived from it.
     ]->
-    [ State(inj,~ltkR,pkI,sisr,<'resp',cr3>)
+    [ State(~inj,~ltkR,pkI,sisr,'nopsk',<'transport',cr3>)
     , Out(m2)
     ]
 
@@ -125,38 +154,76 @@ rule Handshake_CompleteNoPSK:
         ci2 = h(<ci1,eier,'1'>)
         ki3 = h(<ci2,sier,'2'>)
         ci3 = h(<ci2,sier,'1'>)
-        aemp= aead(ki3,'0','0',hi3)
+        aemp= aead(ki3,'0',hi3)
         hi4 = h(<hi3,aemp>)
         m2  = <'2',sidI,sidR,pekR,aemp,$mac1,$mac2> in
-    [ State(inj,~ltkI,pkR,sisr,<'init',sidI,~ekI,ci1,ki1,hi2>)
+    [ State(~inj,~ltkI,pkR,sisr,'nopsk',<'init',sidI,~ekI,ci1,ki1,hi2>)
     , In(m2)
     ]--[
-      Binding(inj,'g'^~ltkI,pkR)
-    , InitTransportKeys('g'^~ltkI,pkR,ci3) //Not actually ci3, but derived from it.
+      Binding(~inj,~ltkI,pkR)
+    , InitKeys(sisr,eier,ci3) //Not actually ci3, but derived from it.
     ]->
-    [ State(inj,~ltkI,pkR,sisr,<'init',ci3>)
+    [ State(~inj,~ltkI,pkR,sisr,'nopsk',<'transport',ci3>)
     ]
 
 /////////////////////////////////////////////////////////////////////////////
+//      PSK Mode (NYI)
+/////////////////////////////////////////////////////////////////////////////
+/*
+rule SwitchtoPSK:
+    [ State(inj,~ltka,pkb,sisr,'nopsk',anything)
+    , !AgentPSK(~psk)
+    ]--[
+      Binding(~inj,~ltka,pkb)
+    , AddPSK(~ltka,pkb,~psk)
+    ]->
+    [ State(inj,~ltka,pkb,sisr,~psk,anything)
+    ]
+
+rule RemovePSK:
+    [ State(inj,ltka,pkb,sisr,~psk,anything)
+    ]--[
+      Binding(~inj,ltka,pkb)
+    , RemovePSK(~ltka,pkb,~psk)
+    ]->
+    [ State(inj,ltka,pkb,sisr,'nopsk',anything)
+    ]
+
+*/
+
+/////////////////////////////////////////////////////////////////////////////
 
 lemma exists_session: exists-trace
-    "Ex a b ck #i #j.
-        InitTransportKeys(a,b,ck) @ i & RespTransportKeys(a,b,ck) @ j & #j < #i"
+    "Ex sisr eka ekb ck #i #j.
+        InitKeys(sisr,eka,ck) @ i & RespKeys(sisr,ekb,ck) @ j & #j < #i"
 
 lemma state_invariant[reuse,use_induction]:
-    "All inj pka pkb #i.
-        Binding(inj,pka,pkb) @ i ==> Ex #j. Paired(inj,pka,pkb) @ j & #j < #i"
-
+    "All inj ka pkb #i.
+        Binding(inj,ka,pkb) @ i ==> Ex #j. Paired(inj,ka,pkb) @ j & #j < #i"
+/*
+lemma K_ck_implies_K_ephemeral[reuse,use_induction]:
+    "(All sisr ek ck #i #j.
+        InitKeys(sisr,ek,ck) @ i & K(ck) @ j
+    ==> Ex #k. #k < #j & KU(ek) @ k)
+    &(All sisr ek ck #i #j.
+        RespKeys(sisr,ek,ck) @ i & K(ck) @ j
+    ==> Ex #k. #k < #j & KU(ek) @ k)"
+*/
 lemma key_secrecy:
-    "(All a b ck #i.
-        InitTransportKeys(a,b,ck) @ i ==> not(Ex #j. K(ck) @ j))
-    &(All a b ck #i.
-        RespTransportKeys(a,b,ck) @ i ==> not(Ex #j. K(ck) @ j))"
+    "(All sisr ek ck #i.
+        InitKeys(sisr,ek,ck) @ i ==> not(Ex #j. K(ck) @ j))
+    &(All sisr ek ck #i.
+        RespKeys(sisr,ek,ck) @ i ==> not(Ex #j. K(ck) @ j))"
+
+lemma agreement[reuse]:
+    "All sisr eier ck #i.
+        InitKeys(sisr,eier,ck) @ i 
+    ==> Ex #j. #j < #i & RespKeys(sisr,eier,ck) @ j"
 
 lemma injective_agreement:
-    "All a b ck #i #j.
-        InitTransportKeys(a,b,ck) @ i & RespTransportKeys(a,b,ck) @ j
-    ==> #j < #i & not(Ex #k. RespTransportKeys(a,b,ck) @ k & not(#k = #j))"
+    "All sisr eier ck #i #j.
+        InitKeys(sisr,eier,ck) @ i & RespKeys(sisr,eier,ck) @ j 
+    ==> not(Ex #k. RespKeys(sisr,eier,ck) @ k & not(#k = #j))"
 end
 
 // vim: ft=spthy