diff options
| -rw-r--r-- | wireguard.m4 | 12 |
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) ]--[ |