(* FDH signature scheme *)

param qS.

type pkey [bounded].
type skey [bounded].
type seed [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.

let processS(hk: hashkey, sk: skey) =
	foreach iS <= qS do
	OS(m:bitstring) :=
	return(invf(sk, hash(hk, m))).

let processT(hk: hashkey, pk: pkey) = 
	OT(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 
	Ostart() :=
	hk <-R hashkey;
	r <-R seed; 
	let pk = pkgen(r) in
	let sk = skgen(r) in
	return(pk);
	(run processS(hk,sk) | run processT(hk,pk) | run hashoracle(hk))


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