diff options
| author |   Jason A. Donenfeld <Jason@zx2c4.com> | 2017-05-06 14:56:09 +0200 |
|---|---|---|
| committer | Jason A. Donenfeld <Jason@zx2c4.com> | 2017-05-06 14:56:09 +0200 |
| commit | 61ea232eaa68770cfec4937f321144b389736a40 (patch) | |
| tree | 67d190a38a18d368269672082cd46cdd4c39f998 | |
| parent | Without heuristic hackery (diff) | |
| download | wireguard-tamarin-61ea232eaa68770cfec4937f321144b389736a40.tar.xz wireguard-tamarin-61ea232eaa68770cfec4937f321144b389736a40.zip | |
Exists PSK
| -rw-r--r-- | wireguard.m4 | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/wireguard.m4 b/wireguard.m4 index 3cb8f9f..f7dca4c 100644 --- a/wireguard.m4 +++ b/wireguard.m4 @@ -255,6 +255,11 @@ lemma exists_session: exists-trace IKeys(<pki,pkr,peki,pekr,'nopsk',ck>) @ i & RConfirm(<pki,pkr,peki,pekr,'nopsk',ck>) @ j & #i < #j" +lemma exists_session_psk: exists-trace + "Ex pki pkr peki pekr psk ck #i #j. + IKeys(<pki,pkr,peki,pekr,psk,ck>) @ i & UsingPSK(psk) @ i + & RConfirm(<pki,pkr,peki,pekr,psk,ck>) @ j & #i < #j" + //There are only three numbers, 0, 1, and infinity. So 2 == infinity lemma exists_two_sessions: exists-trace "Ex pki pkr sesskeys sesskeys2 #i #j #i2 #j2. |