cookie

process_complete_with_cookie/wireguard_peer_initiator_reference.spthy

@@ -39,12 +39,12 @@ let Initiator_Receive_Cookie(~ltkI, pkI, pkR, zero_1, chi:channel) =
     out(<'xI', sidI, pekI0, astat, ats, macI1, macI2>);    // Send InitHello
 
     // Cookie reception
-    in(<~nonce, encrypted_cookie>); // Receive Cookie
+    in(<'xC', ~nonce, encrypted_cookie>); // Receive Cookie
     let cookie = xdecrypt(h(pkR), ~nonce, encrypted_cookie) in
     if (checkxaead(h(pkR), ~nonce, macI1, encrypted_cookie) = true) then
     (
       let macI2n = mac(cookie, previous_msg) in
-      out(chi, <macI2n, pkR>)
+      out(chi, <macI2n, pkR, sisr>)
     )) | (RevealEkin(~ekI0))
 
 let Initiator(~ltkI, pkI, ~psk, empty, zero_1, chi:channel) =
@@ -62,11 +62,7 @@ let Initiator(~ltkI, pkI, ~psk, empty, zero_1, chi:channel) =
     let ctrR0:nat = zero_1 in
     //let ctrR1:nat = ctrR0 + 'one' in
 
-    // cookie reception
-
-    in(chi, <macI2n, pkR>);
-
-    let sisr = (pkR)^~ltkI in // precompi input
+    in(chi, <macI2n, pkR, sisr>);
 
       //InitHello generation
       let pekI  = 'g'^~ekI in

process_complete_with_cookie/wireguard_peer_responder_reference.spthy

@@ -13,7 +13,7 @@ let Responder_Send_Cookie(~ipI, ~portI, pkR, chr:channel) =
       new ~nonce;
       let cookie_encrypted = xaead(h(pkR),~nonce, macI1, cookie) in
       let new_macI2 = mac(cookie, <sidI, pekI0, astat, ats, macI1, macI2>) in
-      out(<~nonce, cookie_encrypted>);
+      out(<'xC', ~nonce, cookie_encrypted>);
       out(chr, new_macI2)
     )