diff options
Diffstat (limited to 'wireguard.m4')
| -rw-r--r-- | wireguard.m4 | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/wireguard.m4 b/wireguard.m4 index df86b70..e48b7f3 100644 --- a/wireguard.m4 +++ b/wireguard.m4 @@ -26,7 +26,6 @@ equations: decrypt(aead(k, p, a), k) = p equations: verify(aead(k, p, a), a, k) = true restriction Eq_testing: "All x y #i. Eq(x, y) @ i ==> x = y" -restriction InEq_testing: "All x y #i. InEq(x, y) @ i ==> not(x = y)" /* Uncomment these to prevent any adversary message modifications, * useful for checking exists-trace lemmas and making sure messsages @@ -47,12 +46,6 @@ define(StateInvariants, F_StateInvariants($*)) * session anyway. */ define(State, L_State($*)) /* HACK: This is a heuristic hack that should be removed by prefixing with m4 comment - d n l. */ -/* Pre-established trust relationships */ -restriction pairings_unique: - "All id id2 ka kb #i #j. - Paired(id, ka, kb) @ i & Paired(id2, ka, kb) @ j - ==> #i = #j" - /* Keygen is separate from pairing to allow keys to be paired * more than once (if they were generated fresh in the pairing * this would not be possible */ |