(* A model of Visa's payWave qVSDC protocol  *)

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.

(* Does the reader have the right cryptogram AC? *)
query evinj:readerAccept(cGram) ==> evinj:cardGen(cGram).
(* This check fail, indicating that Visa cards can be tricked into accepting an incorrect cryptogram *)

let Card = 
	  in (c, (=SELECT,=PAYSYSDDF));
	  out (c, AID);				
	  in (c,(=SELECT,=AID));	
	  out (c,PDOL);
	  in (c,(=GPO,amountToPay,nonceReader));
          new nonceCard;
	  let macSessionKey = genSkey(atc,bankMacKey) in
	  let transCryptoGram = mac((amountToPay,nonceReader,atc),macSessionKey) in
	  event cardGen(transCryptoGram);
	  let sdad = sign((nonceReader,nonceCard,amountToPay,atc), cardKey) in
	  out (c, (sdad,transCryptoGram,atc) );
	  in (c,=READRECORD);
	  out (c,(cert,ccNo,nonceCard)).
           
let Reader =     
	  out (c, (SELECT,PAYSYSDDF));
	  in (c, appId);
	  out (c, (SELECT,appId));				
	  in (c,dataRequested);	
	  new nonceR;
	  out (c,(GPO,amount,nonceR));
	  in (c, (sig,cryptogram,counter) );
	  out (c,READRECORD);
	  in (c,(cardCert,pan,nonceC));
	  let cardKeyR = checksign(cardCert,pk(bankSignKey)) in			
	  if checksign(sig,cardKeyR) = (nonceR,nonceC,amount,counter) then					
   	  out(bankChannel,(cryptogram,amount,pan));    
	  event readerAccept(cryptogram).	  

process ( !new amount;!Reader 
	  | !(new ccNo;new cardKey; let cert = sign(pk(cardKey),bankSignKey) in !new atc;Card) 
	  | out (c, pk(bankSignKey)) )