(* 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).

param qH [noninteractive].
channel hc1, hc2.
let hashoracle = ! qH in(hc1, x: bitstring); out(hc2, hash(hk,x)).

(* Queries *)

event bad.
query event bad ==> false.

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

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

let processT = 
	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 | processT | hashoracle))


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