diff options
| -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 |