(* A model of the PaySafe payment protocol  *)
(* with an encoding to check for relay attacks *)
(* See http://www.cs.bham.ac.uk/~tpc/Relay/ for details *)

free c.

(* mac *)
fun mac/2.

(* Public key cryptography *)
fun pk/1.
fun encrypt/2.
reduc decrypt(encrypt(x,pk(y)),y) = x.

(* Signatures for certificates *)
fun sign/2.
reduc checksign(sign(x,y),pk(y)) = x.
reduc getmess(sign(x,y)) = x.

(* function for generating the session MAC key) *)
fun genSkey/2.

private free bankSignKey.
private free bankMacKey.
private free bankChannel.

data SELECT/0.
data PAYSYSDDF/0.
data AID/0.
data GPO/0.
data PDOL/0.
data READRECORD/0.
data GENERATEAC/0.

(* If the attacker can find a sequence of actions that make the reader *)
(* finish the protocol then a relay attack is possible. If the reader  *)
(* cannnot finish then the protocol is safe from relay attacks *)
private free readerFinish.
query attacker:readerFinish.


let Card1 = 
	  in (c, (=SELECT,=PAYSYSDDF));
	  out (c, AID);				
	  in (c,(=SELECT,=AID));
	  new nonceCard;	
	  out (c,PDOL);
	  in (c,(=GPO,amountToPay,nonceReader));
	  out (c,(nonceCard,atc,ccNo));
	  in (c,=GENERATEAC);
	  let macSessionKey = genSkey(atc,bankMacKey) in
	  let transCryptoGram = mac((amountToPay,nonceReader,atc),macSessionKey) in
	  let sdad = sign((nonceReader,nonceCard,amountToPay,atc,transCryptoGram), cardKey) in
	  out (c, (sdad,transCryptoGram) );
	  in (c,=READRECORD);
	  out (c,cert).

let Card2 = 
	  in (c, (=SELECT,=PAYSYSDDF));
	  out (c, AID);				
	  in (c,(=SELECT,=AID));
	  new nonceCard;	
	  out (c,PDOL);
	  in (c,(=GPO,amountToPay,nonceReader));
	  out (c,(nonceCard,atc,ccNo));
	  in (c,=GENERATEAC);
	  let macSessionKey = genSkey(atc,bankMacKey) in
	  let transCryptoGram = mac((amountToPay,nonceReader,atc),macSessionKey) in
	  let sdad = sign((nonceReader,nonceCard,amountToPay,atc,transCryptoGram), cardKey) in
	  out (c, (sdad,transCryptoGram) );
	  phase 2;
	  in (c,=READRECORD);
	  out (c,cert).

let Card3 = 
	  in (c, (=SELECT,=PAYSYSDDF));
	  out (c, AID);				
	  in (c,(=SELECT,=AID));
	  new nonceCard;	
	  out (c,PDOL);
	  in (c,(=GPO,amountToPay,nonceReader));
	  out (c,(nonceCard,atc,ccNo));
	  phase 2;
	  in (c,=GENERATEAC);
	  let macSessionKey = genSkey(atc,bankMacKey) in
	  let transCryptoGram = mac((amountToPay,nonceReader,atc),macSessionKey) in
	  let sdad = sign((nonceReader,nonceCard,amountToPay,atc,transCryptoGram), cardKey) in
	  out (c, (sdad,transCryptoGram) );
	  in (c,=READRECORD);
	  out (c,cert).

let Card4 = 
	  in (c, (=SELECT,=PAYSYSDDF));
	  out (c, AID);				
	  in (c,(=SELECT,=AID));
	  new nonceCard;	
	  out (c,PDOL);
	  phase 2;
	  in (c,(=GPO,amountToPay,nonceReader));
	  out (c,(nonceCard,atc,ccNo));
	  in (c,=GENERATEAC);
	  let macSessionKey = genSkey(atc,bankMacKey) in
	  let transCryptoGram = mac((amountToPay,nonceReader,atc),macSessionKey) in
	  let sdad = sign((nonceReader,nonceCard,amountToPay,atc,transCryptoGram), cardKey) in
	  out (c, (sdad,transCryptoGram) );
	  in (c,=READRECORD);
	  out (c,cert).

let Card5 = 
	  in (c, (=SELECT,=PAYSYSDDF));
	  out (c, AID);				
	  phase 2;
	  in (c,(=SELECT,=AID));
	  new nonceCard;	
	  out (c,PDOL);
	  in (c,(=GPO,amountToPay,nonceReader));
	  out (c,(nonceCard,atc,ccNo));
	  in (c,=GENERATEAC);
	  let macSessionKey = genSkey(atc,bankMacKey) in
	  let transCryptoGram = mac((amountToPay,nonceReader,atc),macSessionKey) in
	  let sdad = sign((nonceReader,nonceCard,amountToPay,atc,transCryptoGram), cardKey) in
	  out (c, (sdad,transCryptoGram) );
	  in (c,=READRECORD);
	  out (c,cert).


let Card6 = 
	  phase 2;
	  in (c, (=SELECT,=PAYSYSDDF));
	  out (c, AID);				
	  in (c,(=SELECT,=AID));
	  new nonceCard;	
	  out (c,PDOL);
	  in (c,(=GPO,amountToPay,nonceReader));
	  out (c,(nonceCard,atc,ccNo));
	  in (c,=GENERATEAC);
	  let macSessionKey = genSkey(atc,bankMacKey) in
	  let transCryptoGram = mac((amountToPay,nonceReader,atc),macSessionKey) in
	  let sdad = sign((nonceReader,nonceCard,amountToPay,atc,transCryptoGram), cardKey) in
	  out (c, (sdad,transCryptoGram) );
	  in (c,=READRECORD);
	  out (c,cert).


let Reader =     
	  out (c, (SELECT,PAYSYSDDF));
	  in (c, appId);
	  out (c, (SELECT,appId));				
	  in (c,dataRequested);	
	  new nonceR;
	  phase 1;
	  out (c,(GPO,amount,nonceR));
	  in (c, (nonceC,counter,pan) );
	  phase 2;
	  out (c, GENERATEAC);
	  in (c, (sig,cryptogram) );
	  out (c,READRECORD);
	  in (c,cardCert);
	  let cardKey = checksign(cardCert,pk(bankSignKey)) in			
	  if checksign(sig,cardKey) = (nonceR,nonceC,amount,counter,cryptogram) then			
   	  out(bankChannel,(cryptogram,amount,ccNo));    
	  out (c,readerFinish).	 

let Reader1 =     
	  out (c, (SELECT,PAYSYSDDF));
	  in (c, appId);
	  out (c, (SELECT,appId));				
	  in (c,dataRequested);	
	  new nonceR;
	  out (c,(GPO,amount,nonceR));
	  in (c, (nonceC,counter,pan) );
	  out (c, GENERATEAC);
	  in (c, (sig,cryptogram) );
	  out (c,READRECORD);
	  in (c,cardCert);
	  let cardKey = checksign(cardCert,pk(bankSignKey)) in			
	  if checksign(sig,cardKey) = (nonceR,nonceC,amount,counter,cryptogram) then			
   	  out(bankChannel,(cryptogram,amount,ccNo)).	 

let Reader2 =     
	  out (c, (SELECT,PAYSYSDDF));
	  in (c, appId);
	  out (c, (SELECT,appId));				
	  in (c,dataRequested);	
	  new nonceR;
	  out (c,(GPO,amount,nonceR));
	  in (c, (nonceC,counter,pan) );
	  out (c, GENERATEAC);
	  in (c, (sig,cryptogram) );
	  out (c,READRECORD);
	  phase 2;
	  in (c,cardCert);
	  let cardKey = checksign(cardCert,pk(bankSignKey)) in			
	  if checksign(sig,cardKey) = (nonceR,nonceC,amount,counter,cryptogram) then			
   	  out(bankChannel,(cryptogram,amount,ccNo)).	 


let Reader3 =     
	  out (c, (SELECT,PAYSYSDDF));
	  in (c, appId);
	  out (c, (SELECT,appId));				
	  in (c,dataRequested);	
	  new nonceR;
	  out (c,(GPO,amount,nonceR));
	  in (c, (nonceC,counter,pan) );
	  out (c, GENERATEAC);
	  phase 2;
	  in (c, (sig,cryptogram) );
	  out (c,READRECORD);
	  in (c,cardCert);
	  let cardKey = checksign(cardCert,pk(bankSignKey)) in			
	  if checksign(sig,cardKey) = (nonceR,nonceC,amount,counter,cryptogram) then			
   	  out(bankChannel,(cryptogram,amount,ccNo)).	 
  
let Reader4 =     
	  out (c, (SELECT,PAYSYSDDF));
	  in (c, appId);
	  out (c, (SELECT,appId));				
	  in (c,dataRequested);	
	  new nonceR;
	  out (c,(GPO,amount,nonceR));
	  phase 2;
	  in (c, (nonceC,counter,pan) );
	  out (c, GENERATEAC);
	  in (c, (sig,cryptogram) );
	  out (c,READRECORD);
	  in (c,cardCert);
	  let cardKey = checksign(cardCert,pk(bankSignKey)) in			
	  if checksign(sig,cardKey) = (nonceR,nonceC,amount,counter,cryptogram) then			
   	  out(bankChannel,(cryptogram,amount,ccNo)).	 

let Reader5 =     
	  out (c, (SELECT,PAYSYSDDF));
	  in (c, appId);
	  out (c, (SELECT,appId));
	  phase 2;				
	  in (c,dataRequested);	
	  new nonceR;
	  out (c,(GPO,amount,nonceR));
	  in (c, (nonceC,counter,pan) );
	  out (c, GENERATEAC);
	  in (c, (sig,cryptogram) );
	  out (c,READRECORD);
	  in (c,cardCert);
	  let cardKey = checksign(cardCert,pk(bankSignKey)) in			
	  if checksign(sig,cardKey) = (nonceR,nonceC,amount,counter,cryptogram) then			
   	  out(bankChannel,(cryptogram,amount,ccNo)).	

let Reader6 =     
	  out (c, (SELECT,PAYSYSDDF));
	  phase 2;				
	  in (c, appId);
	  out (c, (SELECT,appId));
	  in (c,dataRequested);	
	  new nonceR;
	  out (c,(GPO,amount,nonceR));
	  in (c, (nonceC,counter,pan) );
	  out (c, GENERATEAC);
	  in (c, (sig,cryptogram) );
	  out (c,READRECORD);
	  in (c,cardCert);
	  let cardKey = checksign(cardCert,pk(bankSignKey)) in			
	  if checksign(sig,cardKey) = (nonceR,nonceC,amount,counter,cryptogram) then			
   	  out(bankChannel,(cryptogram,amount,ccNo)).	



process ( !new amount;( !Reader | !Reader1 | !Reader2 | !Reader3 | !Reader4 | !Reader5 | !Reader6 )  
	  | !(new ccNo;new cardKey; let cert = sign(pk(cardKey),bankSignKey) in 
	    	  !new atc;( !Card1 | !Card2 | !Card3 | !Card4 | !Card5 | !Card6) ) 
	  | out (c, pk(bankSignKey)) )