cookie

process_complete_with_cookie/wireguard_peer_initiator_reference.spthy

@@ -44,10 +44,10 @@ let Initiator_Receive_Cookie(~ltkI, pkI, pkR, zero_1, chi:channel) =
     if (checkxaead(h(pkR), ~nonce, macI1, encrypted_cookie) = true) then
     (
       let macI2n = mac(cookie, previous_msg) in
-      out(chi, macI2n)
+      out(chi, <macI2n, pkR>)
     )) | (RevealEkin(~ekI0))
 
-let Initiator(~ltkI, pkI, pkR, ~psk, empty, zero_1, chi:channel) =
+let Initiator(~ltkI, pkI, ~psk, empty, zero_1, chi:channel) =
 
     new sidIn;  // session id is new
     new ~ekI;
@@ -62,13 +62,13 @@ let Initiator(~ltkI, pkI, pkR, ~psk, empty, zero_1, chi:channel) =
     let ctrR0:nat = zero_1 in
     //let ctrR1:nat = ctrR0 + 'one' in
 
-    // pkr input
+    // cookie reception
 
-    let sisr = (pkR)^~ltkI in // precompi input
+    in(chi, <macI2n, pkR>);
 
-    // cookie reception
+    // pkr input
 
-      in(chi, macI2n);
+    let sisr = (pkR)^~ltkI in // precompi input
 
       //InitHello generation
       let pekI  = 'g'^~ekI in

process_complete_with_cookie/wireguard_process_reference.spthy

@@ -22,7 +22,7 @@ out(empty);
 
 
 (
-      (! Initiator(~ltkI, 'g'^~ltkI, 'g'^~ltkR, ~psk, empty, %1, chi)) | (!Initiator_Receive_Cookie(~ltkI, 'g'^~ltkI, 'g'^~ltkR, %1, chi))
+      (! Initiator(~ltkI, 'g'^~ltkI, ~psk, empty, %1, chi)) | (!Initiator_Receive_Cookie(~ltkI, 'g'^~ltkI, 'g'^~ltkR, %1, chi))
     | (! Responder(~ltkR, 'g'^~ltkI, 'g'^~ltkR, ~psk, empty, %1, chr)) | (!Responder_Send_Cookie(~ipI, ~portI, 'g'^~ltkR, chr))
     | RevealPsk(~psk)
     | RevealLtki(~ltkI)