Unknown key-share resistanceHEADmaster

1 files changed, 6 insertions, 0 deletions

diff --git a/wireguard.m4 b/wireguard.m4
index a286b77..8137c3c 100644
--- a/wireguard.m4
+++ b/wireguard.m4
@@ -298,6 +298,12 @@ lemma R_disagreement_implies_Si_or_SrEr_compromise_and_PSK_compromise[reuse]:
         | (Ex #j #j2. Reveal_AK(pkr) @ j & Reveal_EphK(pekr) @ j2 & #j2 < #i & #j < #i)
         )"
 
+lemma UKS_resistance:
+    "All pki1 pki2 pkr1 pkr2 peki1 peki2 pekr1 pekr2 psk1 psk2 ck #i #j.
+        IKeys(<pki1, pkr1, peki1, pekr1, psk1, ck>) @ i
+        & RKeys(<pki2, pkr2, peki2, pekr2, psk2, ck>) @ j
+    ==> pki1 = pki2 & pkr1 = pkr2 & peki1 = peki2 & pekr1 = pekr2 & psk1 = psk2"
+
 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