daa_pnc_charge_authorisation_offline.spthy

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

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

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

analyzed: daa_pnc_charge_authorisation_offline.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 (102 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 (58 steps)
  correctness_charge_authorisation (exists-trace): verified (76 steps)
  correctness_charge_data_authentication (exists-trace): verified (90 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_Off (all-traces): verified (100 steps)
  test_auth_non_injective_agreement_CP_sessKey (all-traces): verified (46 steps)
  test_auth_non_injective_agreement_CP (all-traces): verified (47 steps)
  test_auth_injective_agreement_CP (all-traces): verified (133 steps)
  test_new_test_CP_sessKey (all-traces): verified (88 steps)
  test_key_tpm_binding_test2 (all-traces): verified (87 steps)
  test_new_auth_non_injective_agreement_CP_data (all-traces): verified (105 steps)
  test_new_auth_injective_agreement_CP_data (all-traces): verified (111 steps)
  test_auth_injective_agreement_CP_test2 (all-traces): verified (9 steps)
  test_test1 (all-traces): verified (45 steps)
  test_test2 (all-traces): verified (100 steps)
  test_test (all-traces): verified (84 steps)

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

real	25m16,817s
user	131m36,396s
sys	38m37,382s

*/

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) ]

rule ChanOut_A:
    [ Out_A($A,$B,x) ]
    --[ ChanOut_A($A,$B,x) ]->
    [ Auth($A,x), Out(<$A,$B,x>) ]

rule ChanIn_A:
	[ Auth($A,x), In($B) ]
    --[ ChanIn_A($A,$B,x) ]->
    [ In_A($A,$B,x) ]


rule ChanIn_A_ADV1:
	[ In(<$A,$B,x>) ]
	--[ ChanIn_A($A,$B,x)
		, KeyReveal('TLS_KeyReveal', $A) 
	]->
    [ In_A($A,$B,x) ]

rule ChanIn_A_ADV2:
	[ In(<$A,$B,x>) ]
	--[ ChanIn_A($A,$B,x)
		, KeyReveal('TLS_KeyReveal', $B) 
	]->
    [ In_A($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
//=============================================================	 

rule CounterAdv:
	[ In(i_x_t) ]
	--[
		CounterAdv(i_x_t)
		, CertifyOnlyOnce('CounterAdv')
	]->
	[ !OutIX(i_x_t) ]
	

rule EMSP_CSO_Offline_Calc:
	let
		i_x=h(i_x_t)

		tM_id=MAC(<'00', i_x>, ~sk_emaid)
		M_id=h(tM_id) //id_ix
		CPM_id=h(<M_id, $CP>)
		M_auth=MAC(<'01',i_x>, ~sk_emaid) //auth_ix
		tM_auth=h(<M_auth, ~nonce_ix>)
		CPM_auth=h(tM_auth)
		localAuth_ix=<CPM_id, ~nonce_ix, CPM_auth>
	in
     [ !OutIX(i_x_t)
	 , !Issuer_EMAID_SK(I, pke, ~sk_emaid)
	 , !CP_Initialised($CP) 
	 , Fr(~nonce_ix)
	 ] 
	 --[  EMSP_Offline_Calc(I, pke, ~sk_emaid, i_x)
	 	, EMSP_Offline_Calc2(I, $CP, pke, tM_auth)
		, CertifyOnlyOnce('EMSP_Offline_Calc')
		]->
	 [
	  Out_A(I, $CP, <localAuth_ix>)
	 ]	

rule CP_Start:
	let 
		m=<$CP, ~sid, 'ISO_SID'> 
		localAuth_ix=<CPM_id, nonce_ix, CPM_auth>
		localAuth=<I, CPM_id, nonce_ix, CPM_auth>
	in
     [ Fr(~sid)
	 	, In_A(I, $CP, <localAuth_ix>)
		, !CP_Initialised($CP) 
	 ]
	 --[ 
	 	 CP_Start($CP, ~sid)
		, CertifyOnlyOnce('CP_Start')
		]-> 
	 [Out(m)
		, CP_State_00($CP, ~sid, localAuth)
	 ]


//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')
	   ]->
	[
	//Out_S($AS,$PS,<s_2_bar,y_2,S, 'TPM2_Commit_rand'>)
	//, Out_S($AS, $PS, <pke, 'createSessionKey'>)
	!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 Host we randomise the credentials
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 some more elements
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)