From 9f01a2022a06f25a9f55405ca1af8899b0dd3585 Mon Sep 17 00:00:00 2001 From: Matthias Meijers Date: Mon, 10 Feb 2025 20:35:05 +0100 Subject: [PATCH] Start cleanup of ROM proofs and think more about abstractions. --- proofs/DoubleROM.eca | 5 +- proofs/HashFunctionsAlt.eca | 55 +++ proofs/HashFunctionsx2.eca | 84 +++- proofs/KeyedHashFunctionsAlt.eca | 68 +++ proofs/KeyedHashFunctionsx2.eca | 89 ++++ proofs/ML_KEM_HL_Binding_SM.eca | 282 ++++++++++++ proofs/ROMx2.eca | 764 +++++++++++++++++++++++++++++++ 7 files changed, 1321 insertions(+), 26 deletions(-) create mode 100644 proofs/HashFunctionsAlt.eca create mode 100644 proofs/KeyedHashFunctionsAlt.eca create mode 100644 proofs/KeyedHashFunctionsx2.eca create mode 100644 proofs/ML_KEM_HL_Binding_SM.eca create mode 100644 proofs/ROMx2.eca diff --git a/proofs/DoubleROM.eca b/proofs/DoubleROM.eca index 639ca80..2684277 100644 --- a/proofs/DoubleROM.eca +++ b/proofs/DoubleROM.eca @@ -1,6 +1,5 @@ require import AllCore Distr List FMap PROM. - lemma size_behead (s : 'a list) : size (behead s) = if s = [] then 0 else size s - 1. proof. by elim: s. qed. @@ -18,7 +17,6 @@ rewrite -(perm_cons x) => peqxc. rewrite (perm_eq_trans _ _ _ peqxc) perm_eq_sym perm_to_rem 1:/#. qed. - lemma uniq_drop (s : 'a list) (n : int) : uniq s => uniq (drop n s). proof. by elim: s n => // /#. qed. @@ -2408,5 +2406,4 @@ hoare. progress. smt(pmax_ge0). trivial. qed. - - +end section. diff --git a/proofs/HashFunctionsAlt.eca b/proofs/HashFunctionsAlt.eca new file mode 100644 index 0000000..9c1449e --- /dev/null +++ b/proofs/HashFunctionsAlt.eca @@ -0,0 +1,55 @@ +require import AllCore Distr. + +type in_t. + +type out_t. + +op f : in_t -> out_t. + +module type Adv_CRAlt = { + proc find() : in_t * in_t +}. + +module CRAlt(A : Adv_CRAlt) = { + proc main() : bool = { + var x1, x2 : in_t; + + (x1, x2) <@ A.find(); + + return f x1 = f x2; + } +}. + + +theory ROM. + +module type KHF_ROi = { + proc init() : unit + proc get(x : in_t) : out_t +}. + +module type KHF_RO = { + include KHF_ROi [init] +}. + +module type Adv_CRAlt_ROM (F_RO : KHF_RO) = { + include Adv_CRAlt +}. + +module CRAlt_ROM (F_RO : KHF_ROi) (A : Adv_CRAlt_ROM) = { + proc main() : bool = { + var x1, x2 : in_t; + var y1, y2 : out_t; + + F_RO.init(); + + (x1, x2) <@ A(F_RO).find(); + + y1 <@ F_RO.get(x1); + y2 <@ F_RO.get(x2); + + return y1 = y2; + } +}. + +end ROM. diff --git a/proofs/HashFunctionsx2.eca b/proofs/HashFunctionsx2.eca index c3eca6e..0900849 100644 --- a/proofs/HashFunctionsx2.eca +++ b/proofs/HashFunctionsx2.eca @@ -1,31 +1,71 @@ require import AllCore. -require HashFunctions. - -type in_t. +type in_t1. +type in_t2. type out_t. -op f : in_t -> out_t. -clone import HashFunctions as F with - type in_t <- in_t, - type out_t <- out_t, - - op f <- f - - proof *. - +op f : in_t1 -> out_t. +op g : in_t2 -> out_t. -type in_t2. -type out_t2. -op g : in_t2 -> out_t2. +module type Adv_CRx2 = { + proc find() : in_t1 * in_t2 +}. + +module CRx2 (A : Adv_CRx2) = { + proc main() : bool = { + var x1 : in_t1; + var x2 : in_t2; + + (x1, x2) <@ A.find(); + + return f x1 = g x2; + } +}. -clone import HashFunctions as G with - type in_t <- in_t2, - type out_t <- out_t2, - - op f <- g - - proof *. +theory ROM. + +module type KHF_RO1i = { + proc init() : unit + proc get(x : in_t1) : out_t +}. + +module type KHF_RO2i = { + proc init() : unit + proc get(x : in_t2) : out_t +}. + +module type KHF_RO1 = { + include KHF_RO1i [init] +}. + +module type KHF_RO2 = { + include KHF_RO2i [init] +}. + + +module type Adv_CRx2_ROM (F_RO : KHF_RO1) (G_RO : KHF_RO2) = { + include Adv_CRx2 +}. + + +module CRx2_ROM (F_RO : KHF_RO1i) (G_RO : KHF_RO2i) (A : Adv_CRx2_ROM) = { + proc main() : bool = { + var x1 : in_t1; + var x2 : in_t2; + var y1, y2 : out_t; + + F_RO.init(); + G_RO.init(); + + (x1, x2) <@ A(F_RO, G_RO).find(); + y1 <@ F_RO.get(x1); + y2 <@ G_RO.get(x2); + + return y1 = y2; + } +}. + +end ROM. diff --git a/proofs/KeyedHashFunctionsAlt.eca b/proofs/KeyedHashFunctionsAlt.eca new file mode 100644 index 0000000..d5b2c49 --- /dev/null +++ b/proofs/KeyedHashFunctionsAlt.eca @@ -0,0 +1,68 @@ +require import AllCore Distr. +require KeyedHashFunctionsx2. + +type key_t. + +type in_t. + +type out_t. + +op f : key_t -> in_t -> out_t. + +op dkey : key_t distr. + +module type Adv_CRAlt = { + proc find(k1 : key_t, k2 : key_t) : in_t * in_t +}. + +module CRAlt(A : Adv_CRAlt) = { + proc main() : bool = { + var k1, k2 : key_t; + var x1, x2 : in_t; + + k1 <$ dkey; + k2 <$ dkey; + + (x1, x2) <@ A.find(k1, k2); + + return f k1 x1 = f k2 x2; + } +}. + + +theory ROM. + +module type KHF_ROi = { + proc init() : unit + proc get(kx : key_t * in_t) : out_t +}. + +module type KHF_RO = { + include KHF_ROi [init] +}. + +module type Adv_CRAlt_ROM (F_RO : KHF_RO) = { + include Adv_CRAlt +}. + +module CRAlt_ROM (F_RO : KHF_ROi) (A : Adv_CRAlt_ROM) = { + proc main() : bool = { + var k1, k2 : key_t; + var x1, x2 : in_t; + var y1, y2 : out_t; + + F_RO.init(); + + k1 <$ dkey; + k2 <$ dkey; + + (x1, x2) <@ A(F_RO).find(k1, k2); + + y1 <@ F_RO.get((k1, x1)); + y2 <@ F_RO.get((k2, x2)); + + return y1 = y2; + } +}. + +end ROM. diff --git a/proofs/KeyedHashFunctionsx2.eca b/proofs/KeyedHashFunctionsx2.eca new file mode 100644 index 0000000..37b21cb --- /dev/null +++ b/proofs/KeyedHashFunctionsx2.eca @@ -0,0 +1,89 @@ +require import AllCore Distr. + +type key_t1. +type key_t2. + +type in_t1. +type in_t2. + +type out_t. + +op f : key_t1 -> in_t1 -> out_t. +op g : key_t2 -> in_t2 -> out_t. + +op dkey1 : key_t1 distr. +op dkey2 : key_t2 distr. + + +module type Adv_CRx2 = { + proc find(k1 : key_t1, k2 : key_t2) : in_t1 * in_t2 +}. + +module CRx2 (A : Adv_CRx2) = { + proc main() : bool = { + var k1 : key_t1; + var k2 : key_t2; + var x1 : in_t1; + var x2 : in_t2; + + k1 <$ dkey1; + k2 <$ dkey2; + + (x1, x2) <@ A.find(k1, k2); + + return f k1 x1 = g k2 x2; + } +}. + + + +theory ROM. + +module type KHF_RO1i = { + proc init() : unit + proc get(kx : key_t1 * in_t1) : out_t +}. + +module type KHF_RO2i = { + proc init() : unit + proc get(kx : key_t2 * in_t2) : out_t +}. + +module type KHF_RO1 = { + include KHF_RO1i [init] +}. + +module type KHF_RO2 = { + include KHF_RO2i [init] +}. + + +module type Adv_CRx2_ROM (F_RO : KHF_RO1) (G_RO : KHF_RO2) = { + include Adv_CRx2 +}. + + +module CRx2_ROM (F_RO : KHF_RO1i) (G_RO : KHF_RO2i) (A : Adv_CRx2_ROM) = { + proc main() : bool = { + var k1 : key_t1; + var k2 : key_t2; + var x1 : in_t1; + var x2 : in_t2; + var y1, y2 : out_t; + + F_RO.init(); + G_RO.init(); + + k1 <$ dkey1; + k2 <$ dkey2; + + (x1, x2) <@ A(F_RO, G_RO).find(k1, k2); + + y1 <@ F_RO.get((k1, x1)); + y2 <@ G_RO.get((k2, x2)); + + return y1 = y2; + } +}. + +end ROM. diff --git a/proofs/ML_KEM_HL_Binding_SM.eca b/proofs/ML_KEM_HL_Binding_SM.eca new file mode 100644 index 0000000..988198c --- /dev/null +++ b/proofs/ML_KEM_HL_Binding_SM.eca @@ -0,0 +1,282 @@ +(*^ + Binding security for (very) high-level specification of ML-KEM. + Specification considered here abstracts away from any algebraic + structure used in the construction, particularly + viewing the PKE procedures as abstract (black box) operators. + To be instantiated and linked to lower-level specification + and, in turn, implementation. +^*) +(* Require/Import *) +require import AllCore Distr. +require (*--*) DMap DProd. +require (*--*) KeyEncapsulationMechanisms. +require (*--*) HashFunctions KeyedHashFunctionsAlt KeyedHashFunctionsx2. + + +(* Types *) +(* General *) +(** Randomness ("seeds") **) +type rand_t. + + +(* Underlying PKE scheme (K-PKE) *) +(** Public keys **) +type pk_t_pke. + +(** Secret keys **) +type sk_t_pke. + +(** Plaintexts of underlying PKE scheme **) +type ptxt_t = rand_t. + +(** Ciphertexts **) +type ctxt_t_pke. + + +(* KEM (ML-KEM *) +(** Public keys **) +type pk_t = pk_t_pke. + +(** Secret keys **) +type sk_t = sk_t_pke * pk_t * rand_t * rand_t. + +(** Shared/session keys (symmetric) **) +type key_t = rand_t. + +(** Ciphertexts/Encapsulations **) +type ctxt_t = ctxt_t_pke. + + +(* Operators *) +(** Hash function H, used to hash public keys to randomness **) +op H : pk_t -> rand_t. + +(** + Hash function G, used to hash (pairs of) plaintexts and + hashes of public keys (randomness) to (pairs of) keys and randomness +**) +op G : ptxt_t * rand_t -> key_t * rand_t. + +(** + Hash function J, used to hash (pairs of) randomness and ciphertexts + to shared keys (for implicit rejection) +**) +op J : rand_t -> ctxt_t -> key_t. + +(** Operator capturing "derandomized" key generation of underlying PKE scheme **) +op kg : rand_t -> pk_t_pke * sk_t_pke. + +(** Operator capturing "derandomized" encryption function of underlying PKE scheme **) +op enc : rand_t -> pk_t_pke -> ptxt_t -> ctxt_t_pke. + +(** Operator capturing decryption function of underlying PKE scheme **) +(** + By design, the underlying PKE scheme never returns a failure, + so we refrain from using option monad as output. +**) +op dec : sk_t_pke -> ctxt_t_pke -> ptxt_t. + + +(* Distributions *) +(** Proper, full, and uniform distribution over randomness **) +op [lossless full uniform] drand : rand_t distr. + +(** Proper, full, and uniform distribution over (shared) keys **) +op [lossless full uniform] dkey : key_t distr. + +(** Proper, full, and uniform distribution over pairs of (shared) keys and randomness **) +op [lossless full uniform] dkeyrand : (key_t * rand_t) distr. + +(** `dkeyrand` is equal to the product distribution of dkey and drand **) +lemma dkeyrand_dprod : dkeyrand = dkey `*` drand. +proof. +rewrite &(eq_funi_ll) ?is_full_funiform ?(dkeyrand_ll, dkeyrand_fu, dkeyrand_uni). ++ by rewrite dprod_fu_auto ?(dkey_fu, drand_fu) /=. ++ by rewrite dprod_uni 1,2:(dkey_uni, drand_uni). +by rewrite dprod_ll_auto 1,2:(dkey_ll, drand_ll). +qed. + +(** Distribution representing key generation of underlying PKE scheme **) +op dkg : (pk_t_pke * sk_t_pke) distr = dmap drand kg. + +(** `dkg` is a proper distribution **) +lemma dkg_ll : is_lossless dkg. +proof. by rewrite dmap_ll drand_ll. qed. + + +(* Clones/Imports *) +(* Definitions and properties for H as a (non-keyed) hash function *) +clone import HashFunctions as H_HF with + type in_t <- pk_t, + type out_t <- rand_t, + + op f <- H + + proof *. + +(* Definitions and properties for G as a (non-keyed) hash function +clone import HashFunctions as G_HF with + type in_t <- ptxt_t * rand_t, + type out_t <- key_t * rand_t, + + op f <- G + + proof *. +*) + +(* Definitions and properties for J as a (non-keyed) hash function +clone import HashFunctions as J_HF with + type in_t <- rand_t * ctxt_t, + type out_t <- key_t, + + op f <- J + + proof *. +*) + +(* Definitions and properties for KEMs with types as required for ML-KEM *) +clone import KeyEncapsulationMechanisms as KEMs with + type pk_t <- pk_t, + type sk_t <- sk_t, + type key_t <- key_t, + type ctxt_t <- ctxt_t + + proof *. + + +(* Schemes *) +(** K-PKE, PKE scheme underlying ML-KEM **) +(** + As per FIPS 203, we specify the PKE in a derandomized manner. + That is, any procedure using randomness (i.e., key generation and encryption) + takes it as input rather than sampling it itself. This also means + it does not adhere to the regular syntax of a PKE scheme. +**) +(** + Further, this is a (very) high-level specification, essentially abstracting + away all algebraic structure and modeling the procedures as simple operators + (which is possible because all randomness is taken as input) +**) +module K_PKE_HL = { + proc keygen(d : rand_t) : pk_t_pke * sk_t_pke = { + return kg d; + } + + proc enc(pk : pk_t_pke, p : ptxt_t, r : rand_t) : ctxt_t_pke = { + return enc r pk p; + } + + proc dec(sk : sk_t_pke, c : ctxt_t_pke) : ptxt_t = { + return dec sk c; + } +}. + +(** + ML-KEM in the standard model. + Closely follows FIPS 203 (without accounting for sampling failures, so + the "internal" ML-KEM procedures--as they are called in FIPS 203--are + most similar). +**) +module ML_KEM_HL : Scheme = { + proc keygen() : pk_t * sk_t = { + var pk_pke : pk_t_pke; + var sk_pke : sk_t_pke; + var d, z : rand_t; + var pk : pk_t; + var sk : sk_t; + + d <$ drand; + z <$ drand; + + (pk_pke, sk_pke) <@ K_PKE_HL.keygen(d); + + pk <- pk_pke; + sk <- (sk_pke, pk, H pk, z); + + return (pk, sk); + } + + proc encaps(pk : pk_t) : key_t * ctxt_t = { + var p, r : rand_t; + var k : key_t; + var c : ctxt_t_pke; + + p <$ drand; + (k, r) <- G (p, H pk); + + c <@ K_PKE_HL.enc(pk, p, r); + + return (k, c); + } + + proc decaps(sk : sk_t, c : ctxt_t) : key_t option = { + var pk_pke : pk_t_pke; + var sk_pke : sk_t_pke; + var h, z, r' : rand_t; + var p' : ptxt_t; + var k', k_ : key_t; + var c' : ctxt_t; + + (sk_pke, pk_pke, h, z) <- sk; + + p' <@ K_PKE_HL.dec(sk_pke, c); + + (k', r') <- G (p', h); + k_ <- J z c; + + c' <@ K_PKE_HL.enc(pk_pke, p', r'); + + if (c <> c') { + k' <- k_; + } + + return Some k'; + } +}. + + +(* + +*) +clone import KeyedHashFunctionsAlt as KHF_J with + type key_t <- rand_t, + type in_t <- ctxt_t, + type out_t <- key_t, + + op f <- J, + + op dkey <- drand + + proof *. + +op G' (r : rand_t) (p : ptxt_t) : key_t * rand_t = G (p, r). + +clone import KeyedHashFunctionsAlt as KHF_Gp with + type key_t <- rand_t, + type in_t <- ptxt_t, + type out_t <- key_t * rand_t, + + op f <- G', + + op dkey <- drand + + proof *. + +op G'' (r : rand_t) (p : ptxt_t) : key_t = (G (p, r)).`1. + +clone import KeyedHashFunctionsx2 as KHF_JGpp with + type key_t1 <- rand_t, + type in_t1 <- ctxt_t, + type key_t2 <- rand_t, + type in_t2 <- ptxt_t, + + type out_t <- key_t, + + op f <- J, + op g <- G'', + + op dkey1 <- drand, + op dkey2 <- drand + + proof *. + diff --git a/proofs/ROMx2.eca b/proofs/ROMx2.eca new file mode 100644 index 0000000..77e0189 --- /dev/null +++ b/proofs/ROMx2.eca @@ -0,0 +1,764 @@ +require import AllCore Distr List FMap PROM. + +(* Auxiliary properties *) +lemma size_behead (s : 'a list) : + size (behead s) = if s = [] then 0 else size s - 1. +proof. by elim: s. qed. + +lemma behead_drop (s : 'a list) (n : int) : + 0 <= n => behead (drop n s) = drop (n + 1) s. +proof. by elim: s n => // /#. qed. + +lemma eq_ss (s1 s2 : 'a list) : + uniq s1 => mem s1 <= mem s2 => size s2 <= size s1 => perm_eq s1 s2. +proof. +elim: s1 s2 => [| x l ih s2 /= [ninl uql] lemem le1sz]; 1: smt(size_ge0). +move: (ih (rem x s2) uql _ _); 1,2: smt(mem_rem_neq size_rem). +rewrite -(perm_cons x) => peqxc. +rewrite (perm_eq_trans _ _ _ peqxc) perm_eq_sym perm_to_rem 1:/#. +qed. + +lemma uniq_drop (s : 'a list) (n : int) : + uniq s => uniq (drop n s). +proof. by elim: s n => // /#. qed. + + +(* Types *) +(** Input type of first oracle **) +type in_t1. + +(** Input type of second oracle **) +type in_t2. + +(* Output type of oracles *) +type out_t. + + +(* Distributions *) +(* Distribution over output type *) +op [lossless] dout : out_t distr. + + +(* Oracles *) +(** + Interface of (first type of) random oracle for security notions, + exposes both initialization and query +**) +module type RandomOracle1i = { + proc init() : unit + proc get(x : in_t1) : out_t +}. + +(** + Interface of (second type of) random oracle for security notions, + exposes both initialization and query +**) +module type RandomOracle2i = { + proc init() : unit + proc get(x : in_t2) : out_t +}. + +(** + Interface of (first type of) random oracle for security notions, + exposes both initialization and query +**) +module type RandomOracle1 = { + include RandomOracle1i [get] +}. + +(** + Interface of (second type of) random oracle for security notions, + exposes both initialization and query +**) +module type RandomOracle2 = { + include RandomOracle2i [get] +}. + + +(** Default implementation for first (type of) oracle **) +module RO1_Default : RandomOracle1i = { + var m : (in_t1, out_t) fmap + + proc init() : unit = { + m <- empty; + } + + proc get(x : in_t1) = { + var r : out_t; + + r <$ dout; + if (x \notin m) { + m.[x] <- r; + } + + return oget m.[x]; + } +}. + +(** Default implementation of second (type of) oracle **) +module RO2_Default : RandomOracle2i = { + var m : (in_t2, out_t) fmap + + proc init() : unit = { + m <- empty; + } + + proc get(x : in_t2) = { + var r : out_t; + + r <$ dout; + if (x \notin m) { + m.[x] <- r; + } + + return oget m.[x]; + } +}. + +(** Counting wrapper for first (type of) oracle **) +module Counting_RO1 (RO1 : RandomOracle1) : RandomOracle1 = { + var q : int + + proc get(x : in_t1) : out_t = { + var y : out_t; + + y <@ RO1.get(x); + + q <- q + 1; + + return y; + } +}. + +(** Counting wrapper for second (type of) oracle **) +module Counting_RO2 (RO2 : RandomOracle2) : RandomOracle2 = { + var q : int + + proc get(x : in_t2) : out_t = { + var y : out_t; + + y <@ RO2.get(x); + + q <- q + 1; + + return y; + } +}. + + +(* Security *) +(* Collision resistance between two random oracles (CR-ROM-x2) *) +(** Adversary class for CR-ROM-x2 **) +module type Adv_CRROMx2 (RO1 : RandomOracle1) (RO2 : RandomOracle2) ={ + proc find() : in_t1 * in_t2 +}. + +(** CR-ROM-x2 security game **) +module CR_ROM_x2 (RO1 : RandomOracle1i) (RO2 : RandomOracle2i) (A : Adv_CRROMx2) = { + proc main() : bool = { + var x1 : in_t1; + var x2 : in_t2; + var y1, y2 : out_t; + + RO1.init(); + RO2.init(); + + (x1, x2) <@ A(RO1, RO2).find(); + + y1 <@ RO1.get(x1); + y2 <@ RO2.get(x2); + + return y1 = y2; + } +}. + + + +section. +(* Declare arbitrary adversary against CR-ROM-x2 *) +declare module A <: Adv_CRROMx2 { -RO1_Default, -RO2_Default, -Counting_RO1, -Counting_RO2 }. + +(* By assumption, the adversary's finding procedure terminates (given that its oracles terminate) *) +declare axiom A_find_ll (RO1 <: RandomOracle1{-A}) (RO2 <: RandomOracle2{-A}) : + islossless RO1.get => islossless RO2.get => islossless A(RO1, RO2).find. + +(* + By assumption, the number of adversary queries is bounded + (by some non-negative constants) +*) +declare op q1 : { int | 0 <= q1 } as ge0_q1. +declare axiom A_find_qs1 (RO1 <: RandomOracle1{-A}) (RO2 <: RandomOracle2{-A}) (n : int) : + hoare[A(Counting_RO1(RO1), RO2).find : Counting_RO1.q = n ==> Counting_RO1.q <= n + q1]. + +declare op q2 : { int | 0 <= q2 } as ge0_q2. +declare axiom A_find_qs2 (RO1 <: RandomOracle1{-A}) (RO2 <: RandomOracle2{-A}) (n : int) : + hoare[A(RO1, Counting_RO2(RO2)).find : Counting_RO2.q = n ==> Counting_RO2.q <= n + q2]. + +(* + Prove the conjucntion of the above assumptions + regarding the adversary's oracle queries +*) +lemma A_find_qs (RO1 <: RandomOracle1{-A}) (RO2 <: RandomOracle2{-A}) (n1 n2 : int) : + hoare[A(Counting_RO1(RO1), Counting_RO2(RO2)).find : + Counting_RO1.q = n1 /\ Counting_RO2.q = n2 ==> + Counting_RO1.q <= n1 + q1 /\ Counting_RO2.q <= n2 + q2]. +proof. by conseq (A_find_qs1 RO1 (Counting_RO2(RO2)) n1) (A_find_qs2 (Counting_RO1(RO1)) RO2 n2). qed. + + +(* + Clone and import relevant ROM-related results + for first (type of) random oracle +*) +local clone FullRO as FullRO1 with + type in_t <- in_t1, + type out_t <- out_t, + + op dout <- fun _ => dout, + + type d_in_t <- unit, + type d_out_t <- bool + + proof *. + +(* + Clone and import relevant ROM-related results + for first (type of) random oracle +*) +local clone FullRO as FullRO2 with + type in_t <- in_t2, + type out_t <- out_t, + + op dout <- fun _ => dout, + + type d_in_t <- unit, + type d_out_t <- bool + + proof *. + +(* + Clone and import relevant ROM-related results for an + intermediate (auxiliary) RO in order to perform lazy-eager argument on + RO1 (can do similarly on RO2 if desired). +*) +local clone import FullRO as FullROI with + type in_t <- int, + type out_t <- out_t, + + type d_in_t <- unit, + type d_out_t <- bool, + + op dout <- fun _ => dout + + proof *. + + +(* + Step (1): + Show equivalence between original game and one where the default + random oracles are replaced by their more advanced (lazy) variants from the + PROM theory (as to be able to utilize the results from PROM later) +*) +local equiv Eqv_CRROMx2_PROM : + CR_ROM_x2(RO1_Default, RO2_Default, A).main ~ CR_ROM_x2(FullRO1.LRO, FullRO2.LRO, A).main : + ={glob A} ==> ={res}. +proof. by proc; sim. qed. + + +(* + Auxiliary oracle that simulates the first random oracle + by employing an intermediate (type of) oracle. This is the key to + performing the lazy sampling -> eager sampling step: If ROI is instantiated with + the lazy oracle, ROI.sample does nothing and, hence, RO1_WI.init will do nohting + but initialize i to 0; if ROI is instantiated with the + eager oracle, ROI.sample is the same as ROI.get and, hence, RO1_WI.init will + already eagerly sample q1 oracle mappings/entries. + Note that the map and q are assumed to be initialized by the game, in order to + massage everything into the right form for the results from PROM. +*) +local module RO1_WI (ROI : FullROI.RO) : FullRO1.RO = { + include var FullRO1.RO [-init, get] + var qu : int + + proc init() : unit = { + var i : int; + + i <- 0; + while (i < q1) { + ROI.sample(i); + i <- i + 1; + } + } + + proc get(x : in_t1) : out_t = { + var y : out_t; + + if (x \notin FullRO1.RO.m) { + y <@ ROI.get(qu); + FullRO1.RO.m.[x] <- y; + qu <- qu + 1; + } else { + y <- oget FullRO1.RO.m.[x]; + } + + return y; + } +}. + + +(* + Auxiliary intermediate variant of CR-ROM-x2 that + uses the above auxiliary oracle (RO1_W) instead of RO1. + This acts as the distinguisher between the lazy and eager + oracles (of the intermediate type). + Uses a separate procedure to have the correct form + for the results from PROM. +*) +local module CR_ROM_x2_I (ROI : FullROI.RO) = { + proc distinguish() = { + var x1 : in_t1; + var x2 : in_t2; + var y1, y2 : out_t; + + RO1_WI(ROI).init(); + + (x1, x2) <@ A(RO1_WI(ROI), FullRO2.LRO).find(); + + if (x1 \notin FullRO1.RO.m) { + y1 <$ dout; + } else { + y1 <- oget FullRO1.RO.m.[x1]; + } + + if (x2 \notin FullRO2.RO.m) { + y2 <$ dout; + } else { + y2 <- oget FullRO2.RO.m.[x2]; + } + + return y1 = y2; + } + + proc main() = { + var b : bool; + + ROI.init(); + FullRO1.RO.m <- empty; + RO1_WI.qu <- 0; + FullRO2.RO.m <- empty; + + b <@ distinguish(); + + return b; + } +}. + +(* + Step (2): + Show equivalence between original CR-ROM-x2 (with the first and second + type of lazy oracles from PROM) + and the above auxiliary intermediate CR-ROM-x2 using the intermediate type + of lazy oracle from PROM. +*) +local equiv Eqv_CRROMx2RO_ILRO : + CR_ROM_x2(FullRO1.LRO, FullRO2.LRO, A).main ~ CR_ROM_x2_I(FullROI.LRO).main : + ={glob A} ==> ={res}. +proof. +proc. +inline{2} distinguish. +seq 2 5 : ( ={glob A} + /\ FullRO1.RO.m{1} = empty + /\ FullRO1.RO.m{2} = empty + /\ FullRO2.RO.m{1} = empty + /\ FullRO2.RO.m{2} = empty + /\ FullROI.RO.m{2} = empty + /\ RO1_WI.qu{2} = 0). ++ inline *. + while{2} (true) (q1 - i{2}). + + by auto => /> /#. + by auto => />; smt(ge0_q1). +inline get. +seq 1 1 : ( ={x1, x2, FullRO1.RO.m, FullRO2.RO.m} + /\ RO1_WI.qu{2} \notin RO.m{2}). ++ call (: ={FullRO1.RO.m, FullRO2.RO.m} + /\ dom RO.m{2} = mem (range 0 RO1_WI.qu{2}) + /\ 0 <= RO1_WI.qu{2}). + + proc. + by wp; rnd. + + proc. + inline{2} get. + case (x{1} \notin FullRO1.RO.m{1}). + + rcondt{1} ^if; 1: by auto. + rcondt{2} ^if; 1: by auto. + rcondt{2} ^if; 1: move => &m. + + rnd; wp; skip => /> &m'. + by rewrite fun_ext => /(_ RO1_WI.qu{m'}); rewrite mem_range => -> /#. + by wp; rnd; wp; skip => /> &m; smt(get_set_sameE mem_range mem_set). + rcondf{1} ^if; 1: by auto. + rcondf{2} ^if; 1: by auto. + by rnd{1}; wp. + by skip => />; smt(mem_empty mem_range). +sp 1 0. +case (x{1} \notin FullRO1.RO.m{1}). ++ rcondt{1} ^if; 1: by auto. + rcondt{2} ^if; 1: by auto. + case (x2{1} \notin FullRO2.RO.m{1}). + + rcondt{1} ^if; 1: by auto. + rcondt{2} ^if; 1: by auto. + by auto => />; smt(get_set_sameE). + + rcondf{1} ^if; 1: by auto. + rcondf{2} ^if; 1: by auto. + by wp; rnd{1}; wp; rnd; skip => />; smt(get_set_sameE). +rcondf{1} ^if; 1: by auto. +rcondf{2} ^if; 1: by auto. +case (x2{1} \notin FullRO2.RO.m{1}). ++ rcondt{1} ^if; 1: by auto. + rcondt{2} ^if; 1: by auto. + auto => />; smt(get_set_sameE). +rcondf{1} ^if; 1: by auto. +rcondf{2} ^if; 1: by auto. +by wp; rnd{1}; wp; rnd{1}; skip. +qed. + + +(* + Step (3): + Apply the results from PROM to show move from lazy sampling to eagerly sampling + (up to q1 queries) for the first (type of) random oracle. +*) +local equiv Eqv_CRROMx2RS_Dist_LRO_RO : + CR_ROM_x2_I(FullROI.LRO).distinguish ~ CR_ROM_x2_I(FullROI.RO).distinguish : + ={glob CR_ROM_x2_I, FullROI.RO.m} ==> ={res, glob CR_ROM_x2_I}. +proof. +symmetry. +conseq (FullROI.FullEager.RO_LRO_D CR_ROM_x2_I _) => //. +by move => ?; apply dout_ll. +qed. + +local equiv Eqv_CRROMx2RS_Main_LRO_RO : + CR_ROM_x2_I(FullROI.LRO).main ~ CR_ROM_x2_I(FullROI.RO).main : + ={glob A} ==> ={res}. +proof. +proc. +seq 4 4 : ( ={glob CR_ROM_x2_I, FullROI.RO.m}); 1: by inline *; auto. +by rewrite equiv[{1} 1 Eqv_CRROMx2RS_Dist_LRO_RO]; sim. +qed. + + +(* + Auxiliary first oracle that directly eagerly samples + q1 oracle mappings/entries. Effectively an inlined + version of RO1_WI(FullROI.RO). +*) +local module RO1_Eager : RandomOracle1i = { + import var FullRO1.RO + var mi : (int, out_t) fmap + + proc init() = { + var y : out_t; + + m <- empty; + + mi <- empty; + while (fsize mi < q1) { + y <$ dout; + mi.[fsize mi] <- y; + } + } + + proc get(x : in_t1) = { + var y : out_t; + + if (x \notin m) { + if (fsize m < q1) { + m.[x] <- oget mi.[fsize m]; + } + y <- oget m.[x]; + } else { + y <- oget m.[x]; + } + + return y; + } +}. + +(* + Auxiliary version of CR-ROM-x2 that employs the above + eagerly sampling first oracle (i.e., RO1_Eager). Splits up + execution in separate procedures, as well as moves some local variables + to the module level, to massage it into the right form for using the FEL +*) +local module CR_ROM_x2_Eager1 = { + var x1 : in_t1 + var x2 : in_t2 + + proc advcr() : unit = { + RO1_Eager.init(); + FullRO2.RO.init(); + + (x1, x2) <@ A(RO1_Eager, FullRO2.LRO).find(); + } + + proc main() = { + var y1, y2 : out_t; + + advcr(); + + if (x1 \notin FullRO1.RO.m) { + y1 <$ dout; + } else { + y1 <- oget FullRO1.RO.m.[x1]; + } + + if (x2 \notin FullRO2.RO.m) { + y2 <$ dout; + } else { + y2 <- oget FullRO2.RO.m.[x2]; + } + + return y1 = y2; + } +}. + +(* +declare axiom A_find_qs1 (RO1 <: RandomOracle1{-A}) (RO2 <: RandomOracle2{-A}) (n : int) : + hoare[A(Counting_RO1(RO1), RO2).find : Counting_RO1.q = n ==> Counting_RO1.q <= n + q1]. +*) +(* + Step (3.5): + Translate the assumption regarding the adversary's (first) oracle + queries to a concrete statement usable in the current stage + of the proof. +*) +local lemma A_find_qs1_RO1WI : + hoare[A(RO1_WI(RO), FullRO2.LRO).find : RO1_WI.qu = 0 ==> RO1_WI.qu <= q1]. +proof. +have eqv_qqu : + equiv[ A(RO1_WI(RO), FullRO2.LRO).find ~ A(Counting_RO1(RO1_WI(RO)), FullRO2.LRO).find : + ={glob A, glob RO, glob RO1_WI, glob FullRO2.LRO} /\ RO1_WI.qu{2} <= Counting_RO1.q{2} + ==> + ={res, RO1_WI.qu} /\ RO1_WI.qu{2} <= Counting_RO1.q{2}]. ++ proc (={glob RO, glob RO1_WI, glob FullRO2.LRO} /\ RO1_WI.qu{2} <= Counting_RO1.q{2}) => //. + + by proc; auto. + proc; inline get. + sp 0 1. + by if => //; auto => /> /#. +conseq eqv_qqu (: Counting_RO1.q = 0 ==> Counting_RO1.q <= q1); 1,2: by smt(). +by apply (A_find_qs1 (RO1_WI(RO)) (FullRO2.LRO)). +qed. + +(* + Step (4): + Show equivalence between (1) auxiliary CR-ROM-x2 using RO1_WI(RO) as first oracle + and (2) auxiliary CR-ROM-x2 using RO1_Eager as first oracle +*) +local equiv Eqv_CRROMx2RO_ILROT_RS : + CR_ROM_x2_I(FullROI.RO).main ~ CR_ROM_x2_Eager1.main : + ={glob A} ==> ={res}. +proof. +proc. +inline{1} init distinguish. +inline{2} advcr init. +seq 6 4 : ( ={glob A} + /\ FullRO1.RO.m{1} = empty + /\ FullRO1.RO.m{2} = empty + /\ FullRO2.RO.m{1} = empty + /\ FullRO2.RO.m{2} = empty + /\ FullROI.RO.m{1} = RO1_Eager.mi{2} + /\ dom FullROI.RO.m{1} = mem (range 0 q1) + /\ RO1_WI.qu{1} = 0). ++ swap{2} 4 -1. + while ( FullROI.RO.m{1} = RO1_Eager.mi{2} + /\ dom FullROI.RO.m{1} = mem (range 0 i{1}) + /\ i{1} = fsize FullROI.RO.m{1} + /\ i{1} <= q1). + + inline{1} sample get. + sp; rcondt{1} ^if; first by auto => />; smt(mem_range). + by wp; rnd; skip => /> &2; smt(ge0_q1 mem_set mem_range fsize_set ge0_fsize). + by wp; skip => />; smt(ge0_q1 fsize_empty mem_empty mem_range). +wp. +seq 1 1 : ( ={FullRO2.RO.m, FullRO1.RO.m} + /\ x1{1} = CR_ROM_x2_Eager1.x1{2} + /\ x2{1} = CR_ROM_x2_Eager1.x2{2}); 2: by sim. +call (: ={glob A} + /\ FullRO1.RO.m{1} = empty + /\ FullRO1.RO.m{2} = empty + /\ FullRO2.RO.m{1} = empty + /\ FullRO2.RO.m{2} = empty + /\ RO.m{1} = RO1_Eager.mi{2} + /\ dom RO.m{1} = mem (range 0 q1) + /\ RO1_WI.qu{1} = 0 + ==> + RO1_WI.qu{1} <= q1 + /\ (RO1_WI.qu{1} <= q1 => + ={FullRO1.RO.m, FullRO2.RO.m, res})). ++ conseq (: RO1_WI.qu{1} <= q1 => ={FullRO1.RO.m, FullRO2.RO.m, res}) + A_find_qs1_RO1WI _ => //. + symmetry. + proc (q1 < RO1_WI.qu) + ( ={FullRO1.RO.m, FullRO2.RO.m} + /\ fsize FullRO1.RO.m {1} = RO1_WI.qu{2} + /\ RO.m{2} = RO1_Eager.mi{1} + /\ dom RO.m{2} = mem (range 0 q1)) => //; 1,2: smt(fsize_empty). + + by move => RO1 RO2 RO1ll RO2ll; apply (A_find_ll RO1 RO2 RO2ll RO1ll). + + by proc; auto. + + by move=> &2 lt_qu; proc; auto; smt(dout_ll). + + by move=> _; proc; auto; smt(dout_ll). + + proc; inline get. + if => //; 2: by wp; skip. + by wp; rnd{2}; wp; skip => />; smt(get_setE mem_range fsize_set ge0_fsize). + + move=> &2 ltqu_q1. + by proc; wp. + move => _. + proc. inline get. + if => //; 2: by wp. + by wp; rnd; wp; skip => />; smt(dout_ll). +by skip => />. +qed. + +(* + Step (5): + Show the bound on a relevant collision occuring by queries of the adversary + (i.e., the final potential samplings after the adversary has returned are not + taken into account here). +*) +local lemma Bnd_CRROMx2Eager1V_CR_RS &m : + Pr[CR_ROM_x2_Eager1.advcr() @ &m : + fsize FullRO2.RO.m <= q2 + /\ CR_ROM_x2_Eager1.x1 \in FullRO1.RO.m + /\ CR_ROM_x2_Eager1.x2 \in FullRO2.RO.m + /\ FullRO1.RO.m.[CR_ROM_x2_Eager1.x1] = FullRO2.RO.m.[CR_ROM_x2_Eager1.x2]] + <= + (q1 * q2)%r * p_max dout. +proof. +fel 2 + (fsize FullRO2.RO.m) + (fun _ => q1%r * p_max dout) + q2 + (exists (x1 : int) (x2 : in_t2), + x1 \in RO1_Eager.mi + /\ x2 \in FullRO2.RO.m + /\ RO1_Eager.mi.[x1] = FullRO2.RO.m.[x2]) + [ RO1_Eager.get : false; FullRO2.LRO.get : (arg \notin FullRO2.RO.m) ] + ( dom RO1_Eager.mi = mem (range 0 q1) + /\ rng FullRO1.RO.m <= rng RO1_Eager.mi + /\ fsize RO1_Eager.mi = q1) => //. ++ by rewrite StdBigop.Bigreal.BRA.sumri_const 1:ge0_q2 RField.intmulr /#. ++ move => &m0 [#] leq2_fsz x1in x2in coll [#] eqdm lerng eqq1_fsz. + split; 2: smt(). + by move: lerng => /(_ (oget FullRO1.RO.m{m0}.[CR_ROM_x2_Eager1.x1{m0}]) _) /#. ++ inline init. + wp; sp. + while ( dom RO1_Eager.mi = mem (range 0 (fsize RO1_Eager.mi)) + /\ fsize RO1_Eager.mi <= q1). + + by wp; rnd; skip => /> &m0 eqdm _ ltq1_fsz y0 _; smt(mem_set mem_range ge0_fsize fsize_set). + by skip => />; smt(ge0_q1 mem_empty mem_range fsize_empty emptyE). ++ move => b c /=. + proc. + by wp; skip => /> &2; smt(rng_set domE rem_id mem_range ge0_fsize). ++ proc. + rcondt ^if; 1: by rnd. + wp; rnd; skip => /> &m0 ge0_fsz ltq_fsz nex eqdm lerng eqq1_fsz x0nin. + apply (StdOrder.RealOrder.ler_trans + (mu dout (fun y => exists (i : int), + dom RO1_Eager.mi{m0} i /\ RO1_Eager.mi{m0}.[i] = Some y))). + + by apply mu_sub => k -[x1 x2] []; smt(get_setE). + rewrite -eqq1_fsz Mu_mem.mu_mem_le_fsize => u ? /= -@/pred1. + by apply (StdOrder.RealOrder.ler_trans (mu1 dout (oget RO1_Eager.mi{m0}.[u]))); smt(mu_sub pmax_upper_bound). ++ move => c. + proc. + by wp; rnd; skip => />; smt(fsize_set). +move => b c /=. +proc. +rcondf ^if; 1: by auto. +by rnd. +qed. + + +end section. + + + +(* + One Output, One Function version (of CR-ROM-x2): + Adversary asked to provide single output x such that + RO1(x) collides with RO2(f a x) for some fixed, known f and a +*) +abstract theory OOOF. +(* Additional auxiliary input to function mapping between random oracle inputs *) +type aux_t. + +(* Function mapping between random oracle inputs*) +op f : aux_t -> in_t1 -> in_t2. + + +(* Security *) +(* Collision resistance between two random oracles (CR-ROM-x2) *) +(** Adversary class for CR-ROM-x2 **) +module type Adv_CRROMx2_OOOF (RO1 : RandomOracle1) (RO2 : RandomOracle2) = { + proc find(a : aux_t) : in_t1 +}. + +(** CR-ROM-x2 security game **) +module CR_ROM_x2_OOOF (RO1 : RandomOracle1i) (RO2 : RandomOracle2i) (A : Adv_CRROMx2_OOOF) = { + proc main(a : aux_t) : bool = { + var x : in_t1; + var y1, y2 : out_t; + + RO1.init(); + RO2.init(); + + x <@ A(RO1, RO2).find(a); + + y1 <@ RO1.get(x); + y2 <@ RO2.get(f a x); + + return y1 = y2; + } +}. + +end OOOF. + + +(* + One Output, Two Functions version (of CR-ROM-x2): + Adversary asked to provide single output x such that + RO1(x) collides with RO2(f a x) for some fixed, known f and a +*) +abstract theory OOTF. +(* Type of output provided by adversary, mapped to inputs of random oracles *) +type s_t. + +(* Additional auxiliary input to function mapping between random oracle inputs *) +type aux_t. + +(* Function mapping abetween random oracle inputs *) +op f : aux_t -> s_t -> in_t1. +op g : aux_t -> s_t -> in_t2. + +(* Security *) +(* Collision resistance between two random oracles (CR-ROM-x2) *) +(** Adversary class for CR-ROM-x2 **) +module type Adv_CRROMx2_OOTF (RO1 : RandomOracle1) (RO2 : RandomOracle2) = { + proc find(a : aux_t) : s_t +}. + +(** CR-ROM-x2 security game **) +module CR_ROM_x2_SOSF (RO1 : RandomOracle1i) (RO2 : RandomOracle2i) (A : Adv_CRROMx2_OOTF) = { + proc main(a : aux_t) : bool = { + var x : s_t; + var y1, y2 : out_t; + + RO1.init(); + RO2.init(); + + x <@ A(RO1, RO2).find(a); + + y1 <@ RO1.get(f a x); + y2 <@ RO2.get(g a x); + + return y1 = y2; + } +}. + +end OOTF. +