Identity Hiding

1 files changed, 14 insertions, 19 deletions

diff --git a/wireguard.m4 b/wireguard.m4
index eae6f21..d1fca86 100644
--- a/wireguard.m4
+++ b/wireguard.m4
@@ -95,7 +95,7 @@ rule Handshake_Init:
         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,pkI,hii)
+        astat = aead(ki0,<pkI,~pkISurrogate>,hii)
         hi0   = h(<hii,astat>)
         ki1   = h(<ci0,sisr,'2'>)
         ci1   = h(<ci0,sisr,'1'>)
@@ -109,6 +109,7 @@ rule Handshake_Init:
     , !StateInvariants(~id, ~ltkI, pkR, sisr)
     , Fr(~sidI)
     , Fr(~ekI)
+    , Fr(~pkISurrogate)
     ]--[
       StartHandshake(pkI,pkR,pekI,'nopsk',~sidI)
     ]->
@@ -131,7 +132,7 @@ rule Handshake_Resp:
         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)
+        astat = aead(kr0,<pkI,pkISurrogate>,hri)
         hr0   = h(<hri,astat>)
         kr1   = h(<cr0,sisr,'2'>)
         cr1   = h(<cr0,sisr,'1'>)
@@ -155,6 +156,7 @@ rule Handshake_Resp:
     ]--[
       RKeys(<pkI,pkR,pekI,pekR,'nopsk',cr3>) //Not actually cr3, but derived from it.
     , RSessionID(sidI,~sidR)
+    , IIdentity(pkISurrogate)
     ]->
     [ State(~id,'nopsk',<'transport_unconfirmed',~sidR,pekI,pekR,cr3>)
     //Efficiency hack, lets us make this high priority while making state low priority
@@ -233,7 +235,7 @@ rule Handshake_InitPSK:
         hi0   = h(<hii,pekI>)
         ci1   = h(<ci0,eisr,'1'>)
         ki1   = h(<ci0,eisr,'2'>)
-        astat = aead(ki1,pkI,hi0)
+        astat = aead(ki1,<pkI,~pkISurrogate>,hi0)
         hi1   = h(<hi0,astat>)
         ci2   = h(<ci1,sisr,'1'>)
         ki2   = h(<ci1,sisr,'2'>)
@@ -248,6 +250,7 @@ rule Handshake_InitPSK:
     , !AgentPSK(psk)
     , Fr(~sidI)
     , Fr(~ekI)
+    , Fr(~pkISurrogate)
     ]--[
       StartHandshake(pkI,pkR,pekI,psk,~sidI)
     , UsingPSK(psk)
@@ -276,11 +279,11 @@ rule Handshake_RespPSK:
         hr0   = h(<hri,pekI>)
         cr1   = h(<cr0,eisr,'1'>)
         kr1   = h(<cr0,eisr,'2'>)
-        astat = aead(ki1,pkI,hr0)
+        astat = aead(ki1,<pkI,pkISurrogate>,hr0)
         hr1   = h(<hr0,astat>)
         cr2   = h(<cr1,sisr,'1'>)
         kr2   = h(<cr1,sisr,'2'>)
-        ats   = aead(kr2,$ts,hi2)
+        ats   = aead(kr2,$ts,hr1)
         hr2   = h(<hr1,ats>)
         m1    = <'1',sidI,pekI,astat,ats,$mac1,$mac2> //TODO:Model MACs
         //Constructing the response message m2:
@@ -304,6 +307,7 @@ rule Handshake_RespPSK:
       RKeys(<pkI,pkR,pekI,pekR,psk,cr5>) //Not actually cr, but derived from it.
     , UsingPSK(psk)
     , RSessionID(sidI,~sidR)
+    , IIdentity(pkISurrogate)
     ]->
     [ State(~id,psk,<'transport_unconfirmed',~sidR,pekI,pekR,cr5>)
     //Efficiency hack, lets us make this high priority while making state low priority
@@ -440,20 +444,6 @@ lemma injective_agreement:
 // Work in progress
 /////////////////////////////////////////////////////////////////////////////
 
-lemma key_knowledge_helperI[reuse,hide_lemma=disagreement_implies_Sr_or_SiEi_compromise]:
-    "All pki pkr peki pekr ck #i #j.
-        IKeys(<pki,pkr,peki,pekr,ck>) @ i & K(ck) @ j
-        & not(Ex #j2 #j3. Reveal_AK(pki) @ j2 & Reveal_EphK(peki) @ j3)
-    ==> (Ex #j2. #j2 < #j & Reveal_AK(pkr) @ j2) |
-         ((Ex #j2. #j2 < #j & Reveal_AK(pkr) @ j2)  & ((Ex #j2. #j2 < #j & Reveal_EphK(pekr) @ j2) | (Ex #j2. #j2 < #j & Reveal_EphK(peki) @ j2)))"
-
-lemma key_knowledge_helperR[reuse,hide_lemma=disagreement_implies_Sr_or_SiEi_compromise]:
-    "All pki pkr peki pekr ck #i #j.
-        IKeys(<pki,pkr,peki,pekr,ck>) @ i & K(ck) @ j
-        & not(Ex #j2 #j3. Reveal_AK(pkr) @ j2 & Reveal_EphK(pekr) @ j3)
-    ==> (Ex #j2. #j2 < #j & Reveal_AK(pki) @ j2) | (Ex #j2. #j2 < #j & Reveal_AK(pkr) @ j2)"
-
-
 lemma key_secrecy:
     "(All pki pkr peki pekr ck #i #j.
         //If the two agents agree on keys
@@ -464,6 +454,11 @@ lemma key_secrecy:
         | (Ex #j #j2. Reveal_AK(pki) @ j & Reveal_EphK(peki) @ j2)
         | (Ex #j #j2. Reveal_AK(pkr) @ j & Reveal_EphK(pekr) @ j2))"
 
+lemma identity_hiding:
+    "All pki pkr peki pekr ck surrogate #i #j.
+        RKeys(<pki,pkr,peki,pekr,ck>) @ i & IIdentity(surrogate) @ i
+        & K(surrogate) @ j
+    ==> (Ex #j. Reveal_AK(pkr) @ j) | (Ex #j. Reveal_AK(pki) @ j) | (Ex #j. Reveal_EphK(peki) @ j)"
 
 // vim: ft=spthy
 end