theory DAA_PnC_Unlinkability_EV_Users_Locations
begin

/*
  Protocol:	DAA_PnC
  Properties:	PR4 - Unlinkability of EV Users and Locations

This Tamarin model is used to verify the privacy of the charge data authentication 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".

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 interactive daa_pnc_unlinkability_ev_users_locations.spthy\
 --quit-on-warning --diff --heuristic=O\
 --oraclename=ObsEquOracle_ev_users_locations.py +RTS -N8 -RTS

time tamarin-prover daa_pnc_unlinkability_ev_users_locations.spthy\
 --quit-on-warning --diff --heuristic=O\
 --oraclename=ObsEquOracle_ev_users_locations.py\
 --prove=diff_correctness +RTS -N8 -RTS


time tamarin-prover daa_pnc_unlinkability_ev_users_locations.spthy\
 --quit-on-warning --diff --heuristic=O\
 --oraclename=ObsEquOracle_ev_users_locations.py\
 --prove +RTS -N8 -RTS


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

analyzed: daa_pnc_unlinkability_ev_users_locations.spthy

  RHS :  diff_correctness (exists-trace): verified (14 steps)
  LHS :  diff_correctness (exists-trace): verified (14 steps)
  DiffLemma:  Observational_equivalence : verified (24945 steps)

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

real	82m35,001s
user	196m23,500s
sys	142m41,129s

*/

builtins:   asymmetric-encryption, symmetric-encryption, signing, hashing, multiset//, diffie-hellman//

functions:  MAC/2, KDF_EK/1,KDF_a/3, KDF_e/4, multp/2, plus/2, //len16/1, 
             H_SHA256/1, H_n_8/8, curlyK/1, RB/2, RD/2, PkX/2, PkY/2,
			  E_S/2, H_k_7/7, //TODO BSN/1,
			 H_n_2/2, H_k_2/2, Nonce/1, H_6/1
			 

// 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 event i_x #i #j . (OnlyOnce_ix(event, i_x) @ i & OnlyOnce_ix(event, i_x) @ j) ==> (#i=#j)" 

//the 'Issuer' should only be initialised once
restriction single_issuer_single_init:
	"All #i #j . (Issuer_Init() @ i & Issuer_Init() @ j) ==> (#i=#j)"


// Initialisation of the eMSP (the DAA Issuer) and the CCH (acting as CPS)
rule Issuer_Init:
		let 
			I=$Iss
			pkX=PkX(~x,'P2')
			pkY=PkY(~y,'P2')
		in
		[ Fr(~x)
			, Fr(~y)
			, Fr(~cps)
		]
		--[Issuer_Init()
			, OnlyOnce('Issuer_Init')]->
		[ !Ltk(I,~x, ~y)
			, !Pk(I, pkX,pkY)
			, Out(<pkX,pkY>)
			, Out(<~x,~y>)  //adversary (honest-but-curious eMSP) knows this data
			, !LtkCPS($CPS_I,~cps)
			, !PkCPS($CPS_I, pk(~cps))
			, Out(pk(~cps))
		]


/*
In this model, a EV authenticates two charge data records (CDRs), either from
two different CPs or the same CP.
The question is: Can the adversary decide whether the two CDRs originate from
charging sessions at the same or different CPs?
The identity data of the CPs is controlled by the adversary but the adversary
does not know which CDR is authenticated by the EV.
*/

// We generate a credential request for an EV
rule EV_Generate_Credential_Requests:
	let
		//inputs from Issuer PK
		pkX=PkX(x,'P2')
		pkY=PkY(y,'P2')
		
		//TPM1 details		
		e1=KDF_EK(~TPM_EK_Seed1)
		pke1=pk(e1)
		E_PD1=<'EK_public_data',pke1>
		PC_PD1=<'PC_public_data',pk(~pc1)>
		Q1=multp(~f1, 'P1')
		Q_PD1=<'DAA_public_data', Q1>

		m1=<pke1,pk(~pc1), Q_PD1, ~res_n1, 'join_Issuer_1'>
		signed_m1=H_SHA256(<m1, pk(cps), n1>) // In(n)
		sig_over_m1=sign(signed_m1,~pc1)

		m_out1=aenc(<sig_over_m1,m1>,pk(cps))


  in
        [	//Issuer details
			!Pk(I,pkX,pkY)		//the issuer's public key
			, !PkCPS(CPS_I, pk(cps))		//the issuer's public key

			, In(n1)
			//, In(n2)
			
			, Fr(~TPM_EK_Seed1)
			, Fr(~pc1)
			, Fr(~f1)
			, Fr(~res_n1)
      ]
    --[	Generate_TPM_Keys()
			, OnlyOnce( 'Generate_TPM_Keys' )
	]->	
	 [	 CertReq(m_out1, n1)
		, TPM_EK_QPD(<pke1, PC_PD1, Q_PD1>)
	 ]

// This rule combines the role of the CPS and eMSP in the credential issuing process
// First, the CPS decrypts and validates the request and then the eMSP generates the
// DAA credential for the request
rule Issuer_Issue_Credentials:
	let 
		//inputs
		Q=multp(f, 'P1')
		Q_PD=<'DAA_public_data', Q>
		m=<pke,pk(pc), Q_PD, res_n,'join_Issuer_1'>

		signed_m=H_SHA256(<m, pk(~cps), n>)
		m_in=aenc(<sig,m>,pk(~cps))

		//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_hat=aenc(~s_2_dh, pke) 
		s_2_temp=~s_2_dh

		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)
		curlyH=MAC(<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=aenc(~seed_3_dh, pke) 
		seed_3_temp=~seed_3_dh

		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, curlyK_2_hat, s_2_hat, C_hat, sk_DUP, res_n, 'Host_CompleteJoin'>
		sig_m=sign(H_SHA256(m_out),~cps)	
	in
     [ CertReq(m_in, n)
		, !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))
		, !LtkCPS(CPS_I, ~cps)
	 ] 
	 --[ Eq(verify(sig,signed_m,pk(pc)), true)	
	 	, CreateRes()
	 	, CreateResSig(sig_m)
		, OnlyOnce('Issuer_Verify_Challenge')
		]->
	 [ CertRes(m_in, n, m_out, sig_m)
		, Out(<sk_SENSITIVE, <A,B,C,D,u,j>, m>) //adversary (honest-but-curious eMSP) knows this data
	 ]	

// The CPS receives the credential responses from the eMSP
// The CPS then signs the response, forwards it
// to the EV and outputs the public data to the adversary
rule Cert_Res:
	let
		m1=<pke1,pk(~pc1), Q_PD1, res_n1, 'join_Issuer_1'>
		m_in1=aenc(<sig_over_m1,m1>,pk(cps))

		sk_DUP1=<sk_PD1, sk_SENSITIVE_hmac1, sk_SENSITIVE_enc1, seed_3_enc1>
		m_out1=<EMSP_Cert1, curlyH1, curlyK_2_hat1, s_2_hat1, C_hat1, sk_DUP1, res_n1, 'Host_CompleteJoin'>
		sig_m1=sign(H_SHA256(m_out1),cps)
	in
     [ 
		CertRes(m_in1, n1, m_out1, sig_m1)
		, TPM_EK_QPD(<pke1, PC_PD1, Q_PD1>)
		, !PkCPS(CPS_I,pk(cps))
	] 
	 --[ 
		Eq(verify(sig_m1,H_SHA256(m_out1),pk(cps)), true)	
		, Cert_Res()
		, OnlyOnce('Cert_Res')
		]->
	 [
	 	!EV_Start_Auth( <m_in1, n1, m_out1, sig_m1, <pke1, PC_PD1, Q_PD1>> )
		, Out(<'FirstTPM', pke1, PC_PD1, Q_PD1, sk_PD1>) // TODO no session key Qk_PD1
	 ]	
// There are two different charge points CP1 and CP2. The EV either charges once at CP1 and once at CP2
// or twice at CP2 (diff property). The question is if the eMSP can distinguish whether the two CDRs
// come from charging sessions at the same or different CPs.
rule Two_CP:
	let
		CP_DIFF=diff( <'req1', $CP1, sid1, <nonce1, nonce_ix1>, <'charge_data', dataID1>>,
		 			  <'req2', $CP2, sid2, <nonce2, nonce_ix2>, <'charge_data', dataID2>>)
		CP_Link=<'req3', $CP2, sid3, <nonce3, nonce_ix3>, <'charge_data', dataID3>>
	in
     [  In(<$CP1, sid1, <nonce1, not_nonce_ix1>, <'charge_data', not_dataID1>>)
		, In(<$CP2, sid2, <nonce2, not_nonce_ix2>, <'charge_data', not_dataID2>>)
		//shuffle the values that may be adversary controlled (by CP) but cannot be used by CCH/eMSP to distinguish charge locations
		, In(<<nonce_ix1 + nonce_ix2>, <dataID1 + dataID2>>)
		//Second time at CP2 to check for linkability
		, In(<$CP2, sid3, <nonce3, nonce_ix3>, <'charge_data', dataID3>>)
	 ] 
	 --[ Two_CP()
		, OnlyOnce('Two_CP')
		]->
	 [ CP_In(CP_DIFF)
	 , CP_In(CP_Link)  ]	


// The EV obtains a credential response as well as charge data (this rule is executed twice,
// once either for charge data send by CP1 or CP2 (diff property) and once for charge data from CP2).
// The EV then uses the obtained credential to authenticate the charge data and sends the
// authenticated data back to the adversary
rule EV_Auth:
	let
		CP_DIFF=<req, $CP, sid, <nonce, nonce_ix>, <'charge_data', dataID>>

		e=KDF_EK(~TPM_EK_Seed)
		//pke1='g'^e1
		pke=pk(e)
		E_PD=<'EK_public_data',pke>
		PC_PD=<'PC_public_data',pk(pc)>
		Q=multp(~f, 'P1')
		Q_PD=<'DAA_public_data', Q>

		i_x=h(<~i_x_t, pke>)

		m=<pke,pk(pc), Q_PD, res_n, 'join_Issuer_1'>
		signed_m=H_SHA256(<m, pk(cps), n>) 
		m_in=aenc(<sig_over_m,m>,pk(cps))

		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)	

		curlyK_2_hat=senc(curlyK_2,k_e)
		C_hat=senc(<A,B,C,D,u,j>,curlyK_2)
		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>
		m_out=<EMSP_Cert, curlyH, curlyK_2_hat, s_2_hat, C_hat, sk_DUP, res_n, 'Host_CompleteJoin'>

		Auth=<m_in, n, m_out, sig_m, <pke, PC_PD, Q_PD>>

		//Host_Randomise_Credentials
		/*
		bsn='bottom'
		R=multp(~l,A)
		S=multp(~l,B)
		T=multp(~l,C)
		W=multp(~l,D)
		s_2_bar=bsn
		y_2=bsn

		//TPM2_Commit
		E=E_S(~r_cv1,S)*/

		//TPM_Create_Session_Key
		pkCCsess=pk(~g)
		/*
		Qk_PD=<'SessionKey_public_data', pkCCsess>
		Qk_n=<'SHA256',H_SHA256(Qk_PD)>
		Qk_SD=senc(~g,aes_key)

		//Host_Load_Qk_For_Ceritfication
		credData='CredentialData'
		c=H_k_7(credData,R,S,T,W,E, sid)*/
		m_buffer=<'00',i_x>

		//TPM2_Load_And_Certify
		/*N1=QName('SHA256',H_SHA256('root'))
		N2=QName('SHA256',H_SHA256(E_PD))
		N3=H_SHA256(<N1, N2>)
		Qk_QualName=H_SHA256(<N3, Qk_n>)*/
		/*
		curlyA=<'certificationData', Qk_n>//, Qk_n, Qk_QualName>
		credData='CredentialData'
		small_c=H_k_7(credData,R,S,T,W,E, sid)
		h1=H_k_2(small_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))*/

		//TPM2_HMAC1
		tM_id=MAC(m_buffer, sk_emaid)
		M_id=h(tM_id)

		//Host_Receive_Certified_Q_k
		//sigma_K=<Qk_PD, curlyA, bsn, R, S, T, W, h2, small_s, n_C>
		//auth_m1=<EMSP_Cert, M_id,  sigma_K, 'TPM_Certificate_Of_Q_K'>

		//Host_Auth
		m_buffer2=<'01',i_x>

		//TPM2_HMAC2
		M_auth=MAC(m_buffer2, sk_emaid)

		//Host_Auth2
		tM_auth=h(<M_auth, nonce_ix>)
		//authH=h(<$CP, nonce, tM_auth>) 

		//TPM2_Sign_SessionKey
		//sig_over_auth=sign(authH,~g)

		//Host_Auth3
		//auth_m2=<authH, sig_over_auth, ~i_x, tM_auth, 'AuthorizationReq'>

		// CP_Verify
		auth_m_emsp=<I, M_id, nonce_ix, tM_auth, pkCCsess, 'EMSP_Auth'>

		//EV_DataSign
		ev_h=h(<'EV_h',M_auth,pkCCsess>)
		dataTBS=h(<'charge_data', dataID, ev_h>)
		dataSig=sign(dataTBS,~g)

		//CP_DataRec
		data_m=<I, 'charge_data', dataID, dataSig>
	in
     [ 
	 	!EV_Start_Auth(Auth)
		, !PkCPS(CPS_I,pk(cps))
		//, Fr(~l)
		//, Fr(~r_cv1)
		, Fr(~g) 
		, In(~i_x_t) //In & onlyonce
		//, !CP_Init($CP)
		, CP_In(CP_DIFF)
		//, In(<$CP, sid>)
		, Fr(~rnd_n_C)		
	] 
	 --[ 
		Eq(verify(sig_m,H_SHA256(m_out),pk(cps)), true)
		, Eq(verify(sig_over_m,signed_m,pk(pc)), true)
		, EV_Auth(req)
		, OnlyOnce(<'EV_Auth', req>)
		, OnlyOnce_ix('EV_Auth', i_x)
		]->
	 [
		Out(<auth_m_emsp, data_m>)
	 ]	



lemma diff_correctness: exists-trace
"	Ex #t1 #t3 #t4 #t5 #t6 #t7 .
		Issuer_Init() @ t1
		& Generate_TPM_Keys() @ t3
		& CreateRes() @ t4
		& Cert_Res() @ t5
		& Two_CP() @ t6
		& ( 
			(Ex #k1 . (EV_Auth('req1') @k1) )
			|
			(Ex #k1 . (EV_Auth('req2') @k1) )
		  ) 
		& EV_Auth('req3') @ t7
		& #t1<#t3
		& #t3<#t4
		& #t4<#t5
		& #t5<#t6
		& #t6<#t7
		
		
		//restrict rules to only run once in a trace
		& (All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j)
"

end