From f2f5c93de7892758b0e154f82fd7a24031b26979 Mon Sep 17 00:00:00 2001
From: "Jason A. Donenfeld" <Jason@zx2c4.com>
Date: Tue, 9 May 2017 00:16:34 +0200
Subject: Re-add heuristic hacks

---
 wireguard.m4 | 12 ++++++++----
 1 file 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)
     ]--[
-- 
cgit v1.2.3-59-g8ed1b