More efficiency changes to reduce DH variant computations. Injective agreement now proves directly from agreement

1 files changed, 170 insertions, 68 deletions

diff --git a/wireguard.m4 b/wireguard.m4
index 1822028..fe98795 100644
--- a/wireguard.m4
+++ b/wireguard.m4
@@ -13,8 +13,8 @@ theory WireGuard
 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, 
+//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
@@ -25,13 +25,15 @@ equations: decrypt(aead(k,p,a),k) = p     //Plaintext can be recovered using the
 dnl define(In, AuthenticatedMessage($*))
 dnl define(Out, AuthenticatedMessage($*))
 
+define(AgentKey, F_AgentKey($*))
+
 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 pkb #i #j.
-        Paired(inj,ka,pkb) @ i & Paired(inj2,ka,pkb) @ j
+    "All inj inj2 ka kb #i #j.
+        Paired(inj,ka,kb) @ i & Paired(inj2,ka,kb) @ j
     ==> #i = #j"
 
 //Keygen is separate from pairing to allow keys to be paired
@@ -82,19 +84,20 @@ rule CompromisePSK:
 */
 
 // MESSAGE RULES
-rule Handshake_InitNoPSK:
-    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,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,~ts,hi1)
-        hi2 = h(<hi1,ats>)
-        m1  = <'1',~sidI,'g'^~ekI,altk,ats,$mac1,$mac2> in //TODO:Model MACs
+rule Handshake_Init:
+    let 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
+        ki0   = h(<cii,eisr,'2'>)
+        ci0   = h(<cii,eisr,'1'>)
+        astat = aead(ki0,'g'^~ltkI,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
     [ //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.
@@ -104,14 +107,135 @@ rule Handshake_InitNoPSK:
     , Fr(~ts)
     ]--[
       Binding(~inj,~ltkI,pkR)
-//    , HandshakeInit('g'^~ltkI, pkR, hi2)
+    , EphemeralKey(~ekI)
     ]->
     [ //We cache DH sisr to reduce variant precomputation time for tamarin.
-      State(~inj,~ltkI,pkR,sisr,'nopsk',<'init',~sidI,~ekI,ci1,ki1,hi2>)
+      State(~inj,~ltkI,pkR,sisr,'nopsk',<'init',~sidI,~ekI,ci1,ki1,hi1>)
     , Out(m1)
     ]
 
-rule Handshake_RespNoPSK:
+rule Handshake_Resp:
+    let 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
+        kr0   = h(<cri,eisr,'2'>)
+        cr0   = h(<cri,eisr,'1'>)
+        astat = aead(kr0,pkI,hri)
+        hr0   = h(<hri,astat>)
+        kr1   = h(<cr0,sisr,'2'>)
+        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
+        //Constructing the response message m2:
+        hr2   = h(<hr1,'g'^~ekR>)
+        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)
+    , 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.
+    ]->
+    [ State(~inj,~ltkR,pkI,sisr,'nopsk',<'transport',cr3>)
+    , Out(m2)
+    ]
+
+rule Handshake_Complete:
+    let 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> in
+    [ State(~inj,~ltkI,pkR,sisr,'nopsk',<'init',sidI,~ekI,ci1,ki1,hi1>)
+    , In(m2)
+    ]--[
+      Binding(~inj,~ltkI,pkR)
+    , AEADIncludesKey(aempt,eier)
+    , InitKeys('g'^~ltkI,pkR,ci3) //Not actually ci3, but derived from it.
+    ]->
+    [ State(~inj,~ltkI,pkR,sisr,'nopsk',<'transport',ci3>)
+    ]
+
+/////////////////////////////////////////////////////////////////////////////
+//      PSK Mode 
+// (NYI, most of these rules are currently copy paste from above)
+/////////////////////////////////////////////////////////////////////////////
+/*
+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)
+    ]
+
+// MESSAGE RULES WITH PSK
+rule Handshake_InitPSK:
+    let 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>)
+        ci1   = h(<ci0,eisr,'1'>)
+        ki1   = h(<ci0,eisr,'2'>)
+        astat = aead(ki1,'g'^~ltkI,hi0)
+        hi1   = h(<hi1,astat>)
+        ci2   = h(<ci1,sisr,'1'>)
+        ki2   = h(<ci1,sisr,'2'>)
+        ats   = aead(kif,~ts,hi2)
+        hi2   = h(<hi1,ats>)
+        m1    = <'1',~sidI,'g'^~ekI,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)
+    , Fr(~sidI)
+    , Fr(~ekI)
+    , Fr(~ts)
+    ]--[
+      Binding(~inj,~ltkI,pkR)
+    ]->
+    [ //We cache DH sisr to reduce variant precomputation time for tamarin.
+      State(~inj,~ltkI,pkR,sisr,~psk,<'init',~sidI,~ekI,cif,kif,hif>)
+    , Out(m1)
+    ]
+*/
+/*
+rule Handshake_RespPSK:
     let cri = h('nopsk')
         eisr = pekI^~ltkR
         eier = pekI^~ekR
@@ -146,7 +270,7 @@ rule Handshake_RespNoPSK:
     , Out(m2)
     ]
 
-rule Handshake_CompleteNoPSK:
+rule Handshake_CompletePSK:
     let eier = pekR^~ekI
         sier = pekR^~ltkI
         hi3 = h(<hi2,pekR>)
@@ -165,65 +289,43 @@ rule Handshake_CompleteNoPSK:
     ]->
     [ 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 sisr eka ekb ck #i #j.
-        InitKeys(sisr,eka,ck) @ i & RespKeys(sisr,ekb,ck) @ j & #j < #i"
+    "Ex pki pkr ck #i #j.
+        InitKeys(pki,pkr,ck) @ i & RespKeys(pkr,pki,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)"
 
 lemma state_invariant[reuse,use_induction]:
-    "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)"
-*/
+    "All inj ka kb #i.
+        Binding(inj,ka,kb) @ i ==> Ex #j. Paired(inj,ka,kb) @ j & #j < #i"
+
 lemma key_secrecy:
-    "(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))"
+    "(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))"
 
 lemma agreement[reuse]:
-    "All sisr eier ck #i.
-        InitKeys(sisr,eier,ck) @ i 
-    ==> Ex #j. #j < #i & RespKeys(sisr,eier,ck) @ j"
+    "All pki pkr ck #i.
+        InitKeys(pki,pkr,ck) @ i
+    ==> Ex #j. #j < #i & RespKeys(pkr,pki,ck) @ j"
 
+//This follows immediately from agreement, since the agreed ck includes 
+//at least one fresh term
 lemma injective_agreement:
-    "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))"
+    "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))"
 end
 
 // vim: ft=spthy