(* Model of WireGuard written by Benjamin Lipp and Bruno Blanchet, Inria Paris.
*)

proof {
      auto; (* does: crypto prf(mac) Rm; *)
      crypto suf_cma_corrupt(mac2f) r_1;
      move array r_1;
      success
      }

channel c_resp_0, c_resp_1, c_resp_2, c_resp_3, c_resp_4.

param N_Resp_R, N_Resp_C, N_Resp_T.

type key_t [large, fixed].

event generated_cookie(bitstring, N_Resp_R, key_t).
event accepted_cookie(bitstring, N_Resp_R, key_t, bitstring, key_t).

query Am: bitstring, iRm <= N_Resp_R, tau: key_t, msgbeta: bitstring, mac2: key_t;
      event(accepted_cookie(Am, iRm, tau, msgbeta, mac2)) ==>
      event(generated_cookie(Am, iRm, tau)).
      
(* We assume that the MAC that serves for generating the cookie is a PRF,
   because we use its output tau as a key for computing mac2,
   and that key must be random. (SUF-CMA would not be sufficient.) *)

proba Pprf.
expand PRF(key_t, bitstring, key_t, mac, Pprf).

(* For mac2, we assume that the MAC is SUF-CMA.
   CryptoVerif would not succeed with the PRF assumption,
   because it is unable to handle corruptions for PRFs.
   It can handle corruptions for SUF-CMA MACs.
   It is well known that PRF => SUF_CMA, we obtain a proof
   under the assumption that the MAC is a PRF. *)

proba Pmac.
expand SUF_CMA_det_mac(key_t, bitstring, key_t, mac2f, verify2f, Pmac).

process
	! i_Resp_R <= N_Resp_R
	in(c_resp_0, ());
	(* The responder generates a new Rm every two minutes *)
	new Rm: key_t;
	out(c_resp_1, ());
	((
	   ! i_Resp_C <= N_Resp_C
	   in(c_resp_2, Am': bitstring);
	   (* The responder generates a cookie tau for Am'
	      (concatenation of IP source address and UDP source port) *)
	   let tau = mac(Rm, Am') in
	   event generated_cookie(Am', i_Resp_R, tau);
	   (* We give the cookie tau to the adversary.
	      He can encrypt it and run the rest of the protocol. *)
	   out(c_resp_3, tau)
	)|(
	   ! i_Resp_T <= N_Resp_T
	   (* The responder receives a message msgbeta with a mac2 from
	      Am2'. It verifies the mac2. *)
	   in(c_resp_4, (Am2': bitstring, msgbeta: bitstring, mac2: key_t));
	   let tau2' = mac(Rm, Am2') in
	   if mac2 = mac2f(msgbeta, tau2') then
	   event accepted_cookie(Am2', i_Resp_R, tau2', msgbeta, mac2) 
	))

(* EXPECTED
All queries proved.
0.304s (user 0.288s + system 0.016s), max rss 21496K
END *)