dhkem.auth.insider-cca-lr.ocv

(* Analysing the HPKE Standard - Supplementary Material
   Joël Alwen; Bruno Blanchet; Eduard Hauck; Eike Kiltz; Benjamin Lipp; 
   Doreen Riepel

This is supplementary material accompanying the paper:

Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
Long version: https://eprint.iacr.org/2020/1499 *)

proof {
  allowed_collisions default^4/large;
   (* We allow eliminating collisions with probability in power 4 of 
      N, Qeperuser, Qdperuser, Qcperuser times PCollKey, to allow q^2 * PCollKey,
      where q = N * (Qeperuser + Qdperuser + Qcperuser) *)
  (* on the left side *)
  out_game "l0.out.cv";
  (* Let appear this case distinction in the Decap oracle,
     that is present on the right side *)
  insert after "OADecap(pk_S"
    "find ic_1 = ic <= Qcperuser suchthat
      defined(zz_3[ic], sk'[ic], enc_2[ic])
      && (enc_2[ic] = cd)
      && (exp(g, sk'[ic]) = pk_S)
      then";
  simplify;
  out_game "l1.out.cv";
  out_game "l1occ.out.cv" occ;
  (* Use correctnes of the KEM: in the Decap oracle, in the case of
     honest participants, return the key chosen in the Encap oracle. *)
  replace
    at_nth 1 3 "return{[0-9]*}({[0-9]*}AuthDecap_Some({[0-9]*}zz_5))"
    "zz_3[ic_2]";
  remove_assign useless;
  simplify;
  out_game "l2.out.cv";
  out_game "l2occ.out.cv" occ;

  (* Let appear this case distinction in the Encap oracle.
     Treating messages between honest keys separately helps
     when applying GDH. *)
  insert after "OAEncap(pk_R"
    "find i1 <= N suchthat
      defined(sk[i1])
      && pk_R = exp(g, sk[i1]) then";
  out_game "l3.out.cv";
  (* Use unique names for the assignments of the following variables
     that are currently not unique *)
  SArename z_2;
  SArename enc_3;
  SArename dh_4;
  SArename zz_4;
  SArename pkE_4;
  SArename kemContext_4;
  SArename key_1;
  SArename info_1;
  out_game "l4.out.cv";

  (* Make it possible to reason about the composition of the
     random oracle inputs, specifically the group elements,
     which is needed for the usage of the GDH assumption. *)
  insert after "OH(x1"
    "let eae_input(
      salt: extract_salt_t,
      concatExtract(
        protocol1: label_protocol_t,
        suite1: suite_id_t,
        label1: label_extract_t,
        concatDH(dh1: G_t, dh2: G_t)),
      concatExpand(
        l: two_byte_t,
        protocol2: label_protocol_t,
        suite2: suite_id_t,
        label2: label_expand_t,
        concatContext(pkE': G_t, pkR': G_t, pkS': G_t))) = x1 in";
  crypto rom(ExtractAndExpand_inner);
  out_game "l5.out.cv";
  crypto gdh(exp) [variables: sk -> a, z_1 -> b .];
  out_game "l.out.cv" occ;

  (* go to right side *)
  start_from_other_end;
  out_game "r0.out.cv";
  (* Let appear this case distinction in the Encap oracle.
     Treating messages between honest keys separately helps
     when applying GDH. *)
  insert after "OAEncap(pk_R_1"
    "find i2 <= N suchthat
      defined(sk_1[i2])
      && pk_R_1 = exp(g, sk_1[i2]) then";
  (* Make it possible to reason about the composition of the
     random oracle inputs, specifically the group elements,
     which is needed for the usage of the GDH assumption. *)
  insert after "OH(x1"
    "let eae_input(
      salt: extract_salt_t,
      concatExtract(
        protocol1: label_protocol_t,
        suite1: suite_id_t,
        label1: label_extract_t,
        concatDH(dh1: G_t, dh2: G_t)),
      concatExpand(l: two_byte_t,
        protocol2: label_protocol_t,
        suite2: suite_id_t,
        label2: label_expand_t,
        concatContext(pkE'': G_t, pkR'': G_t, pkS'': G_t))) = x1_1 in";
  crypto rom(ExtractAndExpand_inner);
  out_game "r2.out.cv";
  (* Use unique names for the assignments of the following variables
     that are currently not unique *)
  SArename z_5;
  SArename enc_8;
  SArename pkE_10;
  remove_assign binder E_1;
  out_game "r3.out.cv";
  success
}

(* Analysing the HPKE Standard - Supplementary Material
   Joël Alwen; Bruno Blanchet; Eduard Hauck; Eike Kiltz; Benjamin Lipp; 
   Doreen Riepel

This is supplementary material accompanying the paper:

Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp,
and Doreen Riepel. Analysing the HPKE Standard. In Anne Canteaut and
Francois-Xavier Standaert, editors, Eurocrypt 2021, Lecture Notes in
Computer Science, pages 87-116, Zagreb, Croatia, October 2021. Springer.
Long version: https://eprint.iacr.org/2020/1499 *)


type G_t [bounded].
fun Serialize(G_t): bitstring [data].
type Z_t [bounded,nonuniform].
proba PCollKey.

expand DH_proba_collision_minimal(
  G_t,
  Z_t,
  g,
  exp,
  mult,
  PCollKey
).



proba Adv_GDH.
proba PDistRerandom.
expand GDH_RSR_minimal(
  (* types *)
  G_t,  (* Group elements *)
  Z_t,  (* Exponents *)
  (* variables *)
  g,    (* a generator of the group *)
  exp,  (* exponentiation function *)
  mult, (* multiplication function for exponents *)
  (* probabilities *)
  Adv_GDH, (* probability of breaking the GDH assumption *)
  PDistRerandom (* probability of distinguishing a key that comes from 
       rerandomization from an honestly chosen key *)
).



(* For a group of prime order q:
   PColl1Rand(Z_t) = PColl2Rand(Z_t) = 1/(q-1)
   PCollKey1 = PCollKey2 = 1/(q-1)
   PDistRerandom = 0

   For Curve25519:
   PColl1Rand(Z_t) = PColl2Rand(Z_t) = 2^{-251}
   PCollKey1 = PCollKey2 = 2 PColl1Rand(Z_t) = 2^{-250}
   PDistRerandom = 2^{-125}

   For Curve448:
   PColl1Rand(Z_t) = PColl2Rand(Z_t) = 2^{-445}
   PCollKey1 = PCollKey2 = 2 PColl1Rand(Z_t) = 2^{-444}
   PDistRerandom = 2^{-220}
*)

letfun DH(exponent: Z_t, group_element: G_t) =
  exp(group_element, exponent).
letfun pkgen(exponent: Z_t) =
  exp(g, exponent).
letfun skgen(exponent: Z_t) =
  exponent.
letfun GenerateKeyPair() =
  z <-R Z_t;
  (skgen(z), pkgen(z)).


(* KDF *)

type hash_key_t [fixed]. (* RO key *)
type eae_input_t [fixed].
type eae_output_t [fixed,large].
type extract_salt_t [fixed]. (* We only use one constant salt value. *)
type extract_key_t [fixed].
type expand_info_t [fixed].
const lbytes_empty: extract_salt_t.

fun eae_input(extract_salt_t, extract_key_t, expand_info_t): eae_input_t [data].

(* The core of ExtractAndExpand, a.k.a. HKDF.
Usage of the RO assumption is for example justified in Lemma 6 of
Benjamin Lipp, Bruno Blanchet, Karthikeyan Bhargavan,
A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol,
EuroSP2019 *)
expand ROM_hash_1(
  (* types *)
  hash_key_t,
  eae_input_t,
  eae_output_t,
  (* functions *)
  ExtractAndExpand_inner,
  (* processes *)
  ExtractAndExpand_inner_orcl,
  (* parameters *)
  Qh  (* number of queries to the oracle by the adversary *)
).


type length_t [fixed].
type two_byte_t [fixed].
fun I2OSP2(length_t): two_byte_t [data].
const Nsecret: length_t.

type label_protocol_t [fixed].
const RFCXXXX: label_protocol_t.

type label_extract_t [fixed].
const label_eae_prk: label_extract_t.

type label_expand_t [fixed].
const label_shared_secret: label_expand_t.

type suite_id_t [fixed].
const suite_id: suite_id_t.

type GG_t [fixed].
type GGG_t [fixed].

fun concatDH(G_t, G_t): GG_t [data].
fun concatContext(G_t, G_t, G_t): GGG_t [data].

(* This can be data because we only use it with a few known constants
   for the two first parameters, or with fixed-length parameters. *)
fun concatExtract(label_protocol_t, suite_id_t, label_extract_t, GG_t): extract_key_t [data].

(* concatExpand is only used in LabeledExpand, which is only used
   in ExtractAndExpand in the KEM:
     LabeledExpand(eae_prk, label_shared_secret, kem_context, Nsecret)
   with the following call:
     concatExpand(I2OSP2(L), RFCXXXX, suite_id, label, info).
   I2OSP2 is fixed-length (two bytes),
   RFCXXXX is fixed-length (7 bytes),
   suite_id is fixed-length,
   label_shared_secret is fixed-length;
   info is fixed-length as concatenation of enc||pkR||pkS *)
fun concatExpand(two_byte_t, label_protocol_t, suite_id_t, label_expand_t, GGG_t): expand_info_t [data].

(* Detailed justification that the following usage of ExtractAndExpand
   satisfies the assumptions of above-mentioned Lemma 6, given it is
   implemented by HKDF:

- keyspace and info||i_0 do not collide, because info has two bytes and
  then RFCXXXX, and RFCXXXX does not collide with itself when moved by
  two bytes.

For long Nsecret, we also need to consider this:
- keyspace and hmac_output_space||info||i_j with j>0
  Length(keyspace) - Length(hmac_output_space||info||i_j)
  = -2 +Length(label_eae_prk) -Length(label_shared_secret) +Length(dh) -Length(kem_context) -Nh
  = -2 +7 -13 +Ndh -Nenc -Npk -Npk -Nh
  = -8 +Ndh -Nenc -Npk -Npk -Nh
  Assuming that Ndh is pretty close to Npk, we can argue that
  keyspace and hmac_output_space||info||i_j with j>0
  have clearly different lengths, and thus, do not collide.

Therefore the following usage of ExtractAndExpand satisfies the
assumptions of Lemma 6.
*)
letfun ExtractAndExpand(key_extr: hash_key_t, dh: GG_t, kem_context: GGG_t) =
  let key = concatExtract(RFCXXXX, suite_id, label_eae_prk, dh) in
  let info = concatExpand(I2OSP2(Nsecret), RFCXXXX, suite_id, label_shared_secret, kem_context) in
  ExtractAndExpand_inner(key_extr, eae_input(lbytes_empty, key, info)).


expand OptionType_2(AuthEncap_res_t, AuthEncap_tuple, AuthEncap_None, eae_output_t, bitstring).

letfun AuthEncap(key_extr: hash_key_t, pkR: G_t, skS: Z_t) =
  let (skE: Z_t, pkE: G_t) = GenerateKeyPair() in
  (
    let dh: GG_t = concatDH(DH(skE, pkR), DH(skS, pkR)) in
    let enc: bitstring = Serialize(pkE) in
    let pkS = pkgen(skS) in
    let kemContext: GGG_t = concatContext(pkE, pkR, pkS) in
    let zz: eae_output_t = ExtractAndExpand(key_extr, dh, kemContext) in
    AuthEncap_tuple(zz, enc)
  ) else (
    AuthEncap_None
  ).

expand OptionType_1(AuthDecap_res_t, AuthDecap_Some, AuthDecap_None, eae_output_t).

letfun AuthDecap(key_extr: hash_key_t, enc: bitstring, skR: Z_t, pkS: G_t) =
  let Serialize(pkE: G_t) = enc in
  (
    let dh: GG_t = concatDH(DH(skR, pkE), DH(skR, pkS)) in
    let pkR = pkgen(skR) in
    let kemContext: GGG_t = concatContext(pkE, pkR, pkS) in
    let zz: eae_output_t = ExtractAndExpand(key_extr, dh, kemContext) in
    AuthDecap_Some(zz)
  ) else (
    AuthDecap_None
  ).



param N, Qeperuser, Qcperuser, Qdperuser.

table E(G_t, G_t, bitstring, eae_output_t).

equivalence
  Ostart() :=
    key_extr <-R hash_key_t;
    return();
    ((
      foreach i <= N do Osetup() := sk <-R Z_t; return(); (
        foreach ic <= Qcperuser do (
	  Ochall(sk': Z_t) :=
            return(AuthEncap(key_extr, pkgen(sk), skgen(sk')))) |
        foreach ie <= Qeperuser do (
	  OAEncap(pk_R: G_t) :=
            return(AuthEncap(key_extr, pk_R, skgen(sk)))) |
        foreach id <= Qdperuser do (
	  OADecap(pk_S: G_t, cd: bitstring) :=
            return(AuthDecap(key_extr, cd, skgen(sk), pk_S))) |
	(* The next oracle gives the public key to the adversary *)
        Opk() := return(pkgen(sk))
      )) |
      (* The random oracle ExtractAndExpand_inner *)
      run ExtractAndExpand_inner_orcl(key_extr)
    )

  Ostart() :=
    key_extr <-R hash_key_t;
    return();
    ((
      foreach i <= N do Osetup() := sk <-R Z_t; return(); (
        foreach ic <= Qcperuser do (
	  Ochall(sk': Z_t) :=
            let AuthEncap_tuple(k: eae_output_t, ce: bitstring) = AuthEncap(key_extr, pkgen(sk), skgen(sk')) in (
              k' <-R eae_output_t;
	      insert E(pkgen(sk'), pkgen(sk), ce, k');
              return(AuthEncap_tuple(k', ce))
            ) else (
              (* Never happens because AuthEncap always returns AuthEncap_tuple(...) *)
              return(AuthEncap_None)
            )) |
        foreach ie <= Qeperuser do (
	  OAEncap(pk_R: G_t) :=
            return(AuthEncap(key_extr, pk_R, skgen(sk)))) |
        foreach id <= Qdperuser do (
	  OADecap(pk_S: G_t, cd: bitstring) :=
	    get E(=pk_S, =pkgen(sk), =cd, k'') in (
              return(AuthDecap_Some(k''))
            ) else (
              return(AuthDecap(key_extr, cd, skgen(sk), pk_S))
            )) |
        Opk() := return(pkgen(sk))
      )) |
      run ExtractAndExpand_inner_orcl(key_extr)
    )

(* EXPECTED FILENAME: examples/hpke/dhkem.auth.insider-cca-lr.m4.ocv TAG: 1
All queries proved.
0.988s (user 0.980s + system 0.008s), max rss 30224K
END *)