daa_pnc_charge_authorisation_online.spthy

theory DDA_PnC_Charge_Authorisation_online
begin
 
/*
Protocol:	DAA_PnC
Properties:	SR3 - Secure Charge Authorisation (online)
		SR4 - Charge Data Authenticity (online)

This Tamarin model is used to verify the security of the charge authorization
process for the Direct Anonymous Authentication (DAA) based privacy extentsion
of the Plug and Charge (PnC) authentication system. The extension is described
in the paper "Integrating Privacy into the Electric Vehicle Charging Architecture".

The model consists of the following actors:
Host/EV 	- Electric Vehicle
TPM			- Trusted Platform Module used to secure the EVs private keys
Issuer		- The e-mobility service provider (eMSP), corresponding to the Issuer role in the DAA protocol
CP			- Charge Point

This model verifies the security requirement SR2: Secure Credential Installation

It is based on the model from the paper "Formal Analysis and Implementation of a TPM 2.0-based Direct Anonymous Attestation Scheme" accepted to ASIACCS 2020 by
Original Authors:
	Liqun Chen, Surrey Centre for Cyber Security, University of Surrey
	Christoper J.P. Newton, Surrey Centre for Cyber Security, University of Surrey
	Ralf Sasse, Department of Computer Science, ETH Zurich
	Helen Treharne, Surrey Centre for Cyber Security, University of Surrey
	Stephan Wesemeyer, Surrey Centre for Cyber Security, University of Surrey
	Jorden Whitefield, Ericsson AB, Finland
cf. https://github.com/tamarin-prover/tamarin-prover/tree/dddaccbe981343dde1a321ce0c908585d4525918/examples/asiaccs20-eccDAA


time tamarin-prover daa_pnc_charge_authorisation_online.spthy\
 --heuristic=I --prove --quit-on-warning +RTS -N8 -RTS

==============================================================================
summary of summaries:

analyzed: daa_pnc_charge_authorisation_online.spthy

  source_of_key_reveal_sk (all-traces): verified (9 steps)
  restriction_bind (all-traces): verified (4 steps)
  restriction_one_host_per_tpm (all-traces): verified (12 steps)
  restriction_one_tpm_per_host (all-traces): verified (10 steps)
  restriction_pke_comes_from_tpm (all-traces): verified (8 steps)
  correctness_verify_multiple_pkes (exists-trace): verified (30 steps)
  correctness_verify_multiple_pkes_diff_I (exists-trace): verified (27 steps)
  correctness_two_certs_same_credentials (exists-trace): verified (41 steps)
  correctness_two_certs_different_credentials (exists-trace): verified (42 steps)
  correctness_two_auths_same_ev_same_key (exists-trace): verified (110 steps)
  correctness_two_auths_diff_ev_diff_key (exists-trace): verified (97 steps)
  correctness_two_auths_same_ev_diff_key (exists-trace): verified (155 steps)
  correctness_two_data (exists-trace): verified (47 steps)
  correctness_credential_req (exists-trace): verified (29 steps)
  correctness_charge_authorisation_req_1 (exists-trace): verified (42 steps)
  correctness_charge_authorisation_req_2 (exists-trace): verified (57 steps)
  correctness_charge_authorisation (exists-trace): verified (77 steps)
  correctness_charge_data_authentication (exists-trace): verified (91 steps)
  correctness_with_adv (exists-trace): verified (67 steps)
  auth_aliveness_issuer_very_weak (all-traces): verified (3 steps)
  auth_aliveness_issuer (all-traces): verified (3 steps)
  auth_aliveness_host (all-traces): verified (5 steps)
  auth_weak_agreement_host (all-traces): verified (11 steps)
  auth_non_injective_agreement_host_issuer (all-traces): verified (11 steps)
  auth_injective_agreement_host_issuer (all-traces): verified (15 steps)
  auth_secrecy_cre (all-traces): verified (24 steps)
  auth_secrecy_emaid (all-traces): verified (17 steps)
  auth_aliveness_charge (all-traces): verified (35 steps)
  auth_weak_agreement_charge (all-traces): verified (112 steps)
  auth_non_injective_agreement_charge (all-traces): verified (112 steps)
  auth_injective_agreement_charge (all-traces): verified (118 steps)
  auth_aliveness_charge_data (all-traces): verified (110 steps)
  auth_weak_agreement_charge_data (all-traces): verified (110 steps)
  auth_non_injective_agreement_charge_data (all-traces): verified (146 steps)
  auth_injective_agreement_charge_data (all-traces): verified (154 steps)
  SP3_Unforgeability (all-traces): verified (36 steps)

==============================================================================

real	18m55,553s
user	90m15,520s
sys	27m49,332s

*/

builtins:   symmetric-encryption, signing, diffie-hellman, hashing

functions:  accept/0, MAC/2, KDF_AES/1, KDF_EK/1,KDF_a/3, KDF_e/4, QName/2, certData/2, DAAKeyID/1,
             multp/2, plus/2, minus/2, len16/1, 
             H_SHA256/1,  H_k_1/1, H_k_2/2, H_k_4/4, H_k_7/7, H_n_2/2, H_n_2/2, H_n_8/8, H_6/1,
			 curlyK/1, E/2, E_S/2, L_J/2, RB/2, RD/2, 
			 calcE/1, 
			 calcE_S_cert/4, calcL_J_cert/4, 
			 calcRB/1, calcRD/1, Nonce/1,
			 PkX/2, PkY/2, verifyCre1/4, verifyCre2/5,verifyCre3/4,verifyCre4/5,
			 BSN/1, F1/1, F2/1, H_p/1,PointG1/2, Message/1, Q_K/1, certify/1, publicData/1
			 

equations:  
			calcE( 
				minus(
					multp(
							plus(
								r_cv,
								multp(
										H_n_2(n_J, H_k_1(H_k_4(P1,Q,E(r_cv,P1),str))),
										f
									)
								),
							P1
						),
					multp(
							H_n_2(n_J, H_k_1(H_k_4(P1, Q, E(r_cv,P1), str))),
							multp(
									f,
									P1
								)
						)
					)
				) = E(r_cv,P1)
				,

			calcRB(
				minus(
					multp(
						plus(l,multp(multp(y,r),H_n_8(P1, multp(f,P1), RB(l,P1), RD(l,multp(f,P1)), 
						 multp(r,P1), 
						 multp(y,multp(r,P1)), 
						 plus(multp(x,multp(r,P1)),multp(multp(multp(r,x),y),Q)), 
						 multp(multp(r,y),Q)
						 ))),
						P1),
					multp(
						H_n_8(P1, multp(f,P1), RB(l,P1), RD(l,multp(f,P1)), 
						 multp(r,P1), 
						 multp(y,multp(r,P1)), 
						 plus(multp(x,multp(r,P1)),multp(multp(multp(r,x),y),Q)), 
						 multp(multp(r,y),Q)
						),
					    multp(y,multp(r,P1))
						)						
					)
				)= RB(l,P1)
			,

			calcRD(
				minus(
					multp(plus(l,multp(multp(y,r),H_n_8(P1, multp(f, P1), RB(l,P1), RD(l,multp(f,P1)),
						 multp(r,P1), 
						 multp(y,multp(r,P1)), 
						 plus(multp(x,multp(r,P1)),multp(multp(multp(r,x),y),Q)), 
						 multp(multp(r,y),Q)
					))),multp(f, P1)),
					multp(H_n_8(P1, multp(f, P1), RB(l,P1), RD(l,multp(f,P1)), 
						 multp(r,P1), 
						 multp(y,multp(r,P1)), 
						 plus(multp(x,multp(r,P1)),multp(multp(multp(r,x),y),Q)), 
						 multp(multp(r,y),Q)
					), multp(multp(r,y),multp(f, P1)))
					)
					
				)=RD(l,multp(f,P1))
				
			
			,
			//calcL_J(s, J, h2, K)	=sJ-h2K
			//						=(r_cv1+h2f)J-h2(fJ)
			//						=r_cv1 J
			calcL_J_cert(
					plus(r_cv1,multp(h2,f)), //s
				PointG1(H_p(F1(bsn)),F2(bsn)),	//J
					H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,pkCCsess_n)))), //h2
					multp(f,J) //K
				)
				=
				L_J(r_cv1, PointG1(H_p(F1(bsn)),F2(bsn)))
			,

			//calcE_S_cert(small_s, S, h2, W)	=sS-h2W
			//									=(r_cv1+h2f)lyrP1-h2(lryfP1)
			//									=r_cv1lyrP1
			
			calcE_S_cert(plus(r_cv1,multp(H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,pkCCsess_n)))),f)), //small_s
					multp(l,multp(y,multp(r,P1))),					//S
					H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,pkCCsess_n)))), //h2
					multp(l,multp(multp(r,y),multp(f, P1))) //W
					)
				=
				E_S(r_cv1, multp(l,multp(y,multp(r,P1))))	//E_S(r_cv1,S)				
				
			,
			verifyCre1(
				multp(r,P1), //A
				PkY(y,P2),  //Y
				multp(y,multp(r,P1)),//B
				P2)=accept
			,
								
			verifyCre2(
				multp(r,P1), 			//A
				multp(multp(~r,y),multp(f,P1)), 	//D
				PkX(x,P2),				//X
				plus(multp(x,multp(r,P1)),multp(multp(multp(r,x),y),multp(f,P1))),//C
				P2)=accept
				,
			
			verifyCre3(
				multp(l,multp(r,P1)),	//R=lA=l(rP1)
				PkY(y,P2),				//Y
				multp(l,multp(y,multp(r,P1))),	//S=lB=l(y(A))
				P2)=accept
			,	
			verifyCre4(
				multp(l,multp(r,P1)),	//R=lA=l(rP1)
				multp(l,multp(multp(r,y),multp(f,P1))),	//W=l(D)=l(ryQ)=l(ry(fP1))
				PkX(x,P2),				//X
				multp(l,plus(multp(x,multp(r,P1)),multp(multp(multp(r,x),y),multp(f,P1)))), //T=lC=l(xA+rxyQ)=l(xrP1+rxyfP1)
				P2)=accept
			
//=========================================
// Protocol Restrictions (Axioms)
//=========================================

restriction equality: 	     "All #i x y . Eq( x, y ) @ i ==> x = y"

// each authorisation nonce i_x is only accepted once
restriction only_once_ix: "All L R i_x #i #j . (OnlyOnce_i_x(L, R, i_x) @ i & OnlyOnce_i_x(L, R, i_x)@ j) ==> (#i=#j)"

//Modification: removed restriction for single issuer initialisation
//each issuer should only be initialised once
restriction issuer_single_init:
	"All I #i #j . (Issuer_Init(I) @ i & Issuer_Init(I) @ j) ==> (#i=#j)"

//each charge point should only be initialised once
restriction cp_single_init:
	"All CP #i #j . (CP_Init(CP) @ i & CP_Init(CP) @ j) ==> (#i=#j)"

//a host should only initialise itself once
restriction host_single_init:
	"All Host #i #j . ((Host_Init(Host)@i & Host_Init(Host)@j) ==> (#i=#j))"

//a TPM should only be initialised once (and hence there is only one aes key and one TPM_EK_SEED):
restriction tpm_single_init:
	"All PS #i #j. ((TPM_Init(PS)@i & TPM_Init(PS)@j) ==> (#i=#j))"


//a host and a TPM cannot be initialised with the same identity
//Modification: adjusted restrictions for ID uniqueness to new entity definitions
restriction no_shared_id_between_tpm_host:
	"All Ent1 Ent2 #i #j . 
	(Host_Init(Ent1) @ i & TPM_Init(Ent2) @ j) 
	==> 
	(not(Ent1=Ent2))"

//an issuer and a CP cannot be initialised with the same identity
restriction no_shared_id_between_issuer_cp:
	"All Ent1 Ent2 #i #j . 
	(Issuer_Init(Ent1) @ i & CP_Init(Ent2) @ j) 
	==> 
	(not(Ent1=Ent2))"

//When initialized, a host, tpm and issuer must have different identities
restriction no_shared_id_between_tpm_host_issuer:
	"All Ent1 Ent2 Ent3 #i #j #k. 
	(Host_Init(Ent1) @ i & TPM_Init(Ent2) @ j & Issuer_Init(Ent3) @ k ) 
	==> 
	(not(Ent1=Ent2) & not (Ent1=Ent3)
	& not (Ent2=Ent3) )"
	
//When initialized, a host, tpm and issuer, and CP must have different identities
restriction no_shared_id_between_tpm_host_issuer_cp:
	"All Ent1 Ent2 Ent3 Ent4 #i #j #k #l. 
	(Host_Init(Ent1) @ i & TPM_Init(Ent2) @ j & Issuer_Init(Ent3) @ k & CP_Init(Ent4) @ l) 
	==> 
	(not(Ent1=Ent2) & not (Ent1=Ent3) & not (Ent1=Ent4)
	& not (Ent2=Ent3) & not (Ent2=Ent4)
	& not (Ent3=Ent4))"


//=========================================
// Secure Channel Rules
//=========================================
/* 
We need a secure channel between the TPM aka the Principal Signer (PS) 
and its host aka the Assistant Signer (AS). We refer to the combination 
of a PS and AS as a Platform.
*/

/*
   Communication between the Host or Assistant Signer (AS) and the TPM 
   or Principal Signer (PS) is done over a 'Secure Channel'. This means 
   that an adversary can neither modify nor learn messages that are 
   sent over the channel. Sec( A, B, x ) is a linear fact modelling 
   that the adversary cannot replay on this channel. Secure channels 
   have the property of being both confidential and authentic. 
   Communication between the AS and PS is constrained by the channel 
   invariant !F_Paired, such that two arbitrary roles cannot communicate 
   over this channel.
*/
rule ChanOut_S [colour=ffffff]:
    [ Out_S( $A, $B, x ), !F_Paired( $A, $B ) ]
  --[ ChanOut_S( $A, $B, x ) ]->
    [ Sec( $A, $B, x ) ]

rule ChanIn_S [colour=ffffff]:
    [ Sec( $A, $B, x ) ]
  --[ ChanIn_S( $A, $B, x ) ]->
    [ In_S( $A, $B, x ) ]


/* Modification: Added Secure Channel rules for backend communication
	Secure TLS Channel between backend actors.
	Channel is confidential and authentic.
*/
rule ChanOut_S_Backend:
        [ Out_S_B($A,$B,x) ]
      --[ ChanOut_S_B($A,$B,x) ]->
        [ SecB($A,$B,x) ]

rule ChanIn_S_Backend:
        [ SecB($A,$B,x) ]
      --[ ChanIn_S_B($A,$B,x) ]->
        [ In_S_B($A,$B,x) ]


//=========================================
// Protocol Setup and Actor Initialisation
//=========================================
/*
Issuer set-up:
Modification: Allow multiple issuer (eMSP) set-ups
*/
rule Issuer_Init:
		let 
			pkX=PkX(~x,'P2')
			pkY=PkY(~y,'P2')
		in
		[Fr(~x),
		 Fr(~y)]
		--[Issuer_Init($I)
			, Issuer_Init2($I, ~x, ~y)
			, OnlyOnce('Issuer_Init')]->
		[ !Ltk($I,~x, ~y)
			, !Pk($I, pkX,pkY)
			, Out(<pkX,pkY>)
			, !Issuer_Initialised($I)
		]


// simple key reveal rule for the issuer's secret key pair
rule Issuer_KeyReveal:
	[!Ltk($I, ~x, ~y)]
	--[KeyReveal('Issuer_KeyReveal', $I)]->
	[Out(<~x,~y>)]


// Modification: Added CP set-up
rule CP_Init:
		[]
		--[CP_Init($CP)
		   , OnlyOnce('CP_Init')]->
		[ !CP_Initialised($CP) ]


/*
Platform set-up:
For a platform we need a TPM (the principal signer) and a Host (the assistant signer)
before binding them together in a platform.

Modification: Removed need for the host to know the issuer before the join.
*/
rule TPM_INIT:
	let
	//!Assumption that the aes key is derived by a KDF_AES key derivation function
	aes_key=KDF_AES(~TPM_AES_Seed)

	e=KDF_EK(~TPM_EK_Seed)
	pke='g'^e //for key reveal conditions
	in
		[Fr(~TPM_AES_Seed),
		 Fr(~TPM_EK_Seed)]
		--[TPM_Init($PS)
		   , OnlyOnce('TPM_INIT')]->
		[!TPM_AES_Key($PS, aes_key), 
		 TPM_AES_Key2($PS, aes_key, pke),
		 TPM_EK_SEED($PS,~TPM_EK_Seed), 
		 TPM_Initialised($PS)]

//simple rule to allow the TPM's aes key to leak		
rule TPM_AESReveal:
	[TPM_AES_Key2(PS, aes_key, pke)]
	--[KeyReveal('TPM_AESReveal', PS)
	, KeyReveal('PKE_AESReveal', pke)]->
	[Out(aes_key)]

rule Host_Init:
	[]
	--[Host_Init($AS)
	  , OnlyOnce('Host_Init')]->
	[Host_Initialised($AS)]

//This rule binds an $PS and an $AS to one another.
rule Platform_Setup:
	[ TPM_Initialised($PS)
	, Host_Initialised($AS)
	]
	 //Action label used to ensure there is a one-to-one correspondence between AS and PS
	 --[ Bind($PS,$AS)
		,OnlyOnce('Platform_Setup')
	   ]->
	 [ Out_S($AS, $PS, < 'createPrimary'>)
		, !F_Paired($AS,$PS)
		, !F_Paired($PS,$AS)
	 ]
        	 
//The TPM executes this in response to a request by the host
//Note this should only be executed by a TPM once!
rule TPM2_CreatePrimary:
	let
	e=KDF_EK(~TPM_EK_Seed)
	pke='g'^e
	E_PD=<'EK_public_data',pke>
    in
	[ In_S($AS, $PS, < 'createPrimary'>)
	, TPM_EK_SEED($PS,~TPM_EK_Seed)]
	--[ TPM2_EK_Created($PS, $AS, pke)
		, TPM2_EK_Created2(e, pke)
		, OnlyOnce('TPM2_CreatePrimary')
	  ]->
	[Out_S($PS,$AS, < E_PD, 'returnEK'>), 
	!TPM_ENDORSEMENT_SK($PS, e, pke), 
	!TPM_ENDORSEMENT_PK($PS,E_PD),
	Out(pke)]

//simple rule to reveal the TPM's endorsement key
rule TPM_EKReveal:
	let
	e=KDF_EK(~TPM_EK_Seed)
    in
	[!TPM_ENDORSEMENT_SK(PS, e, pke)]
	--[ KeyReveal('TPM_EKReveal_tpm', PS)
		, KeyReveal('TPM_EKReveal_pke', pke)
	  ]->
	[Out(e)]

//The Host should store the public endorsement key	
rule Host_Store_EK:
	let
	E_PD=<'EK_public_data', pke>
	in
	[ In_S($PS,$AS, < E_PD, 'returnEK'>) ]
	--[ Store_EK($PS, $AS)
		, OnlyOnce('Host_Store_EK')
	  ]->
	[
	 Out_S($AS,$PS, < pke, 'createPCKey'>),
	 Host_State_01( $PS, $AS, pke )]

/* 
	Modification: Added the generation of the provisioning key pair. 
	The rule is designed based on the existing TPM2_CreatePrimary and TPM2_Create rules
*/
rule TPM2_CreatePC:
	let
	PC_PD=<'PC_public_data',pk(~pc)>
	PC_SD=senc(~pc,aes_key)
    in
	[ In_S($AS, $PS, < pke, 'createPCKey'>)
	 , !TPM_AES_Key($PS, aes_key)
	 , Fr(~pc) //pc secret key
	 ]
	--[ TPM2_PC_Created($PS, $AS)
		, DerivePCKey($PS, $AS, pke, ~pc)
		, OnlyOnce('TPM2_CreatePC')
	  ]->
	[
	 Out_S($PS, $AS,< PC_SD,PC_PD, 'returnPCKey'>), 
	 !TPM_PC_SK($PS, pke, ~pc),
	 Out(pk(~pc))
	]

//simple rule to reveal the TPM's provisioning key
rule TPM_PCReveal:
	[!TPM_PC_SK(PS, pke, ~pc)]
	--[ KeyReveal('TPM_PCReveal_tpm', PS)
		, KeyReveal('TPM_PCReveal_pke', pke)
	  ]->
	[Out(~pc)]

//The Host should store the public provisioning key	
rule Host_Store_PC_pre:
	let 
	PC_PD=<'PC_public_data',pk(~pc)>
	in
	[ In_S($PS, $AS,< PC_SD,PC_PD, 'returnPCKey'>),
	  Host_State_01( $PS, $AS, pke ) ]
	--[ OnlyOnce('Host_Store_PC_pre')
	  ]->
	[ !Host_Store_PC_pre($PS, $AS, pke, PC_SD,PC_PD)
	//, !RegisterPC(PC_PD)
	] 
rule Host_Store_PC:
	let 
	PC_PD=<'PC_public_data',pk(~pc)>
	in
	[ !Host_Store_PC_pre($PS, $AS, pke, PC_SD,PC_PD) ]
	--[ Store_PC($PS, $AS)
		, OnlyOnce('Host_Store_PC')
	  ]->
	[Out_S($AS,$PS, < pke, 'createDAAKey'>), 
	 Host_State_02( $PS, $AS, pke, PC_PD, PC_SD )]


//=====================================================================	 
// Credential Installation
//=====================================================================
// Simplified Credential installation without Certificate Provisioning
// Service (CPS)

/*
This rule will create a DAA key
Note that unlike the TPM2_CreatePrimary rule, this rule can be executed 
multiple times resulting in a new DAA key
This is obviously not sensible but allowed.
*/
rule TPM2_CreateDAA:
	let 
	Q=multp(~f, 'P1')
	CCdaa_PD=<'DAA_public_data', Q>
	CCdaa_SD=senc(~f,aes_key)
	in
	[In_S($AS, $PS, < pke, 'createDAAKey'>)
	 , !TPM_AES_Key($PS, aes_key)
	 , Fr(~f) //our secret key
	 ]
	--[ TPM2_DAA_Created($PS, $AS)
		, DeriveDAAKey($PS, $AS, pke, ~f)
		, OnlyOnce('TPM2_CreateDAA')
	  ]->
	[ Out_S($PS, $AS,< CCdaa_SD,CCdaa_PD, 'returnDAAKey'>), 
	 !TPM_DAA_SK($PS, pke, ~f),
	 Out(Q)
	]
	
//simpe rule to leak the DAA key:
rule TPM_DAAReveal:
	[!TPM_DAA_SK(PS, pke, ~f)]
	--[ KeyReveal('TPM_DAAReveal_tpm', PS)
		, KeyReveal('TPM_DAAReveal_pke', pke)
		, KeyReveal('TPM_DAAReveal_f', ~f)
	  ]->
	[Out(~f)]

/*
The host needs to store the keys on behalf of the TPM as it has
limited memory. The host then builds the credential request data CertReq and
instructs the TPM to sign this data with the private provisioning key PC

Modification: Included the generation and encryption of the EV's CertReq
*/
rule Host_Store_DAA:
	let 
		PC_PD=<'PC_public_data',pk(~pc)>

		m=<pke,pk(~pc), CCdaa_PD, 'join_Issuer_1'>
	in
	[In_S($PS, $AS, < CCdaa_SD,CCdaa_PD, 'returnDAAKey'>)
	, Host_State_02( $PS, $AS, pke, PC_PD, PC_SD )
	]
	--[ 
		PlatformSendKeys($PS, $AS, pke, CCdaa_PD, pk(~pc))
		, Alive($AS)
		, Role('Platform')
		, Store_DAA($PS, $AS)
		, OnlyOnce('Host_Store_Keys')
	  ]->
	[ 
	Out_S_B($AS, $I, <m, 'CPS_Fwd_Req'>) //CPS_I is included as CS and CSO know chosen CPS
	, Host_State_05($PS, $AS, $I,  pke, CCdaa_PD, CCdaa_SD)
	]

//Issuer: verify the curlyK and the signature before issuing the proper credentials
//Modification: Changed to model new behavior of eMSP issuer, i.e., interaction with CPS and inclusion of EMSP_Cert.
rule Issuer_Issue_Credentials:
	let 
		//inputs
		Q=multp(f, 'P1')
		CCdaa_PD=<'DAA_public_data', Q>
		m=<pke,pk(pc), CCdaa_PD, 'join_Issuer_1'>

		//inputs from Issuer PK
		pkX=PkX(~x,'P2')
		pkY=PkY(~y,'P2')
				
		//new values to be calculated
		A=multp(~r,'P1')
		B=multp(~y,A)
		C=plus(multp(~x,A),multp(multp(multp(~r,~x),~y),Q))
		D=multp(multp(~r,~y),Q)
		
		R_B=RB(~l,'P1')
		R_D=RD(~l,Q)
		
		u=H_n_8('P1', Q, R_B, R_D, A, B, C, D)
		j=plus(~l,multp(multp(~y,~r),u))
		
		s_2_hat='g'^~s_2_dh //pub ecdhe key
		s_2_temp=pke^~s_2_dh //Z
		s_2=KDF_e(s_2_temp,'IDENTITY',s_2_hat,pke)		
		Q_N=<'SHA256',H_SHA256(CCdaa_PD)>			//the name of the DAA key
		k_e=KDF_a(s_2,'STORAGE',Q_N)				
		k_h=KDF_a(s_2,'INTEGRITY','NULL')
		curlyK_2=curlyK(~K_2)
		curlyK_2_hat=senc(curlyK_2,k_e)
		curlyH=MAC(<len16(curlyK_2_hat),curlyK_2_hat, Q_N>,k_h)
		C_hat=senc(<A,B,C,D,u,j>,curlyK_2)

		// for import; change rnd seed to ecdh seed?
		seed_3_enc='g'^~seed_3_dh //pub ecdhe key
		seed_3_temp=pke^~seed_3_dh //Z
		seed_3=KDF_e(seed_3_temp,'DUPLICATE',seed_3_enc,pke)		
		sk_SENSITIVE=<'TPM_ALG_KEYEDHASH', 'NULL', ~obfuscationValue, ~sk_emaid>
		sk_unique=H_SHA256(<~obfuscationValue, ~sk_emaid>)
		sk_PD=<'SK_EMAID_public_data', sk_unique>
		sk_N=<'SHA256',H_SHA256(sk_PD)>
		sk_k_e=KDF_a(seed_3,'STORAGE',sk_N)				
		sk_k_h=KDF_a(seed_3,'INTEGRITY','NULL')
		sk_SENSITIVE_enc=senc(sk_SENSITIVE,sk_k_e)
		sk_SENSITIVE_hmac=MAC(<sk_SENSITIVE_enc, sk_N>,sk_k_h)
		sk_DUP=<sk_PD, sk_SENSITIVE_hmac, sk_SENSITIVE_enc, seed_3_enc>

		EMSP_Cert=<I,pkX,pkY>

		m_out=<EMSP_Cert, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, C_hat, sk_DUP, 'Host_CompleteJoin'>
	in
     [ In_S_B($AS, I, <m, 'CPS_Fwd_Req'>)
		, !Pk(I,pkX,pkY)
		, !Ltk(I,~x,~y)
		, Fr(~r)
		, Fr(~l)
		, Fr(~s_2_dh)
		, Fr(~K_2)
		, Fr(~sk_emaid)
		, Fr(~seed_3_dh)
		, Fr(~obfuscationValue) // for import
	 ] 
	 --[ Running(I, pke, <A, B, C, D>)
		, Alive(I)							//the issuer is "alive" in the protocol here
		, Honest ( I )
		, Honest ( pke )
		, Check_Ek(pke)	
		, IssuerReceivedKeys(I, pke, pk(pc), CCdaa_PD)
		, IssuerCertDAAKey(I, pke, f)
		, Secret_EMAID(I, pke, ~sk_emaid)
		, Secret_Cred(I, pke, <A, B, C, D>)
		, OnlyOnce('Issuer_Verify_Challenge')
		]->
	 [Out_S_B(I, $AS, m_out) 
	 , !Issuer_EMAID_SK(I, pke, ~sk_emaid)
	 , Out(sk_PD)
	 ]	

//Modification: added simpe rule to leak the EMAID secret key:
rule Issuer_EMAID_Reveal:
	[!Issuer_EMAID_SK(I, pke, sk_emaid)]	
	--[
		KeyReveal('Issuer_EMAID_Reveal', I),
		KeyReveal('Issuer_EMAID_Reveal_SK', sk_emaid)
	  ]->	
	[Out(sk_emaid)]

//The host verifies the signature and freshness of the received credential response,
// asking the TPM to decrypt and import the EMAID secret key (contained in sk_DUP)
// as well as the DAA credential
//Modification: Added verification of the CPS' signature
rule Host_Passthrough_2:
	let
		EMSP_Cert=<$I,pkX,pkY>
		sk_DUP=<sk_PD, sk_SENSITIVE_hmac, sk_SENSITIVE_enc, seed_3_enc>
		m=<EMSP_Cert, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, C_hat, sk_DUP, 'Host_CompleteJoin'>

	in
	[ In_S_B($I, $AS, m)
	  , Host_State_05($PS, $AS, $I, pke, CCdaa_PD, CCdaa_SD)
	 ]
	--[ Passthrough_ActivateCred2($PS, $AS)
		, OnlyOnce('Host_Passthrough_2')
	  ]->
	[ Out_S($AS,$PS,< sk_DUP, 'TPM2_Import'>)
	, Out_S($AS,$PS,< CCdaa_SD, CCdaa_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, 'TPM2_ActivateCredentials_2'>)
	, Host_State_06($PS, $AS,  pke, CCdaa_SD, CCdaa_PD, C_hat, sk_PD, EMSP_Cert) //activateData
	]

//The TPM decrypts the EMAID secret key and returns it to the host/EV
//Modification: Added TPM2_Import
rule TPM2_Import:
	let
		sk_unique=H_SHA256(<obfuscationValue, sk_emaid>)
		sk_PD=<'SK_EMAID_public_data', sk_unique>
		sk_SENSITIVE=<'TPM_ALG_KEYEDHASH', 'NULL', obfuscationValue, sk_emaid>
		sk_SENSITIVE_enc=senc(sk_SENSITIVE,sk_k_e)
		sk_DUP=<sk_PD, sk_SENSITIVE_hmac, sk_SENSITIVE_enc, seed_3_enc>

		seed_3_rec_temp=seed_3_enc^e
		seed_3_rec=KDF_e(seed_3_rec_temp,'DUPLICATE',seed_3_enc,pke)
		sk_N_rec=<'SHA256',H_SHA256(sk_PD)>
		sk_k_e_1=KDF_a(seed_3_rec,'STORAGE',sk_N_rec)				
		sk_k_h_1=KDF_a(seed_3_rec,'INTEGRITY','NULL')
		sk_SENSITIVE_hmac_1=MAC(<sk_SENSITIVE_enc, sk_N_rec>,sk_k_h_1)
		sk_SENSITIVE_rec=sdec(sk_SENSITIVE_enc,sk_k_e_1)
		sk_SD=senc(sk_SENSITIVE_rec,aes_key)
	in
	[  In_S($AS,$PS,< sk_DUP, 'TPM2_Import'>)
		, !TPM_AES_Key($PS, aes_key)
		, !TPM_ENDORSEMENT_SK($PS,e, pke)
	]
	--[
		Eq(sk_SENSITIVE_hmac_1,sk_SENSITIVE_hmac)
		, Eq(sk_k_e, sk_k_e_1)
		, EMAIDkey_Imported($PS, $AS)
		, EMAIDkey_Imported2($PS, $AS, sk_emaid)
		, Secret_Imported(pke, sk_emaid)
		, OnlyOnce('TPM2_Import')
	  ]->
	[ Out_S($PS,$AS, < sk_PD, sk_SD, 'ret_TPM2_Import'>)
		, !TPM_EMAID_SK($PS, pke, sk_emaid)
	]

//Modification: added simpe rule to leak the  EMAID secret key:
rule TPM_EMAID_Reveal:
	[!TPM_EMAID_SK($PS, pke, sk_emaid)]	
	--[
		KeyReveal('TPM_EMAID_Reveal', $PS)
		, KeyReveal('PKE_EMAID_Reveal', pke)
		, KeyRevealSK(sk_emaid)
	  ]->	
	[Out(sk_emaid)]

//TPM decrypts DAA credential and returns them to host/EV
rule TPM2_ActivateCredential_2:
	let
		//unwrap the inputs where needed
		curlyK_2_hat=senc(curlyK(K_2),k_e)
		Q=multp(~f, 'P1')
		CCdaa_PD=<'DAA_public_data', Q>
		
		//recompute
		s_2_rec_temp=s_2_hat^e						//retrieve s
		s_2_rec=KDF_e(s_2_rec_temp,'IDENTITY',s_2_hat,pke)	
		Q_N_rec=<'SHA256',H_SHA256(CCdaa_PD)>		//calculate Q_N_rec which should be the same as Q_N
		k_e_1=KDF_a(s_2_rec,'STORAGE',Q_N_rec)		//calculate k_e_1 which should be the same as k_e	
		k_h_1=KDF_a(s_2_rec,'INTEGRITY','NULL')		//calculate k_h_1 which should be the same as k_h
		curlyH_1=MAC(<len16(curlyK_2_hat),curlyK_2_hat,Q_N_rec>,k_h_1)
		curlyK_2_rec=sdec(curlyK_2_hat,k_e_1)		
	in
	[  In_S($AS,$PS,< CCdaa_SD, CCdaa_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, 'TPM2_ActivateCredentials_2'>) 
		, !TPM_AES_Key($PS, aes_key)
		, !TPM_ENDORSEMENT_SK($PS,e, pke)
	]
	--[
		Eq(curlyH_1,curlyH)
		, Eq(k_e, k_e_1)
		, CurlyK2_recomputed($PS, $AS)
		, OnlyOnce('TPM2_ActivateCredential_2')
	  ]->
	[ Out_S($PS,$AS, < curlyK_2_rec, 'ret_TPM2_ActivateCredentials_2'>) ]

//The host/EV receives the sk_emaid and the DAA credential and competes the credential installation
rule Host_JoinComplete:
	let 
		//unwrap the inputs where needed
		curlyK_2_rec=curlyK(K_2_rec)
		
		//inputs from the issuer
		pkX=PkX(x,'P2')
		pkY=PkY(y,'P2')
		EMSP_Cert=<I,pkX,pkY>

		A=multp(r,'P1')
		B=multp(y,A)
		C=plus(multp(x,A),multp(multp(multp(r,x),y),Q))
		D=multp(multp(r,y),Q)
		
		//input from Host_State
		Q=multp(~f, 'P1')
		CCdaa_PD=<'DAA_public_data', Q>
		C_hat=senc(<A,B,C,D,u,j>,curlyK_2) //we decrypt these credentials by checking that curlyK_2_rec = curlyK_2

		//recompute the hash
		R_B_dash=calcRB(minus(multp(j,'P1'), multp(u,B)))
		R_D_dash=calcRD(minus(multp(j,Q),multp(u,D)))
		u_dash=H_n_8('P1',Q,R_B_dash,R_D_dash, A, B, C, D)
	in 
	[ In_S($PS,$AS, < curlyK_2_rec, 'ret_TPM2_ActivateCredentials_2'>)
		, In_S($PS,$AS, < sk_PD, sk_SD, 'ret_TPM2_Import'>)
		, Host_State_06($PS, $AS,  pke, CCdaa_SD, CCdaa_PD, C_hat, sk_PD, EMSP_Cert)
		//, Host_State_07($PS, $AS,  pke, CCdaa_PD, C_hat, sk_PD, sk_SD, EMSP_Cert)
	]
	 --[ 
	     Eq(curlyK_2, curlyK_2_rec) //this allows C_hat to be decrypted
		, Eq(u,u_dash) 
		, Eq(verifyCre1(A,pkY,B,'P2'),accept)
		, Eq(verifyCre2(A,D,pkX,C,'P2'),accept)
		, JoinCompleted($PS, $AS, pke)
		, Commit(pke, I, <A, B, C, D>)
		, Role ('Platform')
		, Secret(pke, I, <A, B, C, D> )
		, Honest ( $PS )
		, Honest ( $AS )
		, Honest ( pke )
		, Honest ( I )
		, Commit_Test(pke, I, ~f)
		, OnlyOnce('Host_JoinComplete')
		]->
	 [ !Host_Store_Credentials($PS, $AS, pke, EMSP_Cert, A, B, C, D, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD)
	  	, Host_Org_Creds($PS, $AS, pke, A, B, C, D)
	 ]

// The following rule allows a host to leak the credentials
rule Host_CredentialsReveal:
	[Host_Org_Creds($PS, $AS, pke, A, B, C, D)]
	--[ KeyReveal('Host_OrgCred_Reveal', $AS)
	   , KeyReveal('TPM_OrgCred_Reveal', $PS)
	   , KeyReveal('PKE_OrgCred_Reveal', pke)
	  ]->
	[Out(<A, B, C, D>)]

//=============================================================	 
// Credential Installation Completed
//=============================================================	 


//=============================================================	 
// Charge Authorisation
//=============================================================	 

//CP generates and outputs ISO 15118 session id 	
rule CP_Start:
	let 
		m=<$CP, ~sid, 'ISO_SID'> 
	in
     [ Fr(~sid)
		, !CP_Initialised($CP) 
	 ]
	 --[ 
	 	 CP_Start($CP, ~sid)
		, CertifyOnlyOnce('CP_Start')
		]-> 
	 [Out(m), 
	 CP_State_00($CP, ~sid) ]


//as Host we randomise the credentials
rule Host_Randomise_Credentials:
	let 
		A=multp(r,'P1')
		B=multp(y,A)
		C=plus(multp(x,A),multp(multp(multp(r,x),y),Q))
		D=multp(multp(r,y),Q)
	
		bsn=BSN('bottom')
		R=multp(~l,A)
		S=multp(~l,B)
		T=multp(~l,C)
		W=multp(~l,D)
		
		//note that F1 and F2 are assumed to be KDFs such that (H_p(s_2_bar),y_2) is a point in G1
		s_2_bar=BSN('bottom')
		y_2=BSN('bottom')
		//J=PointG1(H_p(s_2_bar),y_2)
	in
	[ 
		!Host_Store_Credentials($PS, $AS, pke, EMSP_Cert, A, B, C, D, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD)
		, Fr(~l)
	]
	--[
		RandomisedCredentials($PS, $AS, pke)
		,CertifyOnlyOnce('Host_Randomise_Credentials')
	   ]->
	[!Host_State_08a( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, s_2_bar, y_2)
		, Host_Rnd_Creds($PS, $AS, pke, bsn, R, S, T, W)
	]

// The following rule allows a host to leak the randomised credentials
rule Host_RandomCredentialsReveal:
	[Host_Rnd_Creds($PS, $AS, pke, bsn, R, S, T, W)]
	--[
	   KeyReveal('Host_RndCred_Reveal', $AS)
	   , KeyReveal('TPM_RndCred_Reveal', $PS)
	   , KeyReveal('PKE_RndCred_Reveal', pke)
	  ]->
	[Out(<bsn, R, S, T, W>)]

//as a host, we ask the TPM to generate a commitment on the randomness of the credential randomisation
//and to create a session key
rule Host_Randomise_Credentials2:
	[ 
	 !Host_State_08a( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, s_2_bar, y_2)
	]
	--[
		RandomisedCredentials2($PS, $AS, pke)
		, CertifyOnlyOnce('Host_Randomise_Credentials2')
	   ]->
	[
		Out_S($AS,$PS,<s_2_bar,y_2,S, 'TPM2_Commit_rand'>)
		, Out_S($AS, $PS, <pke, 'createSessionKey'>)
		, Host_State_08( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD)
	]

	
//as TPM we create a commitment over the credential randomness
rule TPM2_Commit_2:
	let 
		s_2_bar=BSN('bottom')
		y_2=BSN('bottom')
		// because s_2 and y_2 are both 'bottom
		//J,K,L are also all 'bottom' and hence not needed
		E=E_S(~r_cv1,S)
		cv1val=Nonce(~cv1)
	in
	[ In_S($AS,$PS,< s_2_bar,y_2,S, 'TPM2_Commit_rand'>)
		, !TPM_DAA_SK($PS, pke, ~f)
		, Fr(~cv1)
		, Fr(~r_cv1)
	]
	--[
		TPMCommitRandomised($PS, $AS, pke)
		,TPMCommitRandomised2($PS, $AS, pke, ~f)
		, CertifyOnlyOnce('TPM2_Commit_2')
	  ]->
	[
		Out_S($PS,$AS, < S, E,cv1val, 'ret_TPM2_Commit_rand'>)
		, TPM_Commit_RCV1( $PS, $AS, pke, cv1val, ~r_cv1)
	]


//simple helper rule which provides a Session key to the host
//this is done using the appropriate TPM APIs 
rule TPM_Create_Session_Key:
	let 
		kID=DAAKeyID(~keyID) // just a tracker to help Tamarin
		pkCCsess=pk(~g)
		pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
		CCsess_SD=senc(~g,aes_key)
	in
	[In_S($AS, $PS, < pke, 'createSessionKey'>)
	 , !TPM_AES_Key($PS, aes_key) //our AES key
	 , Fr(~g) 
	 , Fr(~keyID) // id to help Tamarin pick the correct response later
	 ]
	--[
		TPM2_SessionKey_Created($PS, $AS, kID, pkCCsess_PD)
		, DeriveSessionKey($PS, $AS, ~g)
		, CertifyOnlyOnce('Create_Session_Key')
	  ]->
	[
	 Out_S($PS, $AS,< kID, CCsess_SD,pkCCsess_PD, 'createdSessionKey'>)
	 , !TPM_Session_SK($PS, pke, pkCCsess, ~g)
	]
	
//simpe rule to leak the Session secret key:
rule TPM_SessionKeyReveal:
	[ !TPM_Session_SK($PS, pke, pkCCsess, ~g) ]
	
	--[
		KeyReveal('TPM_SessionReveal_tpm', $PS)
		, KeyReveal('TPM_SessionReveal_pke', pke)
		, KeyReveal('TPM_SessionReveal_pkCCsess', pkCCsess)
	  ]->
	
	[Out(~g)]

//simple rule that allows the credentials to be re-used:
//as a host, we store the session key and commitment computed by the TPM based on
// the randomised credential
rule Host_Store_Randomised_Credentials:
	[
	 In_S($PS,$AS, <S, E,cv1val, 'ret_TPM2_Commit_rand'>)
	 , In_S($PS, $AS,< kID, CCsess_SD,pkCCsess_PD, 'createdSessionKey'>)
	 , Host_State_08( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD)
	]
	
	--[
		StoreRandomisedCredentials($PS, $AS, pke)
		, CertifyOnlyOnce('Host_Store_Randomised_Credentials')
	]->
	
	[ !Host_State_09_a($PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD,
		 sk_SD, kID, CCsess_SD,pkCCsess_PD ) 
	]


// simple rule that allows the adversary to set the used authorization counter
rule CounterAdv:
	[ In(i_x_t) ]
	--[
		CounterAdv(i_x_t)
		, CertifyOnlyOnce('CounterAdv')
	]->
	[ !OutIX(i_x_t) ]
	
// the host asks the TPM to certify the session key pair with its DAA credential
// and to compute an hmac over the authorization counter using the EMAID secret key
rule Host_Load_pkCCsess_For_Ceritfication:
	let 
		m=<$CP, sid, 'ISO_SID'> 

		//received values
		cv1val=Nonce(cv1) //explicitly stating this prevents partial deconstructions
		pkCCsess=pk(g)
		pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
		// CCsess_SD=senc(g,aes_key) //the host needs to store this on behalf of the TPM
		kID=DAAKeyID(keyID)
		
		//existing values
		A=multp(r,'P1')
		B=multp(y,A)
		C=plus(multp(x,A),multp(multp(multp(r,x),y),Q))
		D=multp(multp(r,y),Q)
	
		bsn=BSN(basename)
		R=multp(sl,A)
		S=multp(sl,B)
		T=multp(sl,C)
		W=multp(sl,D)
	
	    //computed values
		credData='CredentialData'
		c=H_k_7(credData,R,S,T,W,E, sid)

		i_x=h(i_x_t) 
		m_buffer=<'00',i_x>
	in
	[
	 !Host_State_09_a($PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD ) 
	 , In(m)
	 , !OutIX(i_x_t)
	]
	--[
		LoadKeyForCertification($PS, $AS, kID, pkCCsess_PD)
		, LoadKeyForCertification2($PS, $AS, pkCCsess)
		, AliveEV($PS, $AS, pke)
		, CertifyOnlyOnce('Host_Load_pkCCsess_For_Ceritfication')
	]->
	[ Out_S($AS, $PS, < pke, kID, CCsess_SD, pkCCsess_PD, c, cv1val, 'TPM2_Certify'>)
	, Out_S($AS, $PS, < pke, sk_PD, sk_SD,  m_buffer, 'TPM2_HMAC'>)
	, Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, c, sid, $CP, i_x )]
	

//TPM: receives key, c, cv1 and certifies the Session key with the DAA credential
rule TPM2_Load_And_Certify:
	let 
		CCsess_SD=senc(~g,aes_key) //loaded but not used as such
		kID=DAAKeyID(keyID) //only needed to keep track of multiple calls
		
		pkCCsess=pk(~g)
		pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
		pkCCsess_n=QName('SHA256',H_SHA256(pkCCsess_PD))
		
		curlyA=certData('certificationData',pkCCsess_n)
		credData='CredentialData'
		c=H_k_7(credData,R,S,T,W,E, sid)

		h1=H_k_2(c, H_6(curlyA))
		n_C=Nonce(~rnd_n_C)
		h2=H_n_2(n_C, h1)
		small_s=plus(~r_cv1, multp(h2, ~f))
	in
	[
		In_S($AS, $PS, <  pke, kID, CCsess_SD, pkCCsess_PD, c, cv1val_in, 'TPM2_Certify'>)
		, !TPM_DAA_SK($PS, pke, ~f)
		, !TPM_AES_Key($PS, aes_key) //our AES key
		, TPM_Commit_RCV1( $PS, $AS, pke, cv1val, ~r_cv1)
		, Fr(~rnd_n_C)
	 ]
	 
	--[
		TPM2_Created_Cert_TPM($PS, $AS, kID, pkCCsess_PD)
		, Eq(cv1val_in, cv1val) //ensures we have the right ~r_cv1
		, TPM_Certify_q($PS, $AS, pke, pkCCsess, ~f)
		, TPM_Cert_Test2(pke, small_s, ~f)
		, CertifyOnlyOnce('TPM2_Load_And_Certify')
	]->
	
	[Out_S($PS, $AS, <  kID, curlyA, small_s, n_C, 'ret_TPM2_Certify'>)]

// the TPM computes the MAC of ('00' || hash(authorization counter)) using the EMAID secret key
rule TPM2_HMAC:
	let 
		sk_unique=H_SHA256(<obfuscationValue, sk_emaid>)
		sk_PD=<'SK_EMAID_public_data', sk_unique>
		sk_SENSITIVE=<'TPM_ALG_KEYEDHASH', 'NULL', obfuscationValue, sk_emaid>
		sk_SD=senc(sk_SENSITIVE,aes_key)

		mac_out=MAC(m, sk_emaid)
	in
	[
		In_S($AS, $PS, < pke, sk_PD, sk_SD,  m, 'TPM2_HMAC'>)
		, !TPM_AES_Key($PS, aes_key) //our AES key
		, !TPM_EMAID_SK($PS, pke, sk_emaid) //
	 ]
	--[
		TPM_HMAC($PS, $AS, pke, sk_emaid)
		, CertifyOnlyOnce(<'TPM2_HMAC', m>)
	]->
	[Out_S($PS, $AS, < sk_PD, mac_out, 'ret_TPM2_HMAC'>)]

/*
rule TPM2_HMAC_Adv:
	[ In(<$PS, $AS, < sk_PD, mac_out, 'ret_TPM2_HMAC'>>) ]
	--[
		TPM_HMAC_A($PS, $AS, mac_out)
		, CertifyOnlyOnce('TPM2_HMAC_A')
	]->
	[Out_S($PS, $AS, < sk_PD, mac_out, 'ret_TPM2_HMAC'>)]
*/

//Host: receives certified key and mac
rule Host_Receive_Certified_Q_k2:
	[ 
		In_S($PS, $AS, < kID, curlyA, small_s, n_C, 'ret_TPM2_Certify'>)
		, In_S($PS, $AS, < sk_PD, tM_id, 'ret_TPM2_HMAC'>)
		, Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, small_c, sid, $CP, i_x )
	]
	--[
		Host_Receive_Certified_Q_k2($PS, $AS, pkCCsess_PD)
		, CertifyOnlyOnce('Host_Receive_Certified_Q_k2')
	]->
	[ !Host_State_10a( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, small_c, sid, $CP, i_x, curlyA, small_s, n_C, tM_id ) ]

//Host: completes the signature and sends the PaymentDetailsReq message to the CP
rule Host_Receive_Certified_Q_k:
	let //existing values
		EMSP_Cert=<I,pkX,pkY>
		A=multp(r,'P1')
		B=multp(y,A)
		C=plus(multp(x,A),multp(multp(multp(r,x),y),Q))
		D=multp(multp(r,y),Q)

		/*sk_unique=H_SHA256(<obfuscationValue, sk_emaid>)
		sk_PD=<'SK_EMAID_public_data', sk_unique>
		tM_id=MAC(m, sk_emaid)*/

		bsn=BSN('bottom') //basename='bottom'
		E=E_S(r_cv1,S)
		//pkCCsess=Q_K(rndKey)
		R=multp(sl,A)
		S=multp(sl,B)
		T=multp(sl,C)
		W=multp(sl,D)
		credData='CredentialData'
		kID=DAAKeyID(keyID) //needed to associate the response with the right key
		
		pkCCsess=pk(g)
		pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
		pkCCsess_n=QName('SHA256',H_SHA256(pkCCsess_PD))
		curlyA=certData('certificationData',pkCCsess_n)
		
		//received value
		n_C=Nonce(rnd_n_C)
		small_s=plus(r_cv1,multp(h2,f))
		
		small_c=H_k_7(credData,R,S,T,W,E, sid)

		//computed values
		h1_host=H_k_2(small_c, H_6(curlyA))
		h2_host=H_n_2(n_C, h1_host)
		sigma_K=<pkCCsess_PD, curlyA, bsn, R, S, T, W, h2_host, small_s, n_C>
	in
	
	[
		//In_S($PS, $AS, < kID, curlyA, small_s, n_C, 'ret_TPM2_Certify'>)
		//, In_S($PS, $AS, < sk_PD, tM_id, 'ret_TPM2_HMAC'>)
		//, Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, small_c, sid, $CP, i_x )
		!Host_State_10a( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, small_c, sid, $CP, i_x, curlyA, small_s, n_C, tM_id )
	]
	
	--[	Host_Receive_Certified_Q_K($PS, $AS, pke, kID, pkCCsess_PD)
		, Host_Sends_Certified_Q_K($PS, $AS, pke, sigma_K)
		, Host_Sends_Certified_Q_K_cred($PS, $AS, pke, R, S, T, W, sigma_K)
		, Honest ($PS)
		, Honest ($AS)
		, Honest (pke)
		, RunningEV_Test(pke, I, <A, B, C, D>)
		, RunningEV_Test2(pke, $CP, small_s, f)
		, CertifyOnlyOnce('Host_Receive_Certified_Q_K')
	   ]->
	
	[Out(<$CP, sid, EMSP_Cert, h(tM_id),  sigma_K, 'PaymentDetailsReq'>)
	, Host_State_11( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, i_x )]

// CP verifies the PaymentDetailsReq message, generates a fresh nonce_ix and sends it
// with the usual V2G PnC nonce to the EV in the PayDetailsRes message
rule CP_Check_TPM_Certificate:
	let 
		EMSP_Cert=<I,pkX,pkY>
		//ensure the right format
		//of the received values
		bsn_in=BSN('bottom')
		R=multp(sl,A)
		S=multp(sl,B)
		T=multp(sl,C)
		W=multp(sl,D)

		pkCCsess=pk(g)
		pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
		pkCCsess_n=QName('SHA256',H_SHA256(pkCCsess_PD))
		curlyA=certData('certificationData',pkCCsess_n)
		small_s=plus(r_cv1, multp(h2,f))
		n_C=Nonce(rnd_n_C)
		credData='CredentialData'
		sigma_K=<pkCCsess_PD, curlyA, bsn_in, R, S, T, W,  h2_host, small_s, n_C>
		
		//computed values
		//E_dash=minus(multp(small_s, S), multp(h2_host, W)) = E
		E_dash=calcE_S_cert(small_s, S, h2_host, W)

		//generic checks
		check1=verifyCre3(R,pkY,S,'P2')
		check2=verifyCre4(R,W,pkX,T,'P2')
		
		//certificate check
		c_dash=H_k_7(credData, R, S, T, W, E_dash, ~sid)
		h1_dash=H_k_2(c_dash, H_6(curlyA))
		h2_dash=H_n_2(n_C, h1_dash)

		m_out=<$CP, ~sid, ~nonce, ~nonce_ix, 'PaymentDetailsRes'> 
	in
	[In(<$CP, ~sid, EMSP_Cert, M_id, sigma_K, 'PaymentDetailsReq'>)
		, !Pk(I, pkX, pkY)	// Authentic from EMSP cert
		, CP_State_00($CP, ~sid)
		, Fr(~nonce), Fr(~nonce_ix)] 
	--[
		Eq(check1,accept)				//check that h_hat(R,Y)=h_hat(lA,yP2)=h_hat(lyA,P2)=h_hat(lB,P2)=h_hat(S,P2)
		, Eq(check2,accept)				//check that h_hat(R+W,X)=h_hat(T,P2)
		, Eq(h2_dash, h2_host)			//ensure that the recomputed hash matches the one provided
		, VerifiedCertificate($CP, sigma_K)
		, VerifiedCertificateDeAnonymised(bsn_in, sigma_K, f) //allows us to reason about the secret key used in signatures
		, CertifyOnlyOnce('CP_Check_TPM_Certificate')
		]->
	[
		Out(m_out)
		, CP_State_01($CP, ~sid, I, sigma_K, ~nonce,M_id, ~nonce_ix)
	]

//host receives PaymentDetailsRes message from CP and asks TPM to compute the mac_out
// of ('01' || hash(authorization counter))
rule Host_Auth:
	let 
		m=<$CP, sid, nonce, nonce_ix, 'PaymentDetailsRes'> 

		m_buffer=<'01',i_x>
	in
     [ In(m),
		Host_State_11( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, i_x )
	 ]
	 --[ 
		Host_Auth($PS, $AS, sid)
		, CertifyOnlyOnce('Host_Auth')
		]->
	 [ 
	   Out_S($AS, $PS, < pke, sk_PD, sk_SD,  m_buffer, 'TPM2_HMAC'>),
		Host_State_12( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, nonce,  nonce_ix) ]

// host receives mac from TPM and asks the TPM to sign the charge authorisation request
// with the session key
rule Host_Auth2:
	let 
		pkCCsess=pk(g)
		pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
		tM_auth=h(<M_auth, nonce_ix>)
		authH=h(<'AuthorizationReq', $CP, nonce, tM_auth>) 
	in
     [ 
	   In_S($PS, $AS, < sk_PD, M_auth, 'ret_TPM2_HMAC'>),
	   Host_State_12( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, nonce,  nonce_ix) 
	 ]
	 --[ 
		Host_Auth2($PS, $AS, sid)
		, CertifyOnlyOnce('Host_Auth2')
		]->
	 [ Out_S($AS, $PS, < CCsess_SD, pkCCsess_PD, authH, 'TPM2_Sign_S'>),
	 Host_State_13( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, nonce,  nonce_ix, M_auth) 
	  ] 

// TPM signs the authorization request with the session key and returns signature to host
rule TPM2_Sign_SessionKey:
	let 
		CCsess_SD=senc(~g,aes_key) 
		pkCCsess=pk(~g)
		pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
	in
	[	In_S($AS, $PS, <  CCsess_SD, pkCCsess_PD, hash_in, 'TPM2_Sign_S'>)
		, !TPM_AES_Key($PS, aes_key)
	 	, !TPM_Session_SK($PS, pke, pkCCsess, ~g)
	 ]
	--[
		TPM2_Sign_S($PS, $AS, pkCCsess_PD)
		, CertifyOnlyOnce(<'TPM2_Sign_SessionKey', hash_in>)
	]->
	[Out_S($PS, $AS, < pkCCsess_PD, sign(hash_in,~g), 'ret_TPM2_Sign_S'>)]

// host receives signature for authorization request from TPM and sends the 
// signed authorization request to the CP
rule Host_Auth3:
	let 
		EMSP_Cert=<I,pkX,pkY>
		pkCCsess=pk(g)
		pkCCsess_PD=<'SessionKey_public_data', pkCCsess>

		/*sk_unique=H_SHA256(<obfuscationValue, sk_emaid>)
		sk_PD=<'SK_EMAID_public_data', sk_unique>
		M_auth=MAC(m, sk_emaid)*/

		tM_auth=h(<M_auth, nonce_ix>)
		authH=h(<'AuthorizationReq', $CP, nonce, tM_auth>) 
	in
     [	In_S($PS,$AS, < pkCCsess_PD, sig_over_auth, 'ret_TPM2_Sign_S'>),
	  	Host_State_13( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, nonce,  nonce_ix, M_auth) 
	 ]
	 --[ 
		Eq(verify(sig_over_auth,authH,pkCCsess), true) //TPM response is for prev call		
		, Host_Auth3($PS, $AS, sid)
		//, CounterH(i_x_t)
		, RunningEV_Sign( pkCCsess , $CP, authH )
		, RunningEV_Auth( $PS, $AS, pke, I, M_auth )
		, RunningEV_Auth2( $PS, $AS, pke, I, M_auth, pkCCsess_PD )
		, CertifyOnlyOnce('Host_Auth3')
		]->
	 [ 	Out(<sid, authH, sig_over_auth, tM_auth, 'AuthorizationReq'>)
	 	, !Host_State_14( $PS, $AS, pke, EMSP_Cert, kID, CCsess_SD,pkCCsess_PD, sid, $CP, M_auth)
	 ]

//=============================================================	 
// Charge Authorisation Part 2
//=============================================================	 

// the CP verifies the authorization request,
// rquesting the user's authorization data from the backend
rule CP_Verify:
	let 
		bsn_in=BSN('bottom')
		R=multp(sl,A)
		S=multp(sl,B)
		T=multp(sl,C)
		W=multp(sl,D)

		pkCCsess=pk(g)
		pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
		pkCCsess_n=QName('SHA256',H_SHA256(pkCCsess_PD))
		curlyA=certData('certificationData',pkCCsess_n)
		small_s=plus(r_cv1, multp(h2,f))
		n_C=Nonce(rnd_n_C)
		sigma_K=<pkCCsess_PD, curlyA, bsn_in, R, S, T, W,  h2_host, small_s, n_C>

		m_in=<~sid, authH_in, sig_over_auth, tM_auth, 'AuthorizationReq'> 

		authH=h(<'AuthorizationReq', $CP, ~nonce, tM_auth>) 

		m_out=<M_id, ~nonce_ix, tM_auth, pkCCsess>
	in
     [ In(m_in)
		, CP_State_01($CP, ~sid, I, sigma_K, ~nonce, M_id, ~nonce_ix)
	 ]
	 --[ 
		Eq(authH_in, authH)		
		, Eq(verify(sig_over_auth,authH,pkCCsess), true)		
		, CP_Verify($CP, ~sid)
		, CommitCP($CP, pkCCsess, authH)
		, Honest(pkCCsess)
		, Honest($CP)
		, Honest(I)
		, CertifyOnlyOnce('CP_Verify')
		]->
	 [ Out(<I, <m_out, 'EMSP_Auth'>>)
	 , !CP_State_02($CP, ~sid, I, pkCCsess, tM_auth) ]

// the eMSP verifies the authorization request
rule EMSP_Auth:
	let
		i_x=h(i_x_t)
		m=<M_id_in, nonce_ix, tM_auth_in, pkCCsess>
		pkCCsess_PD=<'SessionKey_public_data', pkCCsess>

		tM_id=MAC(<'00', i_x>, ~sk_emaid)
		M_id=h(tM_id)
		M_auth=MAC(<'01',i_x>, ~sk_emaid)
		tM_auth=h(<M_auth, nonce_ix>)
	in
     [ In(<I, <m, 'EMSP_Auth'>>)
	 , !OutIX(i_x_t)
	 , !Issuer_EMAID_SK(I, pke, ~sk_emaid)
	 ] 
	 --[ Eq(M_id, M_id_in)
	 	, Eq(tM_auth, tM_auth_in)
		, CommitEMSP(I, pke, M_auth)
		, CommitEMSP2(I, pke, M_auth, pkCCsess_PD)
		, CommitEMSP_sk(I, pke, ~sk_emaid)
		, CommitEMSP_sk2(I, pke, M_auth, ~sk_emaid)
		, Honest(I)
		, Honest(pke)
		, OnlyOnce_i_x(I, ~sk_emaid, i_x)
		, CertifyOnlyOnce('EMSP_Auth')
		]->
	 [
	 !Issuer_State_Charge(I, pke, ~sk_emaid, i_x, M_auth, pkCCsess)
	 ]	

// the CP sends the charge data to the vehicle for attestation
rule CP_DataSend:
	let 
		data=<$CP, ~sid, 'charge_data',~dataID>
	in
     [ Fr(~dataID)
		, !CP_State_02($CP, ~sid, I, pkCCsess, tM_auth)
	 ]
	 --[ 
	 	CP_DataSend($CP, ~sid, ~dataID),
		CertifyOnlyOnce('CP_DataSend')
		]->
	 [ Out(data)
		, CP_State_03($CP, ~sid, I, pkCCsess, tM_auth, ~dataID) ]

// the EV (using its TPM) signs the charge data together with ev_h, a hash over the authorisation
// value used during charge authorisation and its public session key to bind them
// charge data to the corresponding charge authorisation.
rule EV_DataSign:
	let 
		EMSP_Cert=<I,pkX,pkY>
		pkCCsess=pk(~g)
		pkCCsess_PD=<'SessionKey_public_data', pkCCsess>

		data=<$CP, sid, 'charge_data',dataID>

		ev_h=h(<'EV_h',M_auth,pkCCsess>)
		dataTBS=h(<'charge_data',dataID, ev_h>)
	in
     [ In(data)
	   , !Host_State_14( $PS, $AS, pke, EMSP_Cert, kID, CCsess_SD,pkCCsess_PD, sid, $CP, M_auth)
	 ]
	 --[ EV_DataSign($PS, $AS, kID, pkCCsess_PD, sid, dataID)
		, CertifyOnlyOnce('EV_DataSign')
	 ]->
	 [ Out_S($AS, $PS, <  CCsess_SD, pkCCsess_PD, dataTBS, 'TPM2_Sign_S'>)
	   , Host_State_15( $PS, $AS, pke, EMSP_Cert, kID, CCsess_SD,pkCCsess_PD, sid, $CP, M_auth, data, dataTBS) 
	 ]

// the EV receives the signed charge data from the TPM, sends the signature
// to the CP
rule EV_DataSign_Send:
	let 
		EMSP_Cert=<I,pkX,pkY>
		pkCCsess=pk(~g)
		pkCCsess_PD=<'SessionKey_public_data', pkCCsess>

		data=<$CP, sid, 'charge_data',dataID>

		ev_h=h(<'EV_h',M_auth,pkCCsess>)
		dataTBS=h(<'charge_data',dataID, ev_h>)
		m_out=<ev_h, dataTBS, dataSig>

		m_o2=<'charge_data',dataID, dataSig, ev_h>
	in
     [ In_S($PS, $AS, < pkCCsess_PD, dataSig, 'ret_TPM2_Sign_S'>)
	    , Host_State_15( $PS, $AS, pke, EMSP_Cert, kID, CCsess_SD,pkCCsess_PD, sid, $CP, M_auth, data, dataTBS)
	 ]
	 --[ 
		Eq(verify(dataSig,dataTBS,pkCCsess), true), //TPM response is for prev call
	 	EV_DataSign_Send($PS, $AS, kID, pkCCsess_PD, sid, dataID),
	 	EV_DataSign_Send2($PS, $AS, pkCCsess),
		RunningEV_Data($PS, $AS, pke, I, <M_auth, 'charge_data', dataID>),
		RunningEV_Data2(pke, I, <M_auth, 'charge_data', dataID>),
		CertifyOnlyOnce('EV_DataSign_Send')
		]->
	 [ Out(m_out), Out(m_o2) ]

// The CP receives the signed charge data from the EV, verifies the signatures
// and forwards the data and signature to the eMSP
rule CP_DataRec:
	let 
		data=<$CP, ~sid, 'charge_data',~dataID>
		m_in=<ev_h, dataTBS_in, dataSig>
		dataTBS=h(<'charge_data',~dataID, ev_h>)
		
		M_auth=MAC(<'01',i_x>, sk_emaid)
		tM_auth=h(<M_auth, nonce_ix>)

		m_out=<'charge_data',~dataID, dataSig, ev_h>
	in
     [ In(m_in)
		, CP_State_03($CP, ~sid, I, pkCCsess, tM_auth, ~dataID)
	 ]
	 --[ 
	    Eq(dataTBS_in, dataTBS)
	 	, Eq(verify(dataSig,dataTBS,pkCCsess), true)
	 	, CP_DataRec($CP, ~sid, ~dataID)
	 	, CP_DataRec2($CP, pkCCsess, sk_emaid)
		, CertifyOnlyOnce('CP_DataRec')
		]->
	 [ Out(<I, <m_out, 'EMSP_Data'>>) ]


// The eMSP verifies the signed charge data and its link to a previous charge
// authorisation
rule EMSP_Data:
	let
		M_auth=MAC(<'01',i_x>, ~sk_emaid)
		m=<'charge_data',dataID, dataSig, ev_h_in>

		pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
		ev_h=h(<'EV_h',M_auth,pkCCsess>)
		dataTBS=h(<'charge_data', dataID, ev_h>)
	in
     [ In(<I, <m, 'EMSP_Data'>>)
	 , !Issuer_State_Charge(I, pke, ~sk_emaid, i_x, M_auth, pkCCsess)
	 ] 
	 --[ Eq(ev_h, ev_h_in)
	 	, Eq(verify(dataSig,dataTBS,pkCCsess), true)
		, Honest(I)
		, Honest(pke)
		, CommitEMSP_Data(I, pke, <M_auth, 'charge_data', dataID>)
		, CommitEMSP_Data2(I, pke, <M_auth, 'charge_data', dataID>, pkCCsess_PD)
		, OnlyOnce_i_x(I, M_auth, dataID)
		, CertifyOnlyOnce('EMSP_Data')
		]->
	 [
	 ]	

//======================================================================================
// This concludes the description of the scheme using Tamarin rules
// The next section contains the lemmas encapsulating the various properties that we
// want the scheme to have.
//======================================================================================

//======================================================================================
// We start off with some general checks that verify some of the restriction/assumptions
// which we have imposed on our scheme.
//======================================================================================

// Helper lemma for proof generation
lemma source_of_key_reveal_sk [sources]:
// Each EMAID secret key compromised by the adversary has been previously generated by an issuer
"
All sk_emaid #i .
	(
		KeyRevealSK(sk_emaid) @ i
		==>
		(
			(Ex Iss pke #j . Secret_EMAID(Iss, pke, sk_emaid) @ j & j<i)
		)
	)
"

// When a TPM and Host are bound together, they have to be different entities
lemma restriction_bind:
"
	All Ent1 Ent2 #i . 
		(Bind(Ent1, Ent2) @ i)
		==>
		(not(Ent1=Ent2))
"

//a TPM is associated with one and only one host:
lemma restriction_one_host_per_tpm:
"
	All TPM Host1 Host2 #i #j. 
		(Bind(Host1,TPM)@i & Bind(Host2,TPM)@j)
		==> 
		((#i=#j))
"

//a host has only one TPM:
lemma restriction_one_tpm_per_host:
"
	All TPM1 TPM2 Host #i #j. 
		((Bind(Host,TPM1)@i & Bind(Host,TPM2)@j)
		==>
		(#i=#j))
"

// any endorsement key that is presented to the issuer must have been generated
// by a TPM. This restrictions represents the fact that the issuer will check
// each endorsement key and only allow ones that were created by a TPM
lemma restriction_pke_comes_from_tpm:
	"All pke #i . 
		Check_Ek(pke) @ i 
		==>
		(
			(Ex TPM Host #j .
				(
					TPM2_EK_Created(TPM, Host, pke) @ j
					& 
					(#j<#i)
				)
			)
		)
	"

//======================================================================================
// Correctness properties
//======================================================================================

// the issuer should be able to check at least 2 pkes
lemma correctness_verify_multiple_pkes: exists-trace
	"Ex Issuer TPM1 TPM2 Host1 Host2 pke1 qpd1 pcpd1 pcpd2 pke2 qpd2  #t1 #t2 #t3 #t4 .
		PlatformSendKeys(TPM1, Host1, pke1, qpd1, pcpd1) @ t1
		& PlatformSendKeys(TPM2, Host2, pke2, qpd2, pcpd2) @ t2
		& IssuerReceivedKeys(Issuer, pke1, pcpd1, qpd1) @ t3
		& IssuerReceivedKeys(Issuer, pke2, pcpd2, qpd2) @ t4
		& not(pke1=pke2) 
		& not(qpd1=qpd2) 
		& not(pcpd1=pcpd2) 
		& not(Host1=Host2) 
		& not(TPM1=TPM2)

		//we had no key reveal
		& not( Ex RevealEvent ENTITY #k1 . KeyReveal(RevealEvent, ENTITY)@k1) 
	"

// the issuer should be able to check at least 2 pkes from different Issuers
lemma correctness_verify_multiple_pkes_diff_I: exists-trace
	"Ex Issuer1 Issuer2 TPM Host pke1 qpd1 pcpd1 pcpd2 pke2 qpd2  #t1 #t2 #t3 #t4 .
		PlatformSendKeys(TPM, Host, pke1, qpd1, pcpd1) @ t1
		& PlatformSendKeys(TPM, Host, pke2, qpd2, pcpd2) @ t2
		& IssuerReceivedKeys(Issuer1, pke1, pcpd1, qpd1) @ t3
		& IssuerReceivedKeys(Issuer2, pke2, pcpd2, qpd2) @ t4
		& (pke1=pke2) 
		& not(Issuer1=Issuer2)

		//we had no key reveal
		& not( Ex RevealEvent ENTITY #k1 . KeyReveal(RevealEvent, ENTITY)@k1) 
	"

// we should be able to get two sets of certs using the same 
// randomised credentials
lemma correctness_two_certs_same_credentials: exists-trace
	"Ex TPM Host pke R S T W sigma1 sigma2 #t01 #t02 .
	Host_Sends_Certified_Q_K_cred(TPM, Host, pke, R, S, T, W, sigma1) @ t01
	& Host_Sends_Certified_Q_K_cred(TPM, Host, pke, R, S, T, W, sigma2) @ t02
	& #t01<#t02
	& not(sigma1=sigma2)
	& //we had no key reveal
	  not( Ex RevealEvent ENTITY #k1 . KeyReveal(RevealEvent, ENTITY)@k1) 
	& //we only join once
	  (All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j)
	"


// we should be able to get two sets of certs using different 
// randomised credentials
lemma correctness_two_certs_different_credentials: exists-trace
	"Ex TPM Host pke 
	    R1 S1 T1 W1 sigma1 
		R2 S2 T2 W2 sigma2 
		#t01 #t02 .
	Host_Sends_Certified_Q_K_cred(TPM, Host, pke, R1, S1, T1, W1, sigma1) @ t01
	& Host_Sends_Certified_Q_K_cred(TPM, Host, pke, R2, S2, T2, W2, sigma2) @ t02
	& not(#t01=#t02)
	& //credentials are different
	  not(R1=R2) & not(S1=S2) & not(T1=T2) & not(W1=W2)
	& not(sigma1=sigma2)
	& //we had no key reveal
	  not( Ex RevealEvent ENTITY #k1 . KeyReveal(RevealEvent, ENTITY)@k1) 
	& //we only join once
	  (All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j) 
	"
	
// it should be possible for an vehicle to have two different charge processes
// authorized by the same eMSP
lemma correctness_two_auths_same_ev_same_key: exists-trace
	"Ex Iss Iss2 pke 
	    M_auth1 M_auth2
		sk_emaid1 sk_emaid2
		#t01 #t02 .
	CommitEMSP_sk2(Iss, pke, M_auth1, sk_emaid1) @ t01
	& CommitEMSP_sk2(Iss2, pke, M_auth2, sk_emaid2) @ t02
	& (Iss=Iss2)
	& not(#t01=#t02)
	& //credentials are different
	  not(M_auth1=M_auth2)
	& (sk_emaid1=sk_emaid2)
	& //we had no key reveal
	  not( Ex RevealEvent ENTITY #k1 . KeyReveal(RevealEvent, ENTITY)@k1) 
	& //we only join same ev once
	  (All TPM Host pke sk_emaid #i . 
		TPM_HMAC(TPM, Host, pke, sk_emaid)@i 
		 ==> (sk_emaid=sk_emaid1) | (sk_emaid=sk_emaid2)) 
	& //we only join once
	  (All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j) 
	& //we only sign same value once
	  (All hash_in #i #j . 
		CertifyOnlyOnce(<'TPM2_Sign_SessionKey', hash_in>)@i & CertifyOnlyOnce(<'TPM2_Sign_SessionKey', hash_in>)@j
		 ==> (#i=#j)) 
	& //we only mac same value once
	  (All m #i #j . 
		CertifyOnlyOnce(<'TPM2_HMAC', m>)@i & CertifyOnlyOnce(<'TPM2_HMAC', m>)@j
		 ==> (#i=#j)) 
	"

// it should be possible for the eMSP to authorise two charge processes by
// different EVs
lemma correctness_two_auths_diff_ev_diff_key: exists-trace
	"Ex Iss pke1 pke2
	    M_auth1 M_auth2
		sk_emaid1 sk_emaid2
		#t01 #t02 .
	CommitEMSP_sk2(Iss, pke1, M_auth1, sk_emaid1) @ t01
	& CommitEMSP_sk2(Iss, pke2, M_auth2, sk_emaid2) @ t02
	& not(#t01=#t02)
	& //credentials are different
	  not(M_auth1=M_auth2)
	& not(sk_emaid1=sk_emaid2)
	& not(pke1=pke2)
	& //we had no key reveal
	  not( Ex RevealEvent ENTITY #k1 . KeyReveal(RevealEvent, ENTITY)@k1)
	& //we only join same ev once
	  (All TPM Host pke #i #j . 
		JoinCompleted(TPM, Host, pke)@i & JoinCompleted(TPM, Host, pke)@j
		 ==> (#i=#j)) 
	& //we only alive same ev once
	  (All TPM Host pke #i #j . 
		AliveEV(TPM, Host, pke)@i & AliveEV(TPM, Host, pke)@j
		 ==> (#i=#j)) 
	& //we only sign same value once
	  (All hash_in #i #j . 
		CertifyOnlyOnce(<'TPM2_Sign_SessionKey', hash_in>)@i & CertifyOnlyOnce(<'TPM2_Sign_SessionKey', hash_in>)@j
		 ==> (#i=#j)) 
	& //we only mac same value once
	  (All m #i #j . 
		CertifyOnlyOnce(<'TPM2_HMAC', m>)@i & CertifyOnlyOnce(<'TPM2_HMAC', m>)@j
		 ==> (#i=#j)) 
	"

// it should be possible for an vehicle to have two different charge processes
// using different EMAID keys authorized by the same eMSP
lemma correctness_two_auths_same_ev_diff_key: exists-trace
	"Ex Iss pke
	    M_auth1 M_auth2
		sk_emaid1 sk_emaid2
		#i01 #i02 
		#t01 #t02 .
	Secret_Imported(pke, sk_emaid1) @ i01
	& Secret_Imported(pke, sk_emaid2) @ i02
	& CommitEMSP_sk2(Iss, pke, M_auth1, sk_emaid1) @ t01
	& CommitEMSP_sk2(Iss, pke, M_auth2, sk_emaid2) @ t02
	& not(#i01=#i02) & not(#t01=#t02)
	& //credentials are different
	  not(M_auth1=M_auth2)
	& not(sk_emaid1=sk_emaid2)
	& //we had no key reveal
	  not( Ex RevealEvent ENTITY #k1 . KeyReveal(RevealEvent, ENTITY)@k1) 
	& //we only run ev once w/ same cred 
	  (All pke1 I1 pke2 I2 cred1 #i #j . 
		RunningEV_Test(pke1, I1, cred1)@i & RunningEV_Test(pke2, I2, cred1)@j
		 ==> (#i=#j) ) 
	& //we only TPM once
	(All PS PS2 #i #j . 
		TPM_Init(PS)@i & TPM_Init(PS2)@j
		 ==> (#i=#j) ) 
	& //we only import same once
	  (All pke1 pke2 sk_emaid #i #j . 
		Secret_Imported(pke1, sk_emaid)@i & Secret_Imported(pke2, sk_emaid)@j
		 ==> (#i=#j) )
	& //we only join same ev
	  (All TPM1 Host1 pke1 #i . 
		JoinCompleted(TPM1, Host1, pke1)@i
		 ==> (pke1 = pke)) 
	& //we only sign same value once
	  (All hash_in #i #j . 
		CertifyOnlyOnce(<'TPM2_Sign_SessionKey', hash_in>)@i & CertifyOnlyOnce(<'TPM2_Sign_SessionKey', hash_in>)@j
		 ==> (#i=#j)) 
	& //we only mac same value once
	  (All m #i #j . 
		CertifyOnlyOnce(<'TPM2_HMAC', m>)@i & CertifyOnlyOnce(<'TPM2_HMAC', m>)@j
		 ==> (#i=#j)) 
	"

// it should be possible for the eMSP to obtain two charge data messages
// signed by the same vehicle
lemma correctness_two_data: exists-trace
	"Ex Iss pke 
		data1 data2
		#i01 #i02 
		#t01 #t02 .
	RunningEV_Data2(pke, Iss, data1) @ i01
	& RunningEV_Data2(pke, Iss, data2) @ i02
	& CommitEMSP_Data(Iss, pke, data1) @ t01
	& CommitEMSP_Data(Iss, pke, data2) @ t02
	& not(#i01=#i02) & not(#t01=#t02)
	& //credentials are different
	  not(data1=data2)
	& //we had no key reveal
	  not( Ex RevealEvent ENTITY #k1 . KeyReveal(RevealEvent, ENTITY)@k1) 	
	& //we only run ev once
	  (All pke1 I1 pke2 I2 cred1 cred2 #i #j . 
		RunningEV_Test(pke1, I1, cred1)@i & RunningEV_Test(pke2, I2, cred2)@j
		 ==> (#i=#j) ) 
	& //we only auth once
	(All TPM1 Host1 sid1 TPM2 Host2 sid2 #i #j . 
		Host_Auth3(TPM1, Host1, sid1)@i & Host_Auth3(TPM2, Host2, sid2)@j
		 ==> (#i=#j)) 
	& //we only join once
	  (All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j) 
	& //we only sign same value once
	  (All hash_in #i #j . 
		CertifyOnlyOnce(<'TPM2_Sign_SessionKey', hash_in>)@i & CertifyOnlyOnce(<'TPM2_Sign_SessionKey', hash_in>)@j
		 ==> (#i=#j)) 
	& //we only mac same value once
	  (All m #i #j . 
		CertifyOnlyOnce(<'TPM2_HMAC', m>)@i & CertifyOnlyOnce(<'TPM2_HMAC', m>)@j
		 ==> (#i=#j)) 
	"

// Correctness of the complete credential installation process
lemma correctness_credential_req: exists-trace
" Ex TPM Host I pke pcpd qpd sk_emaid //n
					#t01 #t02 #t03 #t04 #t05 #t06 #t07 #t08 #t09
					#t10 #t14 //#t16 #t17 #t18 #t19 
					#t20 #t21 #t22 #t23
.
					
	//we initiated at one issuer, host/EV, and TPM
	Issuer_Init(I) @ t01 
	& Host_Init(Host) @ t02 
	& TPM_Init(TPM) @ t03 
	
	//we had no key reveal
	& not( Ex RevealEvent ENTITY #k1 . KeyReveal(RevealEvent, ENTITY)@k1) 
		
	//we had a successful Platform set-up
	 & Bind(TPM, Host) @ t04 
	 
	//created an endorsement key EK
	& TPM2_EK_Created(TPM, Host, pke) @ t05 
	
	//stored the EK with the host	
	& Store_EK(TPM, Host) @ t06

	//created an provisioning key PC
	& TPM2_PC_Created(TPM, Host) @ t07
	
	// stored the provisioning key with the host
	& Store_PC(TPM, Host) @ t08

	//created a DAA key
	& TPM2_DAA_Created(TPM, Host) @ t09	
	
	//stored the DAA key with the host	
	& Store_DAA(TPM, Host) @ t10

	//recieved and answered the credential request as the issuer
	& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t14
	& Secret_EMAID(I, pke, sk_emaid) @ t14

	// received the response by the host
	& Passthrough_ActivateCred2(TPM, Host) @ t20
	
	// imported the EMAID key into the TPM and returned it to the host
	& Secret_Imported(pke, sk_emaid) @ t21
	
	//decrypted the DAA credentials in the TPM and returned them to the host
	& CurlyK2_recomputed(TPM, Host) @ t22

	//received the DAA and EMAID key as the host and completed the credential installation
	& JoinCompleted(TPM, Host, pke) @ t23

	// With the correct temporal ordering		
	& t01<t02 //Issuer gets created before Host
	& t02<t04 //Host gets created before Bind
	& t03<t04 //TPM get created before Bind
	& t04<t05 
	& t05<t06 
	& t06<t07 
	& t07<t08 
	& t08<t09
	& t09<t10
	& t10<t14
	& t14<t20
	& t20<t21
	& t21<t22
	& t22<t23

  //restrict the trace further by preventing each rule from firing more than once
	& 	(All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j)
"

// Correctness of the charge autorisation process until the EV sent the authorisation values
lemma correctness_charge_authorisation_req_1: exists-trace
" Ex TPM Host I pke pcpd qpd //n
					#t01 #t02 #t03 #t04 #t05 #t06 #t07 #t08 
					#t12
					//#t12 #t13 #t14 #t15 #t16 #t17 #t18 #t19 
					#t20 
					#t21 #t22
					//certify steps
					kID pkCCsess_PD sigma
					#t23 #t24 #t25 #t26 #t27 #t28 
.
					
	//we initiated at least 3 entities
	
	Issuer_Init(I) @ t01 
	& Host_Init(Host) @ t02 
	& TPM_Init(TPM) @ t03 
	
	
	//we had no key reveal
	& not( Ex RevealEvent ENTITY #k1 . KeyReveal(RevealEvent, ENTITY)@k1) 
		

	//we had a successful Platform set-up
	 & Bind(TPM, Host) @ t04 
	 
	//created an endorsement key EK
	& TPM2_EK_Created(TPM, Host, pke) @ t05 
	
	//stored the EK with the host	
	& Store_EK(TPM, Host) @ t06

	& TPM2_PC_Created(TPM, Host) @ t07
	//created a DAA key
	& TPM2_DAA_Created(TPM, Host) @ t08

	
	//stored the DAA key with the host	
	//& Store_Keys(TPM, Host) @ t10

	//check the EK and CCdaa_PD as the issuer
	& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t12


	& Passthrough_ActivateCred2(TPM, Host) @ t20
	
	& CurlyK2_recomputed(TPM, Host) @ t21
	
	& JoinCompleted(TPM, Host, pke) @ t22
	
	//Certify Key 
	
	& RandomisedCredentials(TPM, Host, pke) @ t23
	
	& TPMCommitRandomised(TPM, Host, pke) @ t24
	
	& TPM2_SessionKey_Created(TPM, Host, kID, pkCCsess_PD) @ t25
	
	& LoadKeyForCertification(TPM, Host, kID, pkCCsess_PD) @ t26
	
	& TPM2_Created_Cert_TPM(TPM, Host, kID, pkCCsess_PD) @ t27
	
	& Host_Sends_Certified_Q_K(TPM, Host, pke, sigma) @ t28

	& t01<t02 //Issuer gets created before Host
	& t02<t04 //Host gets created before Bind
	& t03<t04 //TPM get created before Bind
	& t04<t05 
	& t05<t06 
	& t06<t07 
	& t07<t08 
	& t08<t12
	& t12<t20
	& t20<t21
	& t21<t22
	//certify steps
	& t22<t23
	& t23<t24
	& t24<t25
	& t25<t26
	& t26<t27
	& t27<t28
 
  //restrict the trace further by preventing each rule from firing more than once
	
	& 	(All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j)
	& 	(All event #i #j . CertifyOnlyOnce(event)@i & CertifyOnlyOnce(event)@j ==> #i=#j)

"


// Correctness of charge authorisation request until the request is received by the CP
lemma correctness_charge_authorisation_req_2: exists-trace
" Ex TPM Host I pke pcpd qpd //n
					#t01 #t02 #t03 #t04 #t05 #t06 #t07 #t08 
					#t12 // #t14 #t15 #t16 #t17 #t18 #t19 
					#t20 #t21 #t22
					//certify and verify steps
					kID pkCCsess_PD sigma CP
					#t23 #t24 #t25 #t26 #t27 #t28 #t29
.

	//we initiated at least 3 entities
	
	Issuer_Init(I) @ t01 
	& Host_Init(Host) @ t02 
	& TPM_Init(TPM) @ t03 
	
	
	//we had no key reveal
	& not( Ex RevealEvent ENTITY #k1 . KeyReveal(RevealEvent, ENTITY)@k1) 
		

	//we had a successful Platform set-up
	 & Bind(TPM, Host) @ t04 
	 
	//created an endorsement key EK
	& TPM2_EK_Created(TPM, Host, pke) @ t05 
	
	//stored the EK with the host	
	& Store_EK(TPM, Host) @ t06

	& TPM2_PC_Created(TPM, Host) @ t07
	//created a DAA key
	& TPM2_DAA_Created(TPM, Host) @ t08

	
	//stored the DAA key with the host	
	//& Store_Keys(TPM, Host) @ t10

	//check the EK and CCdaa_PD as the issuer
	& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t12


	& Passthrough_ActivateCred2(TPM, Host) @ t20
	
	& CurlyK2_recomputed(TPM, Host) @ t21
	
	& JoinCompleted(TPM, Host, pke) @ t22
	
	//Certify and verify starts here
	
	& RandomisedCredentials(TPM, Host, pke) @ t23
	
	& TPMCommitRandomised(TPM, Host, pke) @ t24
	
	& TPM2_SessionKey_Created(TPM, Host, kID, pkCCsess_PD) @ t25
	
	& LoadKeyForCertification(TPM, Host, kID, pkCCsess_PD) @ t26
	
	& TPM2_Created_Cert_TPM(TPM, Host, kID, pkCCsess_PD) @ t27
	
	& Host_Sends_Certified_Q_K(TPM, Host, pke, sigma) @ t28
	
	& VerifiedCertificate(CP, sigma) @ t29
	
		
	& t01<t02 //Issuer gets created before CPS
	& t02<t04 //Host gets created before Bind
	& t03<t04 //TPM get created before Bind
	& t04<t05 
	& t05<t06 
	& t06<t07 
	& t07<t08 
	& t08<t12
	& t12<t20
	& t20<t21
	& t21<t22
	//quote and verify
	& t22<t23
	& t23<t24
	& t24<t25
	& t25<t26
	& t26<t27
	& t27<t28
	& t28<t29

 
  //restrict the trace further by preventing each rule from firing more than once
	
	& 	(All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j)
	& 	(All event #i #j . CertifyOnlyOnce(event)@i & CertifyOnlyOnce(event)@j ==> #i=#j)

"	


// Correctness of the complete charge authorisation process
lemma correctness_charge_authorisation: exists-trace
" Ex TPM Host I pke pcpd qpd //n
					#t01 #t02 #t03 #t04 #t05 #t06 #t07 #t08 
					#t12 // #t14 #t15 #t16 #t17 #t18 #t19 
					#t20 #t21 #t22
					//certify and verify steps
					kID pkCCsess_PD sigma
					#t23 #t24 #t25 #t26 #t27 #t28 #t29
					CP sid  #t01_2
					sk_emaid
					#t30 #t31 #t32 #t33 #t34 #t35 #t36
					M_auth
.

	//we initiated at least 3 entities
	
	Issuer_Init(I) @ t01 
	& CP_Init(CP) @ t01_2 
	& Host_Init(Host) @ t02 
	& TPM_Init(TPM) @ t03 
	
	
	//we had no key reveal
	& not( Ex RevealEvent ENTITY #k1 . KeyReveal(RevealEvent, ENTITY)@k1) 
		

	//we had a successful Platform set-up
	 & Bind(TPM, Host) @ t04 
	 
	//created an endorsement key EK
	& TPM2_EK_Created(TPM, Host, pke) @ t05 
	
	//stored the EK with the host	
	& Store_EK(TPM, Host) @ t06

	& TPM2_PC_Created(TPM, Host) @ t07
	//created a DAA key
	& TPM2_DAA_Created(TPM, Host) @ t08

	
	//stored the DAA key with the host	
	//& Store_Keys(TPM, Host) @ t10

	//check the EK and CCdaa_PD as the issuer
	& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t12


	& Passthrough_ActivateCred2(TPM, Host) @ t20
	
	& CurlyK2_recomputed(TPM, Host) @ t21
	
	& JoinCompleted(TPM, Host, pke) @ t22
	
	//Certify and verify starts here
	
	& RandomisedCredentials(TPM, Host, pke) @ t23
	
	& TPMCommitRandomised(TPM, Host, pke) @ t24
	
	& TPM2_SessionKey_Created(TPM, Host, kID, pkCCsess_PD) @ t25
	
	& LoadKeyForCertification(TPM, Host, kID, pkCCsess_PD) @ t26
	
	& TPM2_Created_Cert_TPM(TPM, Host, kID, pkCCsess_PD) @ t27
	
	& Host_Sends_Certified_Q_K(TPM, Host, pke, sigma) @ t28
	
	& VerifiedCertificate(CP, sigma) @ t29
	
	
	& Host_Auth(TPM, Host, sid) @ t30
	& TPM_HMAC(TPM, Host, pke, sk_emaid) @ t31
	& Host_Auth2(TPM, Host, sid) @ t32
	& TPM2_Sign_S(TPM, Host, pkCCsess_PD) @ t33
	& RunningEV_Auth(TPM, Host, pke, I, M_auth ) @ t34
	& CP_Verify(CP, sid) @t35
	& CommitEMSP(I, pke, M_auth) @t36

	& t01<t02 //Issuer gets created before CPS
	& t02<t04 //Host gets created before Bind
	& t03<t04 //TPM get created before Bind
	& t04<t05 
	& t05<t06 
	& t06<t07 
	& t07<t08 
	& t08<t12
	& t12<t20
	& t20<t21
	& t21<t22
	//quote and verify
	& t22<t23
	& t23<t24
	& t24<t25
	& t25<t26
	& t26<t27
	& t27<t28
	& t28<t29
	& t29<t30
	& t30<t31
	& t31<t32
	& t32<t33
	& t33<t34
	& t34<t35
	& t35<t36

 
  //restrict the trace further by preventing each rule from firing more than once
	
	& 	(All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j)
	& 	(All event #i #j . CertifyOnlyOnce(event)@i & CertifyOnlyOnce(event)@j ==> #i=#j)

"	


// Correctness of the charge data authentication process
lemma correctness_charge_data_authentication: exists-trace
" Ex TPM Host I pke pcpd qpd //n
					#t01 #t02 #t03 #t04 #t05 #t06 #t07 #t08 
					#t12 // #t14 #t15 #t16 #t17 #t18 #t19 
					#t20 #t21 #t22
					//certify and verify steps
					kID pkCCsess_PD sigma
					#t23 #t24 #t25 #t26 #t27 #t28 #t29
					CP sid  #t01_2
					sk_emaid