daa_pnc_credential_installation.spthy

theory DDA_PnC_credential_installation
begin
 
/*
Protocol:	DAA_PnC
Properties:	SR2 - Secure Credential Installation

This Tamarin model is used to verify the security of the installation 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
CPS			- Certificate Provisioning Service (limited to one instance)

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_credential_installation.spthy\
 --heuristic=S --quit-on-warning\
 --prove +RTS -N8 -RTS

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

analyzed: join2_wCP2test3.spthy

  forwarded_credential_res_source (all-traces): verified (265 steps)
  secrecy_of_cps_private_key (all-traces): verified (3 steps)
  secrecy_of_pke (all-traces): verified (6 steps)
  integrity_of_forwarded_credential_res_m (all-traces): verified (166 steps)
  restricition_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)
  restricition_pke_comes_from_tpm (all-traces): verified (14 steps)
  correctness_verify_multiple_pkes (exists-trace): verified (70 steps)
  correctness_verify_multiple_pkes_diff_I (exists-trace): verified (69 steps)
  correctness_credential_req (exists-trace): verified (22 steps)
  correctness_credential_req_res_1 (exists-trace): verified (57 steps)
  correctness_credential_req_res_2 (exists-trace): verified (67 steps)
  auth_aliveness_issuer_very_weak (all-traces): verified (49 steps)
  auth_aliveness_issuer (all-traces): verified (49 steps)
  auth_aliveness_host (all-traces): verified (6 steps)
  auth_weak_agreement_host (all-traces): verified (63 steps)
  auth_non_injective_agreement_host_issuer (all-traces): verified (63 steps)
  auth_injective_agreement_host_issuer (all-traces): verified (205 steps)
  auth_non_injective_agreement_CPS_EV (all-traces): verified (32 steps)
  auth_injective_agreement_CPS_EV (all-traces): verified (48 steps)
  auth_secrecy_cre_ev (all-traces): verified (303 steps)
  auth_secrecy_cre_iss (all-traces): verified (116 steps)
  auth_secrecy_emaid_iss (all-traces): verified (36 steps)
  auth_secrecy_emaid_ev (all-traces): verified (123 steps)

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

real	14m4,080s
user	67m9,053s
sys	22m50,816s

*/

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

functions:  accept/0, MAC/2, KDF_AES/1, KDF_EK/1,KDF_a/3, KDF_e/4, certData/2,
             multp/2, plus/2, minus/2, len16/1, 
             H_SHA256/1,  H_k_1/1, H_k_2/2, H_k_4/4, 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
			 

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,Qk_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,Qk_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,Qk_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 certificate installation response CertRes is only accepted once by a EV/Host
restriction only_once_certres: 
"All event #i #j . 
	(OnlyOnceCertRes(event) @ i & OnlyOnceCertRes(event) @ 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)"
	
//the certificate provisioning service (CPS) should only be initialized once 
restriction single_cps_single_init:
	"All CPS_I CPS_I2 #i #j . (CPS_Init(CPS_I) @ i & CPS_Init(CPS_I2) @ j) ==> (#i=#j)"
	
//each charge point (CP) should only be initialized 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 CPS cannot be initialised with the same identity
restriction no_shared_id_between_issuer_cps:
	"All Ent1 Ent2 #i #j . 
	(Issuer_Init(Ent1) @ i & CPS_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))"

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

//When initialized, a host, tpm, 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 & CPS_Init(Ent4) @ l) 
	==> 
	(not(Ent1=Ent2) & not (Ent1=Ent3) & not (Ent1=Ent4)
	& not (Ent2=Ent3) & not (Ent2=Ent4)
	& not (Ent3=Ent4))"

//When initialized, a host, tpm, issuer, CPS and CP must have different identities
// This restriction includes the restrictions above, however, they are maintained for performance reasons
restriction no_shared_id_between_tpm_host_issuer_cps_cp:
	"All Ent1 Ent2 Ent3 Ent4 Ent5 #i #j #k #l #m. 
	(Host_Init(Ent1) @ i & TPM_Init(Ent2) @ j & Issuer_Init(Ent3) @ k & CPS_Init(Ent4) @ l & CP_Init(Ent5) @ m) 
	==> 
	(not(Ent1=Ent2) & not (Ent1=Ent3) & not (Ent1=Ent4) & not (Ent1=Ent5)
	& not (Ent2=Ent3) & not (Ent2=Ent4) & not (Ent2=Ent5)
	& not (Ent3=Ent4) & not (Ent3=Ent5)
	& not (Ent4=Ent5))"



//=========================================
// 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 CPS set-up
rule CPS_Init:
		[Fr(~cps)]
		--[CPS_Init($CPS_I)
		   , CPS_Init2($CPS_I, ~cps)
		   , OnlyOnce('CPS_Init')]->
		[!LtkCPS($CPS_I,~cps)
		   , !PkCPS($CPS_I, pk(~cps))
		   , Out(pk(~cps))
		   , !CPS_Initialised($CPS_I)
		]

// simple key reveal rule for the CPS' secret key pair
rule CPS_KeyReveal:
	[!LtkCPS($CPS_I, ~cps)]
	--[KeyReveal('CPS_KeyReveal', $CPS_I)]->
	[Out(~cps)]


// 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)
	in
		[Fr(~TPM_AES_Seed),
		 Fr(~TPM_EK_Seed)]
		--[TPM_Init($PS)
		   , OnlyOnce('TPM_INIT')]->
		[!TPM_AES_Key($PS, aes_key), 
		 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_Key(PS, aes_key)]
	--[KeyReveal('TPM_AESReveal', PS)]->
	[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_reuse:
	[ In_S($PS, $AS,< PC_SD,PC_PD, 'returnPCKey'>)]
	--[ OnlyOnce('Host_Store_PC_reuse')
	  ]->
	[ !Host_Store_PC_reuse($PS, $AS,< PC_SD,PC_PD, 'returnPCKey'>)]
rule Host_Store_PC:
	let 
	PC_PD=<'PC_public_data',pk(~pc)>
	in
	[ !Host_Store_PC_reuse($PS, $AS,< PC_SD,PC_PD, 'returnPCKey'>),
	 !Host_State_01( $PS, $AS, pke ) ]
	--[ Store_PC($PS, $AS)
		, OnlyOnce('Host_Store_PC')
	  ]->
	[Out_S($AS,$PS, < pke, 'createDAAKey'>), 
	 Host_State_02( $PS, $AS, pke, PC_PD, PC_SD )]


//=====================================================================	 
// Generating and Sending the Contract Credential Installation Request
//=====================================================================
/*
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')
	Q_PD=<'DAA_public_data', Q>
	Q_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,< Q_SD,Q_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)
	  ]->
	[Out(~f)]

// CP sends a nonce to the EV (abstracting the timestamp) 
rule CP_Nonce:
	let 
		m=<$CP, ~sid, ~n, 'CP_Nonce'> 
	in
     [ Fr(~sid)
		, Fr(~n)
		, !CP_Initialised($CP)
	]
	--[ 
		CP_Nonce($CP, ~n, ~sid)
		, OnlyOnce('CP_Nonce')
	]->
	[Out(m)
		, CP_State_00($CP, ~sid, ~n) 
	]

/*
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 
		Q=multp(~f, 'P1')
		Q_PD=<'DAA_public_data', Q>

		PC_PD=<'PC_public_data',pk(~pc)>
		m_in=<$CP, sid, n, 'CP_Nonce'>

		m=<pke,pk(~pc), Q_PD, ~res_n, 'join_Issuer_1'> //EV's CertReq with OEM prov cert and public DAA key
		signed_m=H_SHA256(<m, pk(~cps), n>) //for signature over CertReq; signed_m=<m, pk(~cps)> for inclusion of CPS' public key
	in
	[ In(m_in)
		, Fr(~res_n)
		, In_S($PS, $AS, < Q_SD,Q_PD, 'returnDAAKey'>)
		, Host_State_02( $PS, $AS, pke, PC_PD, PC_SD )
		, !PkCPS(CPS_I, pk(~cps)) //from Charge Station but authentic due to certificate
	]
	--[ 
		 Store_DAA($PS, $AS)
		, Store_DAA_N($PS, $AS, n, sid)
		, Store_DAA_m($PS, $AS, m, pk(~pc))
		, Store_DAA_resn(~res_n)
		, OnlyOnce('Host_Store_Keys')
	  ]->
	[ Host_State_03( $PS, $AS,  pke, Q_PD, Q_SD, pk(~cps), CPS_I, m, signed_m, pk(~pc), sid, n ,  $CP)
		, !Host_Store_DAAKey($PS, $AS, pke, Q_PD, Q_SD)
		, Out_S($AS,$PS,< PC_SD,PC_PD, signed_m, 'TPM2_Sign'>) 
	]

// The TPM signs the credential request generated by rule Host_Store_DAA and returns the signature to the host 
rule TPM_Sign_Req:
	let
		PC_PD=<'PC_public_data',pk(~pc)>
		PC_SD=senc(~pc,aes_key)
    in
	[  In_S($AS,$PS,< PC_SD,PC_PD, signed_m, 'TPM2_Sign'>) 
		, !TPM_AES_Key($PS, aes_key)
	 	, !TPM_PC_SK($PS, pke, ~pc)
	]
	--[ TPM2_Sign($PS, $AS)
		, OnlyOnce('TPM_Sign_Req')
	  ]->
	[ Out_S($PS,$AS, < sign(signed_m,~pc), 'ret_TPM2_Sign'>)
	]

//Upon receiving the signature for a credential request, the host generates the request and sends it to the CP
rule Host_Send_Req:
	let 
		e=KDF_EK(~TPM_EK_Seed)
		pke='g'^e

		//m=<pke,pk(~pc), Q_PD, 'join_Issuer_1'> //EV's CertReq with OEM prov cert and public DAA key
		//signed_m=H_SHA256(<m, pk(~cps), n>)  // for signature over CertReq; signed_m=<m, pk(~cps)> for inclusion of CPS' public key
		Q=multp(~f, 'P1')
		Q_PD=<'DAA_public_data', Q>

		m=<pke,pk(~pc), Q_PD, ~res_n, 'join_Issuer_1'> //EV's CertReq with OEM prov cert and public DAA key
		signed_m=H_SHA256(<m, pk(~cps), n>) // for signature over CertReq; signed_m=<m, pk(~cps)> for inclusion of CPS' public key

		sig_over_m=sign(signed_m,~pc)
	in
	[In_S($PS,$AS, < sig_over_m, 'ret_TPM2_Sign'>)
	, Host_State_03( $PS, $AS,  pke, Q_PD, Q_SD, pk(~cps), CPS_I, m, signed_m, pk(~pc), sid, n ,  CP)
	]
	--[  PlatformSendKeys($PS, $AS, pke, Q_PD, pk(~pc))
		, Alive($AS)
		, Role('Platform')
		, Honest( $PS )
		, Honest($AS)
		, Honest( pke )
		, Honest( CPS_I )
		, RunningEV( pke , CPS_I, signed_m )
		, RunningEV2( ~res_n )
		, RunningEV3( sid )
		, OnlyOnce('Host_Send_Req')
	  ]->
	[ !EK_FOR_ISSUER(<pke,pk(~pc)>) //a TPM created the pke and pk(pc), both certified by OEM
	, Out(<sid, CPS_I, aenc(<sig_over_m,m>,pk(~cps)), 'Host_Send_Req'>) //CPS_I is included as CS and CSO know chosen CPS
	, !Host_State_05($PS, $AS,  pke, pk(~cps), CPS_I, sid,  CP, ~res_n)
	]


//==================================================================	 
// Contract Credential Installation Request Handling in the Backend
//==================================================================

//The CP forwards the signed credential request to the CPS
rule CP_Fwd_Credential_Request:
     [ In(<sid, CPS_I, aenc_m, 'Host_Send_Req'>)
		, CP_State_00(CP, sid, n)
	 ]
	 --[ 
		CP_Fwd_Credential_Request(CP, CPS_I, n)
		, OnlyOnce('CP_Fwd_Credential_Request')
		]->
	 //secure channel to Backend
	 [Out_S_B(CP, CPS_I, < aenc_m, n>), 
	 !CP_State_01(CP, CPS_I, sid, $AS) ]	

// The CPS verifies the credential request
//Modification: Added verification of the credential request by the CPS
rule CPS_Verify_Credential_Request:
	let 
		//inputs
		m_in=<pke,pk(pc), Q_PD, res_n, 'join_Issuer_1'>
		//decrypt and parse request
		aenc_m=aenc(<sig, m_in>, pk(~cps))

		signed_m=H_SHA256(<m_in, pk(~cps), n>) //signed_m=<m_in, pk(~cps)>
	in
     [ In_S_B(CP, CPS_I, <aenc_m, n>)
		, !EK_FOR_ISSUER(<pke,pk(pc)>) 	//a TPM created the pke and pk(pc), both certified by OEM
		//, !PkCPS(CPS_I,pk(~cps))
		, !LtkCPS(CPS_I,~cps)
		, Fr(~r)
	 ]
	 --[ Eq(verify(sig,signed_m,pk(pc)), true)		
		, Check_Ek(pke)		
		, Check_QPD(Q_PD)
		, Honest ( CPS_I )
		, Honest ( CP )
		, Honest ( pke )
		, CPSReceivedReq(CPS_I, pke, pk(pc), Q_PD)
		, CommitCPS(CPS_I, pke, signed_m)
		, OnlyOnce('CPS_Verify_Credential_Request')
		]->
	 [!CPS_State_00(CPS_I, CP, ~r, <m_in, 'CPS_Fwd_Req'>) ]	

// The CPS forwards a valid credential request to the Issuer/eMSP
rule CPS_Fwd_Credential_Request:
	let 
		//inputs
		m_in=<pke,pk(pc), Q_PD, res_n, 'join_Issuer_1'>
		m_out=<pke,pk(pc), Q_PD, 'join_Issuer_1'>
	in
     [ !CPS_State_00(CPS_I, CP, ~r, <m_in, 'CPS_Fwd_Req'>)
		, !Issuer_Initialised(I)
		,Fr(~reqID)
	 ]
	 --[ 
		CPSfwdReq(CPS_I, I, pke, pk(pc), Q_PD)
		//, OnlyOnceCertRes(<CPS_I, I, ~r>)
		, OnlyOnce('CPS_Fwd_Credential_Request')
		]->
	 //secure channel to EMSP
	 [Out_S_B(CPS_I, I, <~reqID, m_out, 'CPS_Fwd_Req'>), 
	 CPS_State_01(CPS_I, CP, ~reqID, res_n)]	

//Issuer: verify the curlyK and the signature before issuing the proper credentials for the host/EV and sending them back to the CPS
//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
		pke='g'^e

		Q=multp(f, 'P1')
		Q_PD=<'DAA_public_data', Q>
		m=<pke,pk(pc), Q_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 (shared ECDH secret)
		s_2=KDF_e(s_2_temp,'IDENTITY',s_2_hat,pke)		
		Q_N=<'SHA256',H_SHA256(Q_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(CPS_I, I, < reqID, 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
		, !PkCPS(CPS_I,pk(~cps))
	 ] 
	 --[ Running(I, pke, <A, B, C, D>)
		, Alive(I)							//the issuer is "alive" in the protocol here
		, Honest ( I )
		, Honest ( pke )
		, Honest ( CPS_I )
		, Role ('Issuer')
		, IssuerReceivedKeys(I, pke, pk(pc), Q_PD)
		, Secret_EMAID(I, pke, ~sk_emaid)
		, Secret_Cred(I, pke, <A,B,C,D>)
		, Iss_s2(s_2, e)
		, Iss_s22(s_2, e, pke, <A,B,C,D>, curlyK_2, k_e)
		, Iss_s3(seed_3, e)
		, Iss_m(m_out)
		, OnlyOnce('Issuer_Verify_Challenge')
		]->
	 [Out_S_B(I, CPS_I, <reqID, m_out>) 
	 , !Issuer_EMAID_SK(I, ~sk_emaid)
	 ]	

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


//The CPS signes the credential response and forwards it to the CP
//Modification: Added signature over the credential response by the CPS
rule CPS_Sign_Credential_Response:
	let 
		//inputs
		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'>
		m_out=<EMSP_Cert, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, C_hat, sk_DUP, res_n, 'Host_CompleteJoin'>
		//sign response
		sig_m=sign(m_out,~cps)		
	in
     [ In_S_B(I, CPS_I, <reqID, m>)
		//, !PkCPS(CPS_I,pk(~cps))
		, !LtkCPS(CPS_I,~cps)
		, CPS_State_01(CPS_I, CP, reqID, res_n)
	 ]
	 --[ CPSReceivedRes(CPS_I)
	 	, CPSsignedRes(CPS_I, ~cps, m_out)
	 	, CPSsignedRes2(CPS_I, ~cps, m_out, sig_m)
		, OnlyOnce('CPS_Sign_Credential_Response')
		]->
	 [Out_S_B(CPS_I, CP, < m_out, sig_m>) ]	

//The CP forwards the received data to the host/EV
rule CP_Fwd_Credential_Res:
	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, res_n, 'Host_CompleteJoin'>
		m_emsp=<EMSP_Cert, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, C_hat, sk_DUP, 'Host_CompleteJoin'>
		//sig_m=sign(m,cps)	
	in
     [ In_S_B(CPS_I, $CP, < m, sig_m>)
		, !CP_State_01($CP, CPS_I, sid, $AS)
		, !PkCPS(CPS_I, pk(cps)) 
	 ]
	 --[  CP_Fwd_Credential_Res($CP, CPS_I, sid)
		, OnlyOnce('CP_Fwd_Credential_Res')
		, CP_C_hat(C_hat)
		, CP_m(m)
		, CP_m2(sid, m_emsp, sig_m, res_n)
		]->
	 [Out(<sid, m, sig_m, 'CP_Fwd_Res'>)]	

//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
		//inputs
		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, ~res_n, 'Host_CompleteJoin'>

		activateData=<Q_SD, Q_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat>
	in
	[ In(<sid, m, sig_m, 'CP_Fwd_Res'>)
	  	, !Host_State_05($PS, $AS, pke, pk(cps), CPS_I, sid,  CP, ~res_n)
	  	, !Host_Store_DAAKey($PS, $AS, pke, Q_PD, Q_SD)
		, !PkCPS(CPS_I, pk(cps)) // from Charge Station but authentic due to certificate
	 ]
	--[ Eq(verify(sig_m,m,pk(cps)), true)
		, Passthrough_ActivateCred2($PS, $AS)
		, Passthrough_ActivateCred2_sid($PS, $AS, sid)
		, Passthrough_m($PS, $AS, m, pk(cps))
		, OnlyOnceCertRes(<$PS, $AS, Q_PD, I, sid>)
		, OnlyOnce('Host_Passthrough_2')
	  ]->
	[ Out_S($AS,$PS,< sk_DUP, 'TPM2_Import'>)
	, Out_S($AS,$PS,< Q_SD, Q_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, 'TPM2_ActivateCredentials_2'>)
	, Host_State_06($PS, $AS,  pke, Q_PD, C_hat, activateData,  CP,  EMSP_Cert, CPS_I, sk_PD)
	]
//====================================================
// Contract Credential Installation Response Handling
//====================================================
//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)
		, 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)]
*/

/*
rule Host_Passthrough_3:
	let
		activateData=<Q_SD, Q_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat>
	in
	[  In_S($PS,$AS, < sk_PD, sk_SD, 'ret_TPM2_Import'>)
	 	, Host_State_06($PS, $AS,  pke, Q_PD, C_hat, activateData,  CP,  EMSP_Cert, CPS_I)
		, !PkCPS(CPS_I, pk(cps))
	 ]
	--[  Passthrough_3($PS, $AS)
		, OnlyOnce('Host_Passthrough_3')
		, Host_C_hat(C_hat, pk(cps))
	  ]->
	[ Out_S($AS,$PS,< Q_SD, Q_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, 'TPM2_ActivateCredentials_2'>)
		, Host_State_07($PS, $AS,  pke, Q_PD, C_hat, sk_PD, sk_SD,  CP,  EMSP_Cert, CPS_I)
	]*/

//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')
		Q_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(Q_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,< Q_SD, Q_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, 'TPM2_ActivateCredentials_2'>)