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)
	]
	--[
		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:
rule Host_Store_Randomised_Credentials:
	/*let
		bsn=BSN('bottom')
		R=multp(~l,A)
		S=multp(~l,B)
		T=multp(~l,C)
		W=multp(~l,D)
	in*/	
	[
	 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 ) 
	]


// 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 
		EMSP_Cert=<I,pkX,pkY>
		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)
		, OnlyOnce_i_x(pke, I, i_x)
		, 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_K2($PS, $AS, pke, sigma_K, g)
		, 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>

		localAuth=<I, CPM_id, nonce_ix, CPM_auth>
		
		//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)

		CPM_id_in=h(<M_id, $CP>)

		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, localAuth)
		, Fr(~nonce)] 
	--[
		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
		, Eq(CPM_id_in, CPM_id)	
		, VerifiedCertificate($CP, sigma_K)
		, VerifiedCertificate2($CP, sigma_K, pk(g), f)
		, 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, localAuth)
	]

//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)
		, Host_Auth22($PS, $AS, authH)
		, 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)
		, TPM2_Sign_S2($PS, $AS, pkCCsess_PD, hash_in)
		, 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( pke , $CP, authH )
		, RunningEV_Sign2( $PS, $AS, $CP, authH )
		, RunningEV_Sign3( $PS, $AS, $CP, authH, pkCCsess, sig_over_auth )
		, 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>

		localAuth=<I, CPM_id, nonce_ix, CPM_auth>

		m_in=<~sid, authH_in, sig_over_auth, tM_auth, 'AuthorizationReq'> 
		
		CPM_auth_in=h(tM_auth)
		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, localAuth)
	 ]
	 --[ 
		Eq(authH_in, authH)		
		, Eq(verify(sig_over_auth,authH,pkCCsess), true)		
		, Eq(CPM_auth_in, CPM_auth)		
		, CP_Verify($CP, ~sid)
		, CommitCP($CP, pkCCsess, authH)
		, CommitCP2($CP, pkCCsess, authH, sig_over_auth)
		, CommitCP3($CP, I, tM_auth, pkCCsess)
		, Honest(I)
		, Honest($CP)
		, 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>),
		RunningEV_Data3($PS, $AS, $CP, dataTBS),
		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)
	 	, CP_DataRec3($CP, pkCCsess, dataTBS)
		, Honest(I)
		, 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
					#t30 #t31 #t32 #t33 #t34 #t35 #t36
					M_auth
					dataID
					#t37 #t38 #t39 #t40 #t41 #t42
.

	//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

	& CP_DataSend(CP, sid, dataID) @t37
	& EV_DataSign(TPM, Host, kID, pkCCsess_PD, sid, dataID) @t38
	& TPM2_Sign_S(TPM, Host, pkCCsess_PD) @t39
	& EV_DataSign_Send(TPM, Host, kID, pkCCsess_PD, sid, dataID) @t40
	& CP_DataRec(CP, sid, dataID) @t41
	& CommitEMSP_Data(I, pke, <M_auth, 'charge_data', dataID>) @t42

	& 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
	& t36<t37
	& t37<t38
	& t38<t39
	& t39<t40
	& t40<t41
	& t41<t42

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

"	


lemma correctness_with_adv: 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
					#t23 #t24 #t25 #t26 #t27 #t28
					sid sk_emaid
					#t30 #t31 #t32 #t33 #t34 #t36
					M_auth  dataID
					#t38 #t39 #t40 #t42
.

	//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_Receive_Certified_Q_K(TPM, Host, pke, kID, pkCCsess_PD) @ t28
	
	
	& 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_Auth2(TPM, Host, pke, I, M_auth, pkCCsess_PD ) @ t34
	& CommitEMSP2(I, pke, M_auth, pkCCsess_PD) @t36

	& EV_DataSign(TPM, Host, kID, pkCCsess_PD, sid, dataID) @t38
	& TPM2_Sign_S(TPM, Host, pkCCsess_PD) @t39
	& EV_DataSign_Send(TPM, Host, kID, pkCCsess_PD, sid, dataID) @t40
	& CommitEMSP_Data2(I, pke, <M_auth, 'charge_data', dataID>, pkCCsess_PD) @t42

	& 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<t30
	& t30<t31
	& t31<t32
	& t32<t33
	& t33<t34
	& t34<t36
	& t36<t38
	& t38<t39
	& t39<t40
	& t40<t42

	& not(Ex CP_x #a1 .	CP_Init(CP_x) @ #a1 )
  //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)

"


//======================================================================================
// In the following section we look at the security properties for
// the charge authorization and charge data authorization in our model
//======================================================================================

// *********** SR2 Secure Credential Installation - Authentication *********************
// The following lemmas go through aspects of Lowe's Authentication hierarchy. 

// Aliveness of Host
// This lemma simply shows that at the end of a run of the protocol, an issuer must have been created previously.
// But it does not require the issuer to have been involved in the running of the protocol at all.
// This is a very weak requirement.
lemma auth_aliveness_issuer_very_weak:
"
All Iss pke n #i .
   // For all commited JOIN sessions running between a platform and issuer on the term(s) n 
	(
		Commit( pke, Iss, n ) @ i
		==>
		(
			// Implies that there is an active issuer
			(Ex #j . Issuer_Init (Iss) @ j)
			|
			// or there has been a key reveal 
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)
"

//this lemma shows that the issuer was involved in a run of the protocol (at least one of its rules fired) 
//or that some of the keys of the entities involved were revealed
lemma auth_aliveness_issuer:
"
All Iss pke n1 #i .
   // For all commited JOIN sessions running between a platform and issuer on the term(s) n 
	(
		Commit( pke, Iss, n1 ) @ i 

	==> // Implies that an issuer has previously been involved in a protocol run 
       
		(	(Ex #k . Alive (Iss) @ k)
			|
			// or there has been a key reveal of one of the entities involved in the Commit 
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)

"

// This lemma simply shows that at the end of a run of the protocol for the issuer with a host, 
// the host must have been involved in a run of a protocol that lead up to the final Issuer rule firing
lemma auth_aliveness_host:
"
All Iss pke n #i .
	// For all JOIN sessions running between an issuer and a host, Host, on the term(s) n
	(
		( Running(Iss, pke,  n) @ i )
		==>
		(	//the host was involved in a run of the protocol that 
			//resulted in a message exchange between the host and the issuer
			(Ex Host2 #k . Alive(Host2) @ k & Role('Platform') @ k)
			|
			// or there has been a key reveal of one of the entities involved in the Commit 
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)	
		)
	)
	"

// Agreement checks 

// This lemma guarantees that whenever the host completes a run of the protocol, apparently with the issuer, 
// then the issuer has previously been running the protocol, apparently with the host.
// This lemma (and also the subsequent agreement lemmas) fails if the endorsement key is not included in
// the str constructed in the Host_ReceiveCurlyK rule which then forms part of the hash p computed in
// Host_ReceiveEAndCV.
lemma auth_weak_agreement_host:
"
All Iss TPM Host pke n1 #i .
	(
		(
			// For all commited JOIN sessions running between a platform and issuer on the term(s) n 
			Commit( pke, Iss, n1 ) @ i & JoinCompleted(TPM, Host, pke) @ i
		)
		==>
        ( 
			// Implies there exists a running issuer on some term(s) n2 
			(Ex n2 #j . Running( Iss, pke, n2 ) @ j) 
			|
			// or there has been a key reveal of one of the entities involved in the Commit 
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)
"

// This lemma shows that the Host is in a non-injective agreement with the issuer on
// the credentials if, whenever the Host completes a run of the protocol, apparently with the Issuer, 
// then the Issuer has previously been running the protocol, apparently with the Host, and
//the two principals agreed on the terms n
lemma auth_non_injective_agreement_host_issuer:
"
All Iss pke n #i .
	(
		(
			// For all commited JOIN sessions running between a platform (identified by is endorsement public key pke) and issuer on the term(s) n 
			Commit( pke, Iss, n ) @ i 
		)
		==>
		(
			// Implies there exists a running issuer on the same term
			(Ex #j . Running( Iss, pke, n ) @ j) 
			|
			// or there has been a key reveal of one of the entities involved in the Commit
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)
"
// This lemma shows that the Host is in an injective agreement with the issuer on
// the credentials if, whenever the Host completes a run of the protocol, apparently with the Issuer, 
// then the Issuer has previously been running the protocol, apparently with the Host, and
//the two principals agreed on the terms n
// Additionally, there is a unique matichng partner instance for each completed run of an agent.
lemma auth_injective_agreement_host_issuer:
"
All Iss pke n #i .
	(
		(
			// For all commited JOIN sessions running between a platform (identified by is endorsement public key pke) and issuer on the term(s) n 
			Commit( pke, Iss, n ) @ i 
		)
		==>
		(
			(
				// Implies there exists a running issuer on the same term
				(Ex #j . 
					(
						Running( Iss, pke, n ) @ j
						& 
						(#j<#i) 
						&
						// And each commited JOIN session corresponds to a unique issuer run
						( not(
							Ex Iss2 pke2 #i2 . ( Commit( pke2, Iss2, n) @ i2 & not(#i2=#i) )
							)
						)
					)
				)
			)
			|
			// or there has been a key reveal of one of the entities involved in the Commit
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)
"


// ************* SR2 Secure Credential Installation - Secrecy ************************

// CRE secrecy from the perspective of both the Issuer and the TPM/Host.
lemma auth_secrecy_cre:
"
  All Iss pke cred #i. 
    // somebody claims to have setup a shared secret, 
    Secret( pke, Iss, cred ) @ i
    ==>
		// implies the adversary does not know it 
		not( Ex #k. K( cred ) @ k )
		|
		// or it is the case that a key has been revealed 
		(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
"


// CRE secrecy from the perspective of both the Issuer and the TPM/Host.
lemma auth_secrecy_emaid:
"
  All  Iss pke sk_emaid #i. 
    // somebody claims to have setup a shared secret, 
    Secret_EMAID( Iss, pke, sk_emaid ) @ i
    ==>
		// implies the adversary does not know it 
		not( Ex #k. K( sk_emaid ) @ k )
		|
		// or it is the case that a key has been revealed 
		(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
"


// **************************** SR3 Secure Charge Authorisation ************************************
// If the eMSP accepts a charge authorisation request, then the EV that apparently
// initiated a charge process has been previously active in the protocol
lemma auth_aliveness_charge:
"
All Iss pke n1 #i .
   // For all commited charge authorisations by an eMSP for an EV (identified by its public endorsement key pke)
	(
		CommitEMSP( Iss, pke, n1 ) @ i 

	==> // Implies that the EV has previously been involved in a protocol run
		(	
			(Ex TPM Host #k . AliveEV(TPM, Host, pke) @ k)
			|
			// or there has been a key reveal of the entities involved in the Commit 
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)

"

// If the eMSP accepts a charge authorisation request, then the EV that apparently
// initiated a charge process has been previously requested a charge authorisation
// by the eMSP (however, not necessary with the same parameters n)
lemma auth_weak_agreement_charge:
"
All Iss pke n1 #i .
	// For all commited charge authorisations by an eMSP for an EV (identified by its public endorsement key pke)
	(
		CommitEMSP( Iss, pke, n1 ) @ i 
	==> // Implies that the EV has been previously requested a charge authorisation by the same eMSP
        ( 
			(Ex TPM Host n2 #j . RunningEV_Auth( TPM, Host, pke, Iss, n2 ) @ j) 
			|
			// or there has been a key reveal of the entities involved in the Commit 
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)
"

// If the eMSP accepts a charge authorisation request, then the EV that apparently
// initiated a charge process has been previously requested a charge authorisation
// by the eMSP and they agree on the parameters n of the request
lemma auth_non_injective_agreement_charge:
"
All Iss pke n #i .
	// For all commited charge authorisations by an eMSP for an EV (identified by its public endorsement key pke)
	(
		CommitEMSP( Iss, pke, n ) @ i 
		
	==> // Implies that the EV has been previously requested a charge authorisation by the same eMSP with the same parameters n
		(
			(Ex TPM Host #j . RunningEV_Auth( TPM, Host, pke, Iss, n ) @ j) 
			|
			// or there has been a key reveal of the entities involved in the Commit
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)
"

// If the eMSP accepts a charge authorisation request, then the EV that apparently
// initiated a charge process has been previously requested a charge authorisation
// by the eMSP and they agree on the parameters n of the request
// Moreover, each commited charge authorisation by an eMSP corresponds to a unique
// request by an EV
lemma auth_injective_agreement_charge:
"
All Iss pke n #i .
	// For all commited charge authorisations by an eMSP for an EV (identified by its public endorsement key pke)
	(
		CommitEMSP( Iss, pke, n ) @ i 
	==> // Implies that the EV has been previously requested a charge authorisation by the same eMSP with the same parameters n
		(
			(
				(Ex TPM Host #j . 
					(
						RunningEV_Auth( TPM, Host, pke, Iss, n ) @ j
						& (#j<#i) 
						& // And each commited charge authorisation corresponds to a unique charge authorisation request
						( not(
							Ex Iss2 Host2 #i2 . ( CommitEMSP( Iss2, Host2, n) @ i2 & not(#i2=#i) )
							)
						)
					)
				)
			)
			|
			// or there has been a key reveal of the entities involved in the Commit
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)
"


// **************************** SR4 Charge Data Authenticity ************************************
// If the eMSP accepts charge data, then the EV that apparently
// signed the charge data has been previously active in the protocol
lemma auth_aliveness_charge_data:
"
All Iss pke n1 #i .
   // For all commited charge data receptions by an eMSP for an EV (identified by its public endorsement key pke)
	(
		CommitEMSP_Data( Iss, pke, n1 ) @ i 

	==> // Implies that the EV has been previously active in the protocol
       
		(	(Ex TPM Host #k . AliveEV(TPM, Host, pke) @ k)
			|
			// or there has been a key reveal of the entities involved in the Commit 
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)

"

// If the eMSP accepts charge data, then the EV that apparently
// signed the charge data has previously signed some charge data for this eMSP
lemma auth_weak_agreement_charge_data:
"
All Iss pke n1 #i .
	// For all commited charge data receptions by an eMSP for an EV (identified by its public endorsement key pke)
	(
		CommitEMSP_Data( Iss, pke, n1 ) @ i 
	==> // Implies that the EV previously signed charge data for this eMSP
		(
			(Ex TPM Host n2 #j . RunningEV_Data( TPM, Host, pke, Iss, n2 ) @ j) 
			|
			// or there has been a key reveal of the entities involved in the Commit
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)
"

// If the eMSP accepts charge data, then the EV that apparently
// signed the charge data has previously signed this charge data for this eMSP
lemma auth_non_injective_agreement_charge_data:
"
All Iss pke n #i .
	// For all commited charge data receptions by an eMSP for an EV (identified by its public endorsement key pke)
	(
		CommitEMSP_Data( Iss, pke, n ) @ i 
	==> // Implies that the EV previously send a signed charge data message with the same content as received by the eMSP
		(
			(Ex TPM Host #j . RunningEV_Data( TPM, Host, pke, Iss, n ) @ j) 
			|
			// or there has been a key reveal of the entities involved in the Commit
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)
"

// If the eMSP accepts charge data, then the EV that apparently
// signed the charge data has previously signed this charge data for this eMSP
// Moreover, each commited charge data set by an eMSP corresponds to a unique
// protocol run of the EV
lemma auth_injective_agreement_charge_data:
"
All Iss pke n #i .
	// For all commited charge data receptions by an eMSP for an EV (identified by its public endorsement key pke)
	(
		CommitEMSP_Data( Iss, pke, n ) @ i 
		==> // Implies that the EV previously send a signed charge data message with the same content as received by the eMSP
		(
			(
				(Ex TPM Host #j . 
					(
						RunningEV_Data( TPM, Host, pke, Iss, n ) @ j
						& 
						(#j<#i) 
						&
						// And each commited charge data set corresponds to a unique protocol run of the EV
						( not(
							Ex Iss2 Host2 #i2 . ( CommitEMSP_Data( Iss2, Host2, n) @ i2 & not(#i2=#i) )
							)
						)
					)
				)
			)
			|
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)
"
// ********************************* Unforgeability *****************************************
lemma SP3_Unforgeability_Off [heuristic=o]:
// Informal description:
// An adversary, who is in the possession of a set of Platforms’ secret keys and associated credentials,
// finds it hard to forge a valid message for a secret key and credential, which is not in that set.
// We restate this as follows: The only way a valid signature  using the secret key f 
// (and hence the associcated credentials) was not created by the platform is if its key or 
// set of credentials was leaked.
"
  All TPM Host pke bsn f sigma #t01 #t02 .
  
  //Assume that a platform's TPM created a secret DAA key,f
  DeriveDAAKey(TPM, Host, pke, f) @ t01
		&
  // and we have a valid deanonymised signature which used this secret f
  VerifiedCertificateDeAnonymised(bsn, sigma, f) @ t02
  &
  //the platform's keys were not revealed
  not ( Ex Event #r1 . KeyReveal(Event, TPM ) @ r1)
  &
  not ( Ex Event #r2 . KeyReveal(Event, Host ) @ r2)
  &
  not ( Ex Event #r3 . KeyReveal(Event, pke ) @ r3)
  &
  //and neither were the issuer's keys leaked
  not ( Ex Iss #ir . KeyReveal('Issuer_KeyReveal', Iss ) @ ir)
  ==>
  //then the platform must have sent out the message
  (Ex #t03 . Host_Sends_Certified_Q_K(TPM, Host, pke, sigma) @ t03)

"


//------------------
/*
  test_auth_non_injective_agreement_CP_sessKey (all-traces): verified (39 steps)
  test_auth_non_injective_agreement_CP (all-traces): verified (34 steps)
  test_auth_injective_agreement_CP (all-traces): verified (90 steps)
  test_test1 (all-traces): verified (38 steps)
  test_test2 (all-traces): verified (74 steps)
  test_test (all-traces): verified (82 steps)
  test_new_test_CP_sessKey (all-traces): verified (42 steps)
  test_new_test2 (all-traces): verified (35 steps)
  test_new_auth_non_injective_agreement_CP_data (all-traces): verified (41 steps)
  test_new_auth_injective_agreement_CP_data (all-traces): verified (43 steps)

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

real	4m3,337s
user	21m27,048s
sys	5m8,335s
*/

lemma test_auth_non_injective_agreement_CP_sessKey [heuristic=o]:
"
All CP g n  #i .
	(
		(
			CommitCP( CP, pk(g), n ) @ i 
		)
		==>
		(
			// Implies there exists a running issuer on the same term
			(Ex  TPM Host #j . DeriveSessionKey( TPM, Host, g ) @ j)
			|
			(Ex  sigma f #j #kr . 
				VerifiedCertificate2( CP, sigma, pk(g), f ) @ j 
				& KeyReveal('TPM_DAAReveal_f', f) @ kr) 
			|
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)
"

lemma test_auth_non_injective_agreement_CP:
"
All CP g n  TPM Host #i #i2 .
	(
		(
			CommitCP( CP, pk(g), n ) @ i 
			&
			DeriveSessionKey(TPM, Host, g) @ i2
		)
		==>
		(
			// Implies there exists a running issuer on the same term
			(Ex  #j . RunningEV_Sign2( TPM, Host, CP, n ) @ j) 
			|
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
			|
			(Ex RevealEvent #kr . KeyReveal(RevealEvent, TPM) @ kr)
		)
	)
"


lemma test_auth_injective_agreement_CP:
"
All CP g n TPM Host #i #i2  .
	(
		(
			CommitCP( CP, pk(g), n ) @ i 
			&
			DeriveSessionKey(TPM, Host, g) @ i2
		)
		==>
		(
			// Implies there exists a running issuer on the same term
			(
				Ex #j . RunningEV_Sign2( TPM, Host, CP, n ) @ j
				& 
				(#j<#i) 
				&
				// And each commited JOIN session corresponds to a unique issuer run
				( not(
					Ex CP2 g2 #i3 . ( CommitCP( CP2, pk(g2), n) @ i3 & not(#i3=#i) )
					)
				)
			) 
			|
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
			|
			(Ex RevealEvent #kr . KeyReveal(RevealEvent, TPM) @ kr)
		)
	)
"


//New:
/*
  test_new_test_CP_sessKey (all-traces): verified (42 steps)
  test_new_test2 (all-traces): verified (35 steps)
  test_new_auth_non_injective_agreement_CP_data (all-traces): verified (41 steps)
  test_new_auth_injective_agreement_CP_data (all-traces): verified (43 steps)
*/

lemma test_new_test_CP_sessKey [heuristic=o]:
"
All CP g sk_emaid  #i .
	(
		(
			CP_DataRec2( CP, pk(g), sk_emaid ) @ i 
		)
		==>
		(
			// Implies there exists a running issuer on the same term
			(Ex  TPM Host #j . DeriveSessionKey( TPM, Host, g ) @ j)
			|
			(Ex  sigma f #j #kr . 
				VerifiedCertificate2( CP, sigma, pk(g), f ) @ j 
				& KeyReveal('TPM_DAAReveal_f', f) @ kr) 
			|
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)
"

lemma test_key_tpm_binding_test2 [heuristic=o]:
"
All CP g sk_emaid TPM Host #i #i2  .
   // For all commited JOIN sessions running between a platform and issuer on the term(s) n 
	(
			CP_DataRec2( CP, pk(g), sk_emaid ) @ i 
			&
			DeriveSessionKey(TPM, Host, g) @ i2

	==> // Implies that an issuer has previously been involved in a protocol run 
       
		(	(Ex TPM Host #k2 . 
				EMAIDkey_Imported2(TPM, Host, sk_emaid) @k2)
			|
			// or there has been a key reveal of the entities involved in the Commit 
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
			|
			(Ex RevealEvent #kr . KeyReveal(RevealEvent, TPM) @ kr)
		)
	)

"


lemma test_new_auth_non_injective_agreement_CP_data [heuristic=o]:
"
All CP g dataTBS TPM Host #i #i2  .
	(
		(
			CP_DataRec3(CP, pk(g), dataTBS) @ i 
			&
			DeriveSessionKey(TPM, Host, g) @ i2
		)
		==>
		(
			// Implies there exists a running issuer on the same term
			(
				Ex #j . RunningEV_Data3( TPM, Host, CP, dataTBS ) @ j
				& 
				(#j<#i) 
			) 
			|
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
			|
			(Ex RevealEvent #kr . KeyReveal(RevealEvent, TPM) @ kr)
		)
	)
"

lemma test_new_auth_injective_agreement_CP_data [heuristic=o]:
"
All CP g dataTBS TPM Host #i #i2  .
	(
		(
			CP_DataRec3(CP, pk(g), dataTBS) @ i 
			&
			DeriveSessionKey(TPM, Host, g) @ i2
		)
		==>
		(
			// Implies there exists a running issuer on the same term
			(
				Ex #j . RunningEV_Data3( TPM, Host, CP, dataTBS ) @ j
				& 
				(#j<#i) 
				&
				// And each commited JOIN session corresponds to a unique issuer run
				( not(
					Ex CP2 g2 #i3 . ( CP_DataRec3( CP2, pk(g2), dataTBS) @ i3 & not(#i3=#i) )
					)
				)
			) 
			|
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
			|
			(Ex RevealEvent #kr . KeyReveal(RevealEvent, TPM) @ kr)
		)
	)
"


lemma test_auth_injective_agreement_CP_test2 [heuristic=o]:
"
All CP Iss tM_auth g TPM Host #i #i2 .
	(
		(
			CommitCP3( CP, Iss, tM_auth, pk(g)) @ i 
			&
			DeriveSessionKey(TPM, Host, g) @ i2
		)
		==>
		(
			// Implies there exists a running issuer on the same term
			(
				Ex pke #j . EMSP_Offline_Calc2(Iss, CP, pke, tM_auth) @ j
				& 
				(#j<#i) 
				&
				// And each commited JOIN session corresponds to a unique issuer run
				( not(
					Ex CP2 Iss2 g2 #i3 . ( CommitCP3( CP2, Iss2, tM_auth, pk(g2)) @ i3 & not(#i3=#i) 
						&
						not(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i3))
					)
				)
			) 
			|
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
			|
			(Ex RevealEvent #kr . KeyReveal(RevealEvent, TPM) @ kr)
		)
	)
"


//--------------------


/*
  test1 (all-traces): verified (2560 steps)
==============================================================================
real	68m15,750s
user	164m30,666s
sys	114m23,677s


  test2 (all-traces): verified (1285 steps)
==============================================================================
real	25m38,519s
user	67m8,266s
sys	42m21,408s


  test (all-traces): verified (115 steps)
==============================================================================
real	3m18,929s
user	14m9,277s
sys	3m55,545s

*/


lemma test_test1[reuse, heuristic=o]:
"
All CP g sk_emaid #i .
   // For all commited JOIN sessions running between a platform and issuer on the term(s) n 
	(
		CP_DataRec2(CP, pk(g), sk_emaid) @ i 

	==> // Implies that an issuer has previously been involved in a protocol run 
       
		(	(Ex TPM Host #k . 
				DeriveSessionKey(TPM, Host, g) @ k)
			|
			// or there has been a key reveal of the entities involved in the Commit 
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr)
		)
	)

"

lemma test_test2[reuse, hide_lemma=test1, heuristic=o]:
"
All CP g sk_emaid #i .
   // For all commited JOIN sessions running between a platform and issuer on the term(s) n 
	(
		CP_DataRec2(CP, pk(g), sk_emaid) @ i 

	==> // Implies that an issuer has previously been involved in a protocol run 
       
		(	(Ex TPM Host #k2 . 
				EMAIDkey_Imported2(TPM, Host, sk_emaid) @k2)
			|
			// or there has been a key reveal of the entities involved in the Commit 
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr)
		)
	)

"

lemma test_test:
"
All CP g sk_emaid #i .
   // For all commited JOIN sessions running between a platform and issuer on the term(s) n 
	(
		CP_DataRec2(CP, pk(g), sk_emaid) @ i 

	==> // Implies that an issuer has previously been involved in a protocol run 
       
		(	(Ex TPM Host #k #k2 . 
				DeriveSessionKey(TPM, Host, g) @ k
				&
				EMAIDkey_Imported2(TPM, Host, sk_emaid) @k2)
			|
			// or there has been a key reveal of the entities involved in the Commit 
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr)
		)
	)

"


end