(*set proverif -graph ~/Documents/proverif1.96/graphs*)
set attacker = active.
set ignoreTypes = false.
(* The channel*)
free c:channel.

type Ui.
type TS.
type N.
type ID.
type PW.
type request.
type credentials.
type pu.
type pv.


fun hash(ID,PW,TS):request.


fun check(ID,ID):bool
reduc forall x:ID; check(x,x) = true
otherwise forall x:ID,y:ID; check(x,y) = false.



event acceptsUser(request).
event acceptsGate(pu).
event termUser(pu).
event termGate(credentials).


(* Asymmetric key encryption *)


fun pk(pv): pu.
fun He(credentials , pu): credentials .
reduc forall m: credentials , sk: pv; Hd(He(m,pk(sk)),sk) = m.


query x:request,y:pu; inj-event(termUser(y))==> inj-event(acceptsUser(x)).
query x:pu,y:credentials; inj-event(termGate(y))==> inj-event(acceptsGate(x)).




let user(IDi:ID,PKGW:pu,Pwi:PW) =
  new ts:TS;
  let rq = hash(IDi,Pwi,ts) in
	out(c,rq);
  in(c,x:pu);
  if x = PKGW then
  event acceptsGate(PKGW);
  new cr:credentials;
  let c' = He(cr,PKGW) in
  out(c,c');
  event termUser(x);
  0.



let gateway(IDi:ID,Pwi:PW,PKGW:pu,PRGW:pv) =
	in(c,reqq:request);
  new ts2:TS;
  let reqq2 = hash(IDi,Pwi,ts2) in
  if reqq = reqq2 then
  event acceptsUser(reqq2);
  out(c,PKGW);
  in(c,x:credentials);
  let yy = Hd(x,PRGW) in
  new xx:credentials;
  if yy = xx then
  event termGate(yy).





  process
  new PKGW:pu;
  new Pwi:PW;
  new IDi:ID;
  new PKGW:pu;
  new PRGW:pv;
	(!user(IDi,PKGW,Pwi)) | (!gateway(IDi,Pwi,PKGW,PRGW))