diff options
-rw-r--r-- | wireguard.m4 | 6 |
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 |