HKDFexpand.cv

(* This file proves that, when l_1, l_2, l_3 are pairwise distinct
labels and s is a fresh random value, HKDF-expand-label(s, l_i, "") for 
i = 1,2,3 are indistinguishable from independent fresh random values. *)

type key [large, fixed].
type label.

(* HMAC is a PRF *)

fun HMAC(key, bitstring):key.

proba Pprf.

param N, N3.

equiv prf(HMAC)
       !N3 new r: key; !N O(x:bitstring) := HMAC(r,x)
     <=(N3 * (2/|key| + Pprf(time + (N3-1)* N * time(HMAC, maxlength(x)), N, maxlength(x))))=>
       !N3 !N O(x: bitstring) :=
	        find[unique] j<=N suchthat defined(x[j],r2[j]) && x = x[j] then r2[j] 
		else new r2: key; r2.

(* HKDF_expand_label_empty_bytes(Secret, Label) = 
   HKDF_expand_label(Secret, Label, "", Length) =
   HKDF_expand(Secret, [Length, "TLS 1.3, " + Label, ""], Length) =
   Truncate(HMAC(Secret, [Length, "TLS 1.3, " + Label, "", 0x00]), Length)

The Length is supposed to be fixed from the Label (true for a given configuration).
Length <= Hash.length
We ignore the final truncation; we assume that the caller will use only
the first Length bits.
We define build_arg(Label) = [Length, "TLS 1.3, " + Label, "", 0x00].
*)

fun build_arg(label): bitstring [compos].

letfun HKDF_expand_label_empty_bytes(Secret: key, Label: label) =
       HMAC(Secret, build_arg(Label)).

(* Three different constant labels
   Typical labels: "finished", "key", "iv" for the handshake_traffic_secret
   or "application traffic secret", "key", "iv" for the traffic_secret_N *)

const l1: label.
const l2: label.
const l3: label.

letfun HKDF_expand_l1(Secret: key) =
       HKDF_expand_label_empty_bytes(Secret, l1).
letfun HKDF_expand_l2(Secret: key) =
       HKDF_expand_label_empty_bytes(Secret, l2).
letfun HKDF_expand_l3(Secret: key) =
       HKDF_expand_label_empty_bytes(Secret, l3).


(* Prove equivalence between processLeft and processRight *)

query secret b.

channel start, c1, c2, c3, c4.

let processLeft =
    !N3 in(c1, ()); new k: key; out(c1, ());
    ((in(c2, ()); out(c2, HKDF_expand_l1(k))) |
     (in(c3, ()); out(c3, HKDF_expand_l2(k))) |
     (in(c4, ()); out(c4, HKDF_expand_l3(k)))).

let processRight =
    !N3 in(c1, ()); out(c1, ());
    ((in(c2, ()); new r1: key; out(c2, r1)) |
     (in(c3, ()); new r2: key; out(c3, r2)) |
     (in(c4, ()); new r3: key; out(c4, r3))).
    
process
	in(start, ());
	new b: bool;
	if b then out(start, ()); processLeft
	     else out(start, ()); processRight

(* EXPECTED
All queries proved.
0.024s (user 0.020s + system 0.004s), max rss 29424K
END *)