diff options
| author |   Kevin Milner <kevin.milner@cs.ox.ac.uk> | 2017-07-14 12:14:24 +0100 |
|---|---|---|
| committer | Kevin Milner <kevin.milner@cs.ox.ac.uk> | 2017-07-14 12:14:24 +0100 |
| commit | a450d6b426b5821811046b4446014ee720706601 (patch) | |
| tree | 88b0dfc7e6e9f1008bf4236aa35abcbaac1fa25c | |
| parent | GPLv2 (diff) | |
| download | wireguard-tamarin-a450d6b426b5821811046b4446014ee720706601.tar.xz wireguard-tamarin-a450d6b426b5821811046b4446014ee720706601.zip | |
Removed unnecessary restrictions
| -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 */ |