(* FDH signature scheme *)

param qS.

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

(* One-way trapdoor permutation *)

proba POW.

expand OW_trapdoor_perm(seed, pkey, skey, D, pkgen, skgen, f, invf, POW).

(* Hash function, random oracle model *)

type hashkey [fixed].

expand ROM_hash(hashkey, bitstring, D, hash, hashoracle, qH).

(* Queries *)

event bad.
query event(bad) ==> false.

channel c0, c1, c2, c3, c4, c5, start.

let processS(hk: hashkey, sk: skey) =
	! qS
	in(c1, m:bitstring);
	out(c2, invf(sk, hash(hk, m))).

let processT(hk: hashkey, pk: pkey) = 
	in(c3, (m':bitstring, s:D));
	if f(pk, s) = hash(hk, m') then
	find u <= qS suchthat defined(m[u]) && (m' = m[u]) then yield else
	event bad.

process 
	(in(start, ());
	new hk: hashkey;
	new r:seed; 
	let pk = pkgen(r) in
	let sk = skgen(r) in
	out(c0, pk);
	(processS(hk,sk) | processT(hk,pk) | hashoracle(hk)))


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