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

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

(* Queries *)

event forge.
query event forge ==> false.

channel cgen, cS, cT.

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

let processT = 
	in(cT, (m':bitstring, s:D));
	if f(pk, s) = hash(m') then
	find j <= qS suchthat defined(m[j]) && (m' = m[j]) then yield else
	event forge.

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