(* -------------------------------- *)
(*           PAYSAFE CCR++          *)
(* tpmID, t1 and t2 are added in AC *)
(* -------------------------------- *)


(* --- Constants / Channels --- *)
free cP:channel.
free GEN_AC:bitstring.
free READ_RECORD:bitstring.
const OK:bitstring.
const data:bitstring.

(* These two constants model the identities of an honest TPM and an honest
card on which the security property will be encoded *)
free TPMO:bitstring.
free CARDO:bitstring.

(* These two constants are used to distinguish TPM and Card certificates *)
const TPMCert:bitstring.
const CardCert:bitstring.

(* -- Functions --- *)
fun timebound(bitstring):bitstring.
fun shk(bitstring,bitstring):bitstring [private].    

(* Symetric encryption *)
fun sEnc(bitstring,bitstring):bitstring.
fun sDec(bitstring,bitstring):bitstring
reduc forall m:bitstring, k:bitstring; sDec(sEnc(m,k),k) = m.
    
(* Signature *)
fun pubKey(bitstring):bitstring.
fun secKey(bitstring):bitstring [private].
fun sign(bitstring,bitstring):bitstring.
fun verify(bitstring,bitstring):bitstring
reduc forall m:bitstring, k:bitstring; verify(sign(m,k),pubKey(k)) = m.

(* Mac *)
fun mac(bitstring,bitstring):bitstring.

(* --- Events --- *)

(* The cardEvent (resp. tpmEvent) is executed when generating an identity 
of a card (resp. TPM) *)
event cardEvent(bitstring).
event tpmEvent(bitstring).

(* This event is used to compare the timebound received by the bank
and the identity of the card that is involved in the transaction 
It contains: 
- the identity of the card
- the time-bound received by the bank
*)
event receivedBound(bitstring,bitstring).

(* The timestamp event takes 3 arguments. The two first appear in the 
theoretical event while the last one is added to make ProVerif prove
- name of the agent executing it
- current time
- additional data: the received value encapsulated in the signature
*)
event timeStamp(bitstring,bitstring,bitstring).

(* The proverAction event is used to highlight specific actions performed
by the prover. It takes two arguments: 
- the identity of the prover
- additional data: the signature sigma1 already received 
*)
event proverAction(bitstring,bitstring).

(* The checkTimes event models that a timing constraint has been verified.
It takes 5 arguments: the 3 first appear in the theoretical event while
the 2 last are added to make ProVerif prove.
- the time t1
- the time t2
- the timebound delta involved in the timing constraint which is t2-t1<delta
- additional data: a session identifier nC, i.e. the nonce generated by 
the card during the transaction
- additional data: the identity of the card involved in the transaction
*)
event checkTimes(bitstring,bitstring,bitstring,bitstring,bitstring).

(* The claim event models that the bank has accepted a transaction.
It takes 4 arguments.
- the identity of the TPM involved in the transaction
- the identity of the CARD involved in the transaction
- the first time of the rapid phase
- the second time of the rapid phase
*)
event claim(bitstring,bitstring,bitstring,bitstring).

(* --- Processes --- *)

let TPM(tpmID:bitstring, time:bitstring) = 
    in(cP, nR:bitstring);
    let sigma1 = sign((time, nR), secKey(tpmID)) in
    event timeStamp(tpmID,time, nR);
    out(cP,(time, sigma1));
    0.

let Card(bankID:bitstring, cardID:bitstring) =

    (* the card gets its certificate *)
    in(cP, cardCert:bitstring);
    if verify(cardCert, pubKey(secKey(bankID))) = (CardCert, cardID, pubKey(secKey(cardID))) then  

    (* the card gets the timebound delta *)
    let timeboundinfo = timebound(cardID) in

    (* Reader -> Card: sigma1 *)
    in(cP, sigma1:bitstring);
    new nC:bitstring;
    event proverAction(cardID, sigma1);
    (* Card -> Reader: Nc *)
    out(cP, nC);

    (* Reader -> Card : READ_RECORD *)
    in(cP, (t2:bitstring, sigma2:bitstring, t1:bitstring, nR:bitstring, certTPM:bitstring));
    (* Card -> Reader: Certs *)
    out(cP, cardCert);

    (* Reader -> Card: GEN_AC *)
    in(cP, =GEN_AC);
    
    (* check TPM certificate *)
    let (=TPMCert, tpmID:bitstring, tpmPub:bitstring) = verify(certTPM, pubKey(secKey(bankID))) in 
    
    (* check signatures *)
    if (t1, nR) = verify(sigma1, tpmPub) then
    if (t2, nC) = verify(sigma2, tpmPub) then
    
    (* Check t2 − t1 ≤ td *)
    event checkTimes(t1,t2,timeboundinfo,nC,cardID);
    
    new ATC:bitstring;
    let Ks = sEnc(ATC, shk(cardID, bankID)) in
    let AC = mac((ATC, data, sigma1, tpmID, t1, t2), Ks) in
    let SDAD = sign((AC, nR, timeboundinfo, nC), secKey(cardID)) in
    (* Card -> Reader: SDAD, AC *)
    out(cP, (SDAD, AC, ATC, cardID));
    0.

let Bank(bankID:bitstring) =
    (* Reader -> Card: AC, ATC, t1, t2, sigma1, nC, SDAD, td, nR *)
    in (cP, (AC:bitstring, ATC:bitstring, cardID:bitstring, sigma1:bitstring, nC:bitstring, nR:bitstring, 
                SDAD:bitstring, timeboundinfo:bitstring, 
                t1:bitstring, t2:bitstring,tpmID:bitstring ));
    (*in (cP, (AC:bitstring, ATC:bitstring, cardID:bitstring, sigma1:bitstring, nC:bitstring, 
            tpmID:bitstring, t1:bitstring, t2:bitstring));*)
    (* Verify SDAD *)
    if (AC, nR, timeboundinfo, nC) = verify(SDAD, pubKey(secKey(cardID))) then 
    (* Construct session key *)
    let Ks = sEnc(ATC, shk(cardID, bankID))   in
    (* Check AC *)
    if AC = mac((ATC, data, sigma1, tpmID, t1, t2), Ks) then         
    (* Accept the transaction *)
    event claim(tpmID, cardID, t1, t2);
    (* Make visible the received timebound used during the transaction *)
    event receivedBound(cardID, timeboundinfo);
    0.

(* --- Security Properties --- *)
(* Sanity Check: the protocol can terminate *)
query t1:bitstring,t2:bitstring;
    event(claim(TPMO, CARDO, t1, t2)). 

(* The bank only accepts transaction between a legitimate TPM and a legitimate Card *)
(* This property is not satisfied by this protocol *)
(* It is acheived when limiting cardID to CARDO *)
query tpmID:bitstring, cardID:bitstring, t1:bitstring, t2:bitstring;
    event(claim(tpmID, cardID, t1, t2))
        ==> ( event(tpmEvent(tpmID)) && event(cardEvent(cardID)) ).

(* Authentication of the timebound: the time-bound received by the bank
must always correspond to the one of the card that is involved in the 
transaction (if the card is honest) *)
query timeboundinfo:bitstring;
    event(receivedBound(CARDO, timeboundinfo)) 
        ==> timeboundinfo = timebound(CARDO).

(* Change: the claim only contains the transaction identifier, nC *)
query bankID:bitstring, t1:bitstring, nR:bitstring, t2:bitstring, nC:bitstring, timeboundinfo:bitstring;
    event(claim(TPMO, CARDO, t1, t2))
       ==> (event(checkTimes(t1, t2, timeboundinfo, nC, CARDO))
           ==> (event(timeStamp(TPMO,t2, nC))
	       ==> (event(proverAction(CARDO,sign((t1,nR), secKey(TPMO))))
	           ==> (event(timeStamp(TPMO,t1, nR)))))
               ).

(* --- Global Process --- *)
process
    !(new bankID:bitstring; out(cP, bankID); out(cP, pubKey(secKey(bankID))); ( !Bank(bankID) 
       (* Processes for the two checked identities *) 
       | (
          let cardCert = sign((CardCert, CARDO, pubKey(secKey(CARDO))),secKey(bankID)) in 
          event cardEvent(CARDO); 
          out(cP, cardCert); !Card(bankID, CARDO)
          )
       | (
          let tpmCert = sign((TPMCert, TPMO, pubKey(secKey(TPMO))),secKey(bankID)) in 
          event tpmEvent(TPMO);
          out (cP, tpmCert); !(new time:bitstring; out(cP, time); TPM(TPMO, time)) 
          )
       
       (* Processes for honest participants *)
       | (
           !new cardID:bitstring; let cardCert = sign((CardCert, cardID, pubKey(secKey(cardID))),secKey(bankID)) in
           event cardEvent(cardID);
           out(cP, cardID); out (cP, cardCert); !Card(bankID, cardID)
           )
       | (
           !new tpmID:bitstring; let tpmCert = sign((TPMCert, tpmID, pubKey(secKey(tpmID))),secKey(bankID)) in
           event tpmEvent(tpmID);
           out(cP, tpmID); out (cP, tpmCert); !(new time:bitstring; out(cP, time); TPM(tpmID, time)) 
          )
       
       (* Processes for dishonest participants *)
       (* I simply assume that all the "bank" processes are executed by honest participants *)
       (* Dishonest cards*)
       | (
           !new cardID:bitstring; let cardCert = sign((CardCert, cardID, pubKey(secKey(cardID))),secKey(bankID)) in
           event cardEvent(cardID);
           out(cP, cardID);
           out(cP, secKey(cardID));
           out(cP, cardCert);
           out(cP, shk(cardID, bankID))
          )
       (* Dishonest TPMs *)
       | (
          !new tpmID:bitstring; let tpmCert = sign((TPMCert, tpmID, pubKey(secKey(tpmID))),secKey(bankID)) in
           event tpmEvent(tpmID);
           out(cP, tpmID);
           out(cP, secKey(tpmID));
           out(cP, tpmCert)
          )
       )
     )