diff options
| author |   Kevin Milner <kamilner@kamilner.ca> | 2017-03-02 10:09:25 -0800 |
|---|---|---|
| committer | Kevin Milner <kamilner@kamilner.ca> | 2017-03-02 10:09:25 -0800 |
| commit | 9f745ba56bd3fb102d2cbc2c8d0a284df6b233e0 (patch) | |
| tree | 282c87ca704f419088e214f333dcd60265a016e7 | |
| parent | Minor update to remove unnecessary terms, and untype the sidI term so the heuristic does better at picking terms to solve for (diff) | |
| download | wireguard-tamarin-9f745ba56bd3fb102d2cbc2c8d0a284df6b233e0.tar.xz wireguard-tamarin-9f745ba56bd3fb102d2cbc2c8d0a284df6b233e0.zip | |
Removed incorrect comment
| -rw-r--r-- | wireguard.m4 | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/wireguard.m4 b/wireguard.m4 index 6d02da5..bbc06a7 100644 --- a/wireguard.m4 +++ b/wireguard.m4 @@ -137,10 +137,7 @@ rule Handshake_CompleteNoPSK: [ State(inj,~ltkI,pkR,sisr,<'init',ci3>) ] -/*///////////////////////////////////////////////////////////////////////////// - TRACE EXISTENCE - Status: All autoprove (~15 minutes, almost entirely on exists_detect) -*/ +///////////////////////////////////////////////////////////////////////////// lemma exists_session: exists-trace "Ex a b ck #i #j. @@ -161,5 +158,6 @@ lemma injective_agreement: InitTransportKeys(a,b,ck) @ i & RespTransportKeys(a,b,ck) @ j ==> #j < #i & not(Ex #k. RespTransportKeys(a,b,ck) @ k & not(#k = #j))" end + // vim: ft=spthy |