(* This file shows indifferentiability between
   (H1, x -> H2(H1(x), x)) and 
   (H1, H3)
   where H1, H2, H3 are independent random oracles.

   That is, it shows indistinguishability between
   (H1, H2, x -> H2(H1(x), x)) and
   (H1, H2', H3)
   where H2' simulates H2 using calls to H1 and H3. *) 

type hashkey1 [large, fixed].
type input1.
type output1 [large, fixed].

type hashkey2 [large, fixed].
type output2 [large, fixed].

expand ROM_hash(hashkey1, input1, output1, H1, hashoracle1, qH1').
expand ROM_hash_2(hashkey2, output1, input1, output2, H2, hashoracle2, qH2').

type hashkey3 [large, fixed].
expand ROM_hash(hashkey3, input1, output2, H3, hashoracle3, qH3').

proof {
      allowed_collisions noninteractive*small/large;
      		 (* prevent eliminating collisions with qH1^2/|output1| *)
      start_from_other_end;
      crypto rom(H3);
      crypto rom(H1);
      show_game occ;
      (* At the beginning of OH2, distinguish whether the call OH2(x2_1,y2_1) 
         is such that y2_1 = OH1(x2_1) for a previous call to OH1 [with index ri4] *)
      insert 32 "find u4 = ri4 <= qH1 suchthat defined(r_2[ri4], x_1[ri4]) && (y2_1 = x_1[ri4]) && (x2_1 = r_2[ri4]) then";
      simplify;
      merge_branches;
      remove_assign useless;
      show_game;
      start_from_other_end;
      crypto rom(H2);
      show_game;
      (* remove_assign on x1_7 = H1(...) to make explicit tests H1(..) = .. 
      	 which are nicely simplified by the equivalence rom(H1). *)
      remove_assign binder x1_7;
      crypto rom(H1);
      show_game occ;
      (* At the beginning of OH2, distinguish whether the call OH2(x2,y2) 
         is such that y2 = OH1(x2) for a previous call to OH1 [with index ri4],
	 similarly to what we did in the other game. *)
      insert 32 "find u4 = ri4 <= qH1 suchthat defined(r_5[ri4], x[ri4]) && (y2 = x[ri4]) && (x2 = r_5[ri4]) then";
      simplify;
      (* SArename r_3, the random result of OH2, to distinguish whether it is
         created for a call that matches a previous call to OH1 
	 (the "find" above succeeds) or not *)
      SArename r_3;
      remove_assign useless;
      show_game occ;
      (* Rewrite the "find" to remove "[unique]", to match the other game *)
      insert 80 "find u9 = ri9 <= qH2 suchthat defined(r_7[ri9], y2[ri9], x2[ri9]) && (x2 = x2[ri9]) && (y2 = y2[ri9]) then";
      simplify;
      remove_assign useless;
      show_game occ;
      (* Rewrite the "find" to replace the condition 
         (u4_1 = u4_1[ri_9]) with (y2 = y2[ri_9]) and 
         (x3[ri_8] = x[u4_1]) with (y2 = x3[ri_8]), to match the other game.
	 As a side-effect, [unique] is removed. 
	 (We cannot insert "find[unique]", since that would 
	 require us to prove uniqueness.) *)
      insert 46 "find ri9 <= qH2 suchthat defined(r_6[ri9], y2[ri9]) && (y2 = y2[ri9]) then orfind ri8 <= qH3 suchthat defined(r_4[ri8], x3[ri8]) && (y2 = x3[ri8]) then";
      simplify;
      remove_assign useless;
      show_game occ;
      (* Rewrite x[u4_1[ri_7]]) into y2[ri_7], to match the other game *)
      replace 116 "y2[ri_7]";
      show_game;
      start_from_other_end;
      (* Rewrite the "find" to remove "[unique]", as it was removed in the other game *)
      insert 46 "find ri3 <= qH2 suchthat defined(r[ri3], y2_1[ri3]) && (y2_1 = y2_1[ri3]) then orfind ri2 <= qH3 suchthat defined(r_1[ri2], x3_1[ri2]) && (y2_1 = x3_1[ri2]) then";
      simplify;
      remove_assign useless;
      show_game;
      success
 } 

param qH1 [noninteractive].
param qH2.
param qH3.



equivalence
    Ostart() :=
    hk1 <-R hashkey1;
    hk2 <-R hashkey2;
    return();
    ((foreach i <= qH1 do OH1(x: input1) := return(H1(hk1, x))) |
     (foreach i <= qH2 do OH2(x2: output1, y2: input1) := return(H2(hk2, x2,y2))) |
     (foreach i <= qH3 do
      HComb(x3: input1) := return(H2(hk2, H1(hk1, x3), x3))))

    Ostart() :=
    hk1 <-R hashkey1;
    hk3 <-R hashkey3;
    return();
    ((foreach i <= qH1 do OH1(x: input1) := return(H1(hk1, x))) |
     (foreach i <= qH2 do OH2(x2: output1, y2: input1) :=
     	     if x2 = H1(hk1, y2) then return(H3(hk3, y2)) else
	     find l <= qH2 suchthat defined(x2[l],y2[l],r2[l]) && x2 = x2[l] && y2 = y2[l] then
		 return(r2[l])
	     else
		 r2 <-R output2;
		 return(r2)) |
     (foreach i <= qH3 do
      HComb(x3: input1) := return(H3(hk3, x3))))


(*

Target game after 
      start_from_other_end;
      crypto rom(H3);
      crypto rom(H1);
      show_game occ;
      insert 32 "find u4 = ri4 <= qH1 suchthat defined(r_2[ri4], x_1[ri4]) && (y2_1 = x_1[ri4]) && (x2_1 = r_2[ri4]) then";
      simplify;
      merge_branches;
      remove_assign useless;

     Ostart() :=
      return();
      ((
        foreach i_3 <= qH1 do
        OH1(x_1: input1) :=
        find [unique] u_5 = ri_5 <= qH1 suchthat defined(r_2[ri_5], x_1[ri_5]) && (x_1 = x_1[ri_5]) then
          return(r_2[u_5])
        else
          r_2 <-R output1;
          return(r_2)
      ) | (
        foreach i_4 <= qH2 do
        OH2(x2_1: output1, y2_1: input1) :=
        find u4_1 = ri4_1 <= qH1 suchthat defined(r_2[ri4_1], x_1[ri4_1]) && (y2_1 = x_1[ri4_1]) && (x2_1 = r_2[ri4_1]) then
          find [unique] u_3 = ri_3 <= qH2 suchthat defined(r[ri_3], y2_1[ri_3]) && (y2_1 = y2_1[ri_3]) then
            return(r[u_3])
          orfind u_2 = ri_2 <= qH3 suchthat defined(r_1[ri_2], x3_1[ri_2]) && (y2_1 = x3_1[ri_2]) then
            return(r_1[u_2])
          else
            r <-R output2;
            return(r)
        else
          find l_1 = l <= qH2 suchthat defined(x2_1[l], y2_1[l], r2[l]) && (x2_1 = x2_1[l]) && (y2_1 = y2_1[l]) then
            return(r2[l_1])
          else
            r2 <-R output2;
            return(r2)
      ) | (
        foreach i_5 <= qH3 do
        HComb(x3_1: input1) :=
        find [unique] u_1 = ri_1 <= qH2 suchthat defined(r[ri_1], y2_1[ri_1]) && (x3_1 = y2_1[ri_1]) then
          return(r[u_1])
        orfind u = ri <= qH3 suchthat defined(r_1[ri], x3_1[ri]) && (x3_1 = x3_1[ri]) then
          return(r_1[u])
        else
          r_1 <-R output2;
          return(r_1)
      ))



EXPECTED
All queries proved.
0.112s (user 0.096s + system 0.016s), max rss 14736K
END

*)