summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--wireguard.m46
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