summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorKevin Milner <kevin.milner@cs.ox.ac.uk>2017-07-14 12:14:24 +0100
committerKevin Milner <kevin.milner@cs.ox.ac.uk>2017-07-14 12:14:24 +0100
commita450d6b426b5821811046b4446014ee720706601 (patch)
tree88b0dfc7e6e9f1008bf4236aa35abcbaac1fa25c
parentGPLv2 (diff)
downloadwireguard-tamarin-a450d6b426b5821811046b4446014ee720706601.tar.xz
wireguard-tamarin-a450d6b426b5821811046b4446014ee720706601.zip
Removed unnecessary restrictions
-rw-r--r--wireguard.m47
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 */