(* OAEP scheme, proof of CPA security *)

proof {
      crypto rom(H);
      crypto rom(G);
      show_game occ;
      insert_event bad1 31;
      show_game occ;
      insert_event bad2 59;
      crypto remove_xor(xorDr);
      crypto remove_xor(xorDow);      
      remove_assign binder pk;
      crypto pd_ow(f);
      success
}

param qS.

type pkey [bounded].
type skey [bounded].
type seed [large,fixed].
type D [fixed,large].
type Dow [fixed,large].
type Dr [fixed,large].

(* Set partial-domain one-way trapdoor permutation *)

proba P_PD_OW.

expand set_PD_OW_trapdoor_perm(seed, pkey, skey, D, Dow, Dr, pkgen, skgen, f, invf, concat, P_PD_OW).

(* Hash functions, random oracle model *)

type hashkey [fixed].

channel chG1, chG2, chH1, chH2.

expand ROM_hash(hashkey, Dr, Dow, G, oG, qG).
let hashoracleG(hkg: hashkey) = !iG <= qG in(chG1, x:Dr); out(chG2, G(hkg,x)).

expand ROM_hash(hashkey, Dow, Dr, H, oH, qH).
let hashoracleH(hkh: hashkey) = !iH <= qH in(chH1, x:Dow); out(chH2, H(hkh,x)).

(* concatenation *)
type Dm.
type Dz [large].

fun concatm(Dm,Dz):Dow [data].
const zero: Dz.

(* Xor *)

expand Xor(Dow, xorDow, zeroDow).
expand Xor(Dr, xorDr, zeroDr).

(* Implementing a test as a function.
   Useful to avoid expanding if, which is necessary for this proof. *)

fun test(bool, Dm, Dm):Dm.
equation forall x:Dm,y:Dm; test(true,x,y) = x.
equation forall x:Dm,y:Dm; test(false,x,y) = y.

(* Queries *)

channel start, c0, c1, c2.

query secret b1.

let processT(hkg: hashkey, hkh: hashkey, pk: pkey) = 
	in(c1, (m1: Dm, m2: Dm));
	new b1: bool;
	(* The next line is equivalent to an "if" that will not be
	expanded. This is necessary for the system to succeed in
	proving the protocol. *)
	let menc = test(b1, m1, m2) in
	new r: Dr;
	let s = xorDow(concatm(menc, zero), G(hkg,r)) in
	let t = xorDr(r, H(hkh,s)) in
	out(c2, f(pk, concat(s,t))).

process 
	in(start, ());
	new hkh: hashkey;
	new hkg: hashkey;
	new r: seed; 
	let pk = pkgen(r) in
	let sk = skgen(r) in
	out(c0, pk);
	(hashoracleG(hkg) | hashoracleH(hkh) | processT(hkg, hkh, pk))


(* EXPECTED
All queries proved.
0.030s (user 0.030s + system 0.000s), max rss 19856K
END *)