daa_pnc_credential_installation.spthy

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

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

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

This model verifies the security requirement SR2: Secure Credential Installation

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


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

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

analyzed: join2_wCP2test3.spthy

  forwarded_credential_res_source (all-traces): verified (265 steps)
  secrecy_of_cps_private_key (all-traces): verified (3 steps)
  secrecy_of_pke (all-traces): verified (6 steps)
  integrity_of_forwarded_credential_res_m (all-traces): verified (166 steps)
  restricition_bind (all-traces): verified (4 steps)
  restriction_one_host_per_tpm (all-traces): verified (12 steps)
  restriction_one_tpm_per_host (all-traces): verified (10 steps)
  restricition_pke_comes_from_tpm (all-traces): verified (14 steps)
  correctness_verify_multiple_pkes (exists-trace): verified (70 steps)
  correctness_verify_multiple_pkes_diff_I (exists-trace): verified (69 steps)
  correctness_credential_req (exists-trace): verified (22 steps)
  correctness_credential_req_res_1 (exists-trace): verified (57 steps)
  correctness_credential_req_res_2 (exists-trace): verified (67 steps)
  auth_aliveness_issuer_very_weak (all-traces): verified (49 steps)
  auth_aliveness_issuer (all-traces): verified (49 steps)
  auth_aliveness_host (all-traces): verified (6 steps)
  auth_weak_agreement_host (all-traces): verified (63 steps)
  auth_non_injective_agreement_host_issuer (all-traces): verified (63 steps)
  auth_injective_agreement_host_issuer (all-traces): verified (205 steps)
  auth_non_injective_agreement_CPS_EV (all-traces): verified (32 steps)
  auth_injective_agreement_CPS_EV (all-traces): verified (48 steps)
  auth_secrecy_cre_ev (all-traces): verified (303 steps)
  auth_secrecy_cre_iss (all-traces): verified (116 steps)
  auth_secrecy_emaid_iss (all-traces): verified (36 steps)
  auth_secrecy_emaid_ev (all-traces): verified (123 steps)

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

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

*/

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

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

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

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

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

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

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


//each certificate installation response CertRes is only accepted once by a EV/Host
restriction only_once_certres: 
"All event #i #j . 
	(OnlyOnceCertRes(event) @ i & OnlyOnceCertRes(event) @ j) ==> (#i=#j)"


//Modification: removed restriction for single issuer initialisation
//each issuer should only be initialised once
restriction issuer_single_init:
	"All I #i #j . (Issuer_Init(I) @ i & Issuer_Init(I) @ j) ==> (#i=#j)"
	
//the certificate provisioning service (CPS) should only be initialized once 
restriction single_cps_single_init:
	"All CPS_I CPS_I2 #i #j . (CPS_Init(CPS_I) @ i & CPS_Init(CPS_I2) @ j) ==> (#i=#j)"
	
//each charge point (CP) should only be initialized once
restriction cp_single_init:
	"All CP #i #j . (CP_Init(CP) @ i & CP_Init(CP) @ j) ==> (#i=#j)"

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

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


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

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

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

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

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

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


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

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

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


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

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


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


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

// Modification: Added CPS set-up
rule CPS_Init:
		[Fr(~cps)]
		--[CPS_Init($CPS_I)
		   , CPS_Init2($CPS_I, ~cps)
		   , OnlyOnce('CPS_Init')]->
		[!LtkCPS($CPS_I,~cps)
		   , !PkCPS($CPS_I, pk(~cps))
		   , Out(pk(~cps))
		   , !CPS_Initialised($CPS_I)
		]

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


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


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

Modification: Removed need for the host to know the issuer before the join.
*/
rule TPM_INIT:
	let
	//!Assumption that the aes key is derived by a KDF_AES key derivation function
	aes_key=KDF_AES(~TPM_AES_Seed)
	in
		[Fr(~TPM_AES_Seed),
		 Fr(~TPM_EK_Seed)]
		--[TPM_Init($PS)
		   , OnlyOnce('TPM_INIT')]->
		[!TPM_AES_Key($PS, aes_key), 
		 TPM_EK_SEED($PS,~TPM_EK_Seed), 
		 TPM_Initialised($PS)]

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

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

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

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

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

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

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

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


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

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

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

Modification: Included the generation and encryption of the EV's CertReq
*/
rule Host_Store_DAA:
	let 
		Q=multp(~f, 'P1')
		Q_PD=<'DAA_public_data', Q>

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

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

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

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

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

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

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


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

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

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

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

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

//Issuer: verify the curlyK and the signature before issuing the proper credentials for the host/EV and sending them back to the CPS
//Modification: Changed to model new behavior of eMSP issuer, i.e., interaction with CPS and inclusion of EMSP_Cert.
rule Issuer_Issue_Credentials:
	let 
		//inputs
		pke='g'^e

		Q=multp(f, 'P1')
		Q_PD=<'DAA_public_data', Q>
		m=<pke,pk(pc), Q_PD, 'join_Issuer_1'>

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

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

		EMSP_Cert=<I,pkX,pkY>

		m_out=<EMSP_Cert, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, C_hat, sk_DUP, 'Host_CompleteJoin'>
	in
     [ In_S_B(CPS_I, I, < reqID, m, 'CPS_Fwd_Req'>)
		, !Pk(I,pkX,pkY)
		, !Ltk(I,~x,~y)
		, Fr(~r)
		, Fr(~l)
		, Fr(~s_2_dh)
		, Fr(~K_2)
		, Fr(~sk_emaid)
		, Fr(~seed_3_dh)
		, Fr(~obfuscationValue) // for import
		, !PkCPS(CPS_I,pk(~cps))
	 ] 
	 --[ Running(I, pke, <A, B, C, D>)
		, Alive(I)							//the issuer is "alive" in the protocol here
		, Honest ( I )
		, Honest ( pke )
		, Honest ( CPS_I )
		, Role ('Issuer')
		, IssuerReceivedKeys(I, pke, pk(pc), Q_PD)
		, Secret_EMAID(I, pke, ~sk_emaid)
		, Secret_Cred(I, pke, <A,B,C,D>)
		, Iss_s2(s_2, e)
		, Iss_s22(s_2, e, pke, <A,B,C,D>, curlyK_2, k_e)
		, Iss_s3(seed_3, e)
		, Iss_m(m_out)
		, OnlyOnce('Issuer_Verify_Challenge')
		]->
	 [Out_S_B(I, CPS_I, <reqID, m_out>) 
	 , !Issuer_EMAID_SK(I, ~sk_emaid)
	 ]	

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


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

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

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

		activateData=<Q_SD, Q_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat>
	in
	[ In(<sid, m, sig_m, 'CP_Fwd_Res'>)
	  	, !Host_State_05($PS, $AS, pke, pk(cps), CPS_I, sid,  CP, ~res_n)
	  	, !Host_Store_DAAKey($PS, $AS, pke, Q_PD, Q_SD)
		, !PkCPS(CPS_I, pk(cps)) // from Charge Station but authentic due to certificate
	 ]
	--[ Eq(verify(sig_m,m,pk(cps)), true)
		, Passthrough_ActivateCred2($PS, $AS)
		, Passthrough_ActivateCred2_sid($PS, $AS, sid)
		, Passthrough_m($PS, $AS, m, pk(cps))
		, OnlyOnceCertRes(<$PS, $AS, Q_PD, I, sid>)
		, OnlyOnce('Host_Passthrough_2')
	  ]->
	[ Out_S($AS,$PS,< sk_DUP, 'TPM2_Import'>)
	, Out_S($AS,$PS,< Q_SD, Q_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, 'TPM2_ActivateCredentials_2'>)
	, Host_State_06($PS, $AS,  pke, Q_PD, C_hat, activateData,  CP,  EMSP_Cert, CPS_I, sk_PD)
	]
//====================================================
// Contract Credential Installation Response Handling
//====================================================
//The TPM decrypts the EMAID secret key and returns it to the host/EV
//Modification: Added TPM2_Import
rule TPM2_Import:
	let
		//sk_unique=H_SHA256(<obfuscationValue, sk_emaid>)
		//sk_PD=<'SK_EMAID_public_data', sk_unique>
		sk_SENSITIVE=<'TPM_ALG_KEYEDHASH', 'NULL', obfuscationValue, sk_emaid>
		sk_SENSITIVE_enc=senc(sk_SENSITIVE,sk_k_e)
		sk_DUP=<sk_PD, sk_SENSITIVE_hmac, sk_SENSITIVE_enc, seed_3_enc>

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

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

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

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

		sk_SENSITIVE=<'TPM_ALG_KEYEDHASH', 'NULL', obfuscationValue, sk_emaid>
		sk_SD=senc(sk_SENSITIVE,aes_key)
		
		//inputs from the issuer
		EMSP_Cert=<I,pkX,pkY>
		//pkX=PkX(x,'P2')
		//pkY=PkY(y,'P2')
		
		//input from Host_State
		Q=multp(~f, 'P1')
		Q_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, Q_PD, C_hat, activateData,  CP,  EMSP_Cert, CPS_I, sk_PD)
		//, Host_State_07($PS, $AS,  pke, Q_PD, C_hat, sk_PD, sk_SD,  CP,  EMSP_Cert, CPS_I)
	 	, !PkCPS(CPS_I, pk(cps))
	]
	 --[ 
	     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> )
		, Secret_EMAID_EV(pke, I, sk_emaid )
		, Honest ( $PS )
		, Honest ( $AS )
		, Honest ( pke )
		, Honest ( I )
		, Honest ( CPS_I )
		, Honest ( CP )
		, Host_C_hat2(C_hat, pk(cps))
		, OnlyOnce('Host_JoinComplete')
		]->
	 [ 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
//=============================================================	 


//======================================================================================
// 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 forwarded_credential_res_source [sources]:
// Information contained in a credential response forwarded by a CP is either generated as intended by the protocol
// or already known to the adversary
"

(All sid m sig res_n #i .
   // For each credential response forwarded to the EV by the CP
	(
		CP_m2(sid, m, sig, res_n) @ i
		==>
		(
			(Ex  CP n  #j1 #j4 . // CPS_I #j3
				// The CP has send a nonce (timestamp) to the EV previously
				CP_Nonce(CP, n, sid) @ j1 & j1<i // < j3
				& ( 
					// and the nonce contained in the response was generated as part of a credential request by the hos
					 (Ex #j2 . Store_DAA_resn(res_n) @ #j2 & #j2<#i)
					 // or was already known to the adversary
					 | (Ex  #kr . KU(res_n) @ kr & #kr<#i)
				  )
				// and the message of the credential response was previously send by an issuer
				& Iss_m(m) @ j4 & j4<i
			)
			// or the adversary already knew the complete credential response before it was forwarded by the CP
			| (Ex  #kr . KU(<sid, m, sig, res_n>) @ kr & kr<i)
		)
	)
)
"

lemma secrecy_of_cps_private_key [reuse]: 
"
// The adversary can only learn the CPS's secret key via the CPS_KeyReveal rule
All CPS_I cps #i #i2 .
	(
		CPS_Init2(CPS_I, cps) @ i & KU(cps) @ i2
		==>
		(
			(Ex  #kr . KeyReveal('CPS_KeyReveal', CPS_I) @ kr & i<kr & kr<i2)
		)
	)
"


lemma secrecy_of_pke [reuse]: //maybe
"
// The adversary can only learn the public endorsement key of a tpm via the TPM_EKReveal rule
All e pke #i #i2 .
	(
		TPM2_EK_Created2( e, pke) @ i & KU(e) @ i2
		==>
		(
			(Ex  #kr . KeyReveal('TPM_EKReveal_pke', pke) @ kr & i<kr)
		)
	)
"


lemma integrity_of_forwarded_credential_res_m [reuse]:
"
// The adversary cannot manipulate or forge credential response messages send by the CP to the host/EV
// without having compromised the CPS's private key
All TPM Host m cps #i .
	(
		Passthrough_m(TPM, Host, m, pk(cps)) @ i
		==>
		(
			(Ex  #j . CP_m(m) @ j & j<i)
			| (Ex  #j . KU(cps) @ 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 restricition_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) 
	"

//======================================================================================
// In the following section we look at the security properties required for 
// the credential installation process
//======================================================================================


// Correctness of the credential request
lemma correctness_credential_req: exists-trace
" Ex TPM Host I CPS_I CP pke sigReq //n
					#t01 #t01_2 #t01_3 #t02 #t03 #t04 #t05 #t06 #t07 #t08 #t09
					#t10 #t11 #t12
.
					
//we initiated at least one entity for each protocol role
	Issuer_Init(I) @ t01 
	& CPS_Init(CPS_I) @ t01_2
	& CP_Init(CP) @ t01_3
	& 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

	//signed a credential request 
	& TPM2_Sign(TPM, Host) @ t11

	//send the credential request to the CP
	& RunningEV(pke, CPS_I, sigReq) @ t12
	
	// With the correct temporal ordering
	& t01<t02 //Issuer gets created before Host
	& t01_2<t02 //CPS gets created before Host
	& t01_3<t02 //CP 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<t11
	& t11<t12

  //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 credential request and response until received by host
lemma correctness_credential_req_res_1: exists-trace
" Ex TPM Host I CPS_I CP pke pcpd qpd sigReq sid n
					#t01 #t01_2 #t01_3 #t02 #t03 #t04 #t05 
					#t06 #t07 #t08 #t09 #t09_2
					#t10 #t11 #t12 #t12_2 #t13 
					#t14 #t15 #t16 #t17
.		
	//we initiated at least one entity for each protocol role
	Issuer_Init(I) @ t01 
	& CPS_Init(CPS_I) @ t01_2
	& CP_Init(CP) @ t01_3
	& 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
	
	//sent a nonce (timestamp) from the CP to the host
	& CP_Nonce(CP, n, sid) @ t09_2
	
	//stored the DAA key with the host
	& Store_DAA_N(TPM, Host, n, sid) @ t10

	//signed a credential request 
	& TPM2_Sign(TPM, Host) @ t11

	//send the credential request to the CP
	& RunningEV(pke, CPS_I, sigReq) @ t12

	//forwarded the request from the CP to the CPS
	& CP_Fwd_Credential_Request(CP, CPS_I, n) @ t12_2
	
	//received and verified the request as the CPS
	& CPSReceivedReq(CPS_I, pke, pcpd, qpd) @ t13

	//recieved and answered the credential request as the issuer
	& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t14
	
	//received the issuers response as the CPS and forwarded it to the CP
	& CPSReceivedRes(CPS_I)	@ t15

	//received the credential response as the CP and forwarded it to the host
	& CP_Fwd_Credential_Res(CP, CPS_I, sid)	@ t16

	// received the response by the host
	& Passthrough_ActivateCred2_sid(TPM, Host, sid) @ t17

	// With the correct temporal ordering
	& t01<t02 //Issuer gets created before Host
	& t01_2<t02 //CPS gets created before Host
	& t01_3<t02 //CP 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_2<t10
	& t09<t10
	& t10<t11
	& t11<t12
	& t12_2<t13
	& t12<t13
	& t13<t14
	& t14<t15
	& t15<t16
	& t16<t17

  //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 complete credential installation process
lemma correctness_credential_req_res_2: exists-trace
" Ex TPM Host I CPS_I CP pke pcpd qpd sigReq sid n
					#t01 #t01_2 #t01_3 #t02 #t03 #t04 #t05 
					#t06 #t07 #t08 #t09 #t09_2
					#t10 #t11 #t12 #t12_2 #t13 
					#t14 #t15 #t16 #t17
					#t18 //#t19 
					#t20 #t21
.
					
	//we initiated at least one entity for each protocol role
	Issuer_Init(I) @ t01 
	& CPS_Init(CPS_I) @ t01_2
	& CP_Init(CP) @ t01_3
	& 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	

	//sent a nonce (timestamp) from the CP to the host
	& CP_Nonce(CP, n, sid) @ t09_2
	
	//stored the DAA key with the host
	& Store_DAA_N(TPM, Host, n, sid) @ t10

	//signed a credential request 
	& TPM2_Sign(TPM, Host) @ t11

	//send the credential request to the CP
	& RunningEV(pke, CPS_I, sigReq) @ t12

	//forwarded the request from the CP to the CPS
	& CP_Fwd_Credential_Request(CP, CPS_I, n) @ t12_2
	
	//received and verified the request as the CPS
	& CPSReceivedReq(CPS_I, pke, pcpd, qpd) @ t13

	//recieved and answered the credential request as the issuer
	& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t14
	
	//received the issuers response as the CPS and forwarded it to the CP
	& CPSReceivedRes(CPS_I)	@ t15

	//received the credential response as the CP and forwarded it to the host
	& CP_Fwd_Credential_Res(CP, CPS_I, sid)	@ t16

	// received the response by the host
	& Passthrough_ActivateCred2_sid(TPM, Host, sid) @ t17
	
	// imported the EMAID key into the TPM and returned it to the host
	& EMAIDkey_Imported(TPM, Host) @ t18
	
	//decrypted the DAA credentials in the TPM and returned them to the host
	& CurlyK2_recomputed(TPM, Host) @ t20

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

	// With the correct temporal ordering
	& t01<t02 //Issuer gets created before Host
	& t01_2<t02 //CPS gets created before Host
	& t01_3<t02 //CP 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_2<t10
	& t09<t10
	& t10<t11
	& t11<t12
	& t12_2<t13
	& t12<t13
	& t13<t14
	& t14<t15
	& t15<t16
	& t16<t17
	& t17<t18
	& t18<t20
	& t20<t21

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


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

// This lemma shows that the CPS is in a non-injective agreement with the Host on
// a credential request if, whenever the CPS receives a credential request, apparently from the Host, 
// then the Host has previously send a credential request to the CPS, and
//the two principals agreed on the terms n
lemma auth_non_injective_agreement_CPS_EV: //requires signed_m=<m, pk(~cps)> for inclusion of CPS' public key
"
All CPS pke n #i .
	(
		(
			// For all credential requests received by the CPS, apparently from the platform identified by pke and with the term(s) n 
			CommitCPS( CPS, pke, n )  @ i 
		)
		==>
		(
			// Implies there exists a running platform that send a credential request with the same term(s)
			(Ex #j . RunningEV( pke, CPS, n )  @ j) 
			|
			// or there has been a key reveal of one of the involved entities
			(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i)
		)
	)
"
// This lemma shows that the CPS is in an injective agreement with the Host on
// a credential request if, whenever the CPS receives a credential request, apparently from the Host, 
// then the Host has previously send a credential request to the CPS, 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_CPS_EV:
"
All CPS pke n #i .
	(
		(
		// For all credential requests received by the CPS, apparently from the platform identified by pke and with the term(s) n 
			CommitCPS( CPS, pke, n ) @ i 
		)
		==>
		(
			(
				(Ex #j . 
					(
					// Implies there exists a running platform that send a credential request with the same term(s)
						RunningEV( pke, CPS, n ) @ j
						& 
						(#j<#i) 
						&
						// and each receive event corresponds to a unique credential request send by the host
						( not(
							Ex CPS2 pke2 #i2 . ( CommitCPS( CPS2, pke2, n) @ i2 & not(#i2=#i) )
							)
						)
					)
				)
			)
			|
			// or there has been a key reveal of one of the involved entities
			(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_ev:
"
  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)
"
lemma auth_secrecy_cre_iss:
"
  All Iss pke cred #i. 
    // somebody claims to have setup a secret credential, 
    Secret_Cred( Iss, pke, 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)
"

// EMAID secrecy from the perspective of both the Issuer and the TPM/Host.
lemma auth_secrecy_emaid_iss:
"
  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)
"
lemma auth_secrecy_emaid_ev:
"
  All  Iss pke sk_emaid #i. 
    // somebody claims to have setup a shared secret, 
    Secret_EMAID_EV( pke, Iss, 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)
"

end