summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorJason A. Donenfeld <Jason@zx2c4.com>2017-05-09 00:16:34 +0200
committerJason A. Donenfeld <Jason@zx2c4.com>2017-05-09 00:19:39 +0200
commitf2f5c93de7892758b0e154f82fd7a24031b26979 (patch)
treedb88065ea35a9415713cca012a659d39aa3908e6
parentBe less ugly (diff)
downloadwireguard-tamarin-f2f5c93de7892758b0e154f82fd7a24031b26979.tar.xz
wireguard-tamarin-f2f5c93de7892758b0e154f82fd7a24031b26979.zip
Re-add heuristic hacks
-rw-r--r--wireguard.m412
1 files changed, 8 insertions, 4 deletions
diff --git a/wireguard.m4 b/wireguard.m4
index 661ea06..df86b70 100644
--- a/wireguard.m4
+++ b/wireguard.m4
@@ -45,7 +45,7 @@ define(StateInvariants, F_StateInvariants($*))
* case, typically agent state can come from just about anywhere so it creates
* a ton of case distinctions when we're usually only interested in the current
* session anyway. */
-dnl define(State, L_State($*))
+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:
@@ -117,7 +117,7 @@ rule Handshake_Init:
ki2 = h(<ci1, sisr, '2'>)
ats = aead(ki2, $ts, hi0)
hi1 = h(<hi0, ats>)
- m1 = <'1', ~sidI, pekI, astat, ats, $mac1, $mac2> in //NOTE: MACs are currently not modeled
+ m1 = <'1', ~sidI, pekI, astat, ats, $mac1, $mac2> in /* NOTE: MACs are currently not modeled. */
[ /* Init can be triggered at any time, even when currently performing
* another role or on another stage. This could happen e.g. because of a timeout.
* As such we bind the previous state as 'anything' and discard it. */
@@ -130,6 +130,7 @@ rule Handshake_Init:
]-->
[ /* We cache DH sisr to reduce variant precomputation time for tamarin. */
State(~id, <'init', ~sidI, ~ekI, ci2, ki2, hi1>)
+ , F_SolveInit(~id, ~psk, <'init', ~sidI, ~ekI, ci2, ki2, hi1>) /* HACK: This is a heuristic hack that should be removed. */
, !EphKeytoReveal(~ekI)
, Out(m1)
]
@@ -152,7 +153,7 @@ rule Handshake_Resp:
kr2 = h(<cr1, sisr, '2'>)
ats = aead(kr2, $ts, hr0)
hr1 = h(<hr0, ats>)
- m1 = <'1', sidI, pekI, astat, ats, $mac1, $mac2> //NOTE: MACs are currently not modeled
+ m1 = <'1', sidI, pekI, astat, ats, $mac1, $mac2> /* NOTE: MACs are currently not modeled. */
/* Constructing the response message m2: */
cr3 = h(<cr2, pekR, '1'>)
hr2 = h(<hr1, pekR>)
@@ -164,7 +165,7 @@ rule Handshake_Resp:
hr3 = h(<hr2, hrt>)
aempt = aead(kr6, 'e', hr3)
hr4 = h(<hr3, aempt>)
- m2 = <'2', sidI, ~sidR, pekR, aempt, $mac1, $mac2> in //NOTE: MACs are currently not modeled
+ m2 = <'2', sidI, ~sidR, pekR, aempt, $mac1, $mac2> in /* NOTE: MACs are currently not modeled. */
[ State(~id, anything)
, !StateInvariants(~id, ~psk, ~ltkR, pkI, sisr)
, Fr(~ekR)
@@ -177,6 +178,7 @@ rule Handshake_Resp:
, Identity_Surrogate(pkISurrogate)
]->
[ State(~id, <'transport_unconfirmed', ~sidR, pekI, pekR, cr6>)
+ , F_SolveResp(~id, ~psk, <'transport_unconfirmed', ~sidR, pekI, pekR, cr6>) /* HACK: This is a heuristic hack that should be removed. */
, !EphKeytoReveal(~ekR)
, Out(m2)
]
@@ -202,6 +204,7 @@ rule Handshake_Complete:
* in it are public except the key used to encrypt. */
mtr = <'4', sidR, aead(ci6, 'message', '0')> in
[ State(~id, <'init', sidI, ~ekI, ci2, ki2, hi1>)
+ , F_SolveInit(~id, ~psk, <'init', sidI, ~ekI, ci2, ki2, hi1>) /* HACK: This is a heuristic hack that should be removed. */
, !StateInvariants(~id, ~psk, ~ltkI, pkR, sisr)
, In(m2)
]--[
@@ -223,6 +226,7 @@ rule Handshake_Complete:
rule R_ConfirmedTransportMessage:
let mtr = <'4', sid, data> in
[ State(~id, <'transport_unconfirmed', sidR, pekI, pekR, cr>)
+ , F_SolveResp(~id, ~psk, <'transport_unconfirmed', sidR, pekI, pekR, cr>) /* HACK: This is a heuristic hack that should be removed. */
, !StateInvariants(~id, ~psk, ~ltkR, pkI, sisr)
, In(mtr)
]--[