Change of agreement property and compromise model

1 files changed, 31 insertions, 8 deletions

diff --git a/wireguard.m4 b/wireguard.m4
index c34b92c..bfc69dc 100644
--- a/wireguard.m4
+++ b/wireguard.m4
@@ -55,6 +55,16 @@ rule PSKKeyGen:
     --[PSKey(~psk)]->
     [ !AgentPSK(~psk) ]
 
+/* Key Reveals for the eCK model */
+rule PSK_reveal: 
+   [ !AgentPSK(k) ] --[ Reveal_PSK(k) ]-> [ Out(k) ]
+
+rule AgentKey_reveal:
+   [ !AgentKey(k) ] --[ Reveal_AK('g'^k) ]-> [ Out(k) ]
+
+rule EphKey_reveal:
+   [ !EphKey(k) ] --[ Reveal_EphK('g'^k) ]-> [ Out(k) ]
+
 //Models an agent adding anothers public key out-of-band.
 rule AddPublicKey:
     let pkB = 'g'^~ltkB in
@@ -115,6 +125,7 @@ rule Handshake_Init:
     [ //We cache DH sisr to reduce variant precomputation time for tamarin.
       State(~id,'nopsk',<'init',~sidI,~ekI,ci1,ki1,hi1>)
     , Out(m1)
+    , !EphKey(~ekI)
     ]
 
 rule Handshake_Resp:
@@ -155,6 +166,7 @@ rule Handshake_Resp:
     ]->
     [ State(~id,'nopsk',<'transport',cr3>)
     , Out(m2)
+    , !EphKey(~ekR)
     ]
 
 rule Handshake_Complete:
@@ -244,6 +256,7 @@ rule Handshake_InitPSK:
     [ //We cache DH sisr to reduce variant precomputation time for tamarin.
       State(~id,~psk,<'init',~sidI,~ekI,ci2,ki2,hi2>)
     , Out(m1)
+    , !EphKey(~ekI)
     ]
 
 rule Handshake_RespPSK:
@@ -293,6 +306,7 @@ rule Handshake_RespPSK:
     ]->
     [ State(~id,~psk,<'transport',cr3>)
     , Out(m2)
+    , !EphKey(~ekR)
     ]
 
 rule Handshake_CompletePSK:
@@ -347,15 +361,24 @@ lemma exists_two_sessions: exists-trace
         & IKeys(<pki,pkr,sesskeys2>) @ i2 & RKeys(<pki,pkr,sesskeys2>) @ j2 & #j2 < #i2
         & #i < #i2 & not(sesskeys = sesskeys2)"
 
+lemma disagreement_implies_Sr_or_SiEi_compromise[reuse]:
+    "All pki pkr peki pekr ck #i.
+        IKeys(<pki,pkr,peki,pekr,ck>) @ i
+        & not(Ex #j. #j < #i & RKeys(<pki,pkr,peki,pekr,ck>) @ j)
+    ==> // Either R's static is compromised
+        (Ex #j. Reveal_AK(pkr) @ j & #j < #i)
+        // Or I is hopelessly broken
+        | (Ex #j #j2. Reveal_AK(pki) @ j & Reveal_EphK(peki) @ j2 & #j2 < #i & #j < #i)"
+
 lemma key_secrecy:
-    "(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 keys #i.
-        IKeys(keys) @ i ==> Ex #j. #j < #i & RKeys(keys) @ j"
+    "(All pki pkr peki pekr ck #i #j.
+        //If the two agents agree on keys
+        IKeys(<pki,pkr,peki,pekr,ck>) @ i & RKeys(<pki,pkr,peki,pekr,ck>) @ j
+    ==> //Either the adversary doesn't know the keys
+        not(Ex #j. K(ck) @ j) 
+        //Or a pair of keys from the same agent were revealed
+        | (Ex #j #j2. Reveal_AK(pki) @ j & Reveal_EphK(peki) @ j2)
+        | (Ex #j #j2. Reveal_AK(pkr) @ j & Reveal_EphK(pekr) @ j2))"
 
 //This follows immediately from agreement, since the agreed ck includes 
 //at least one fresh term