daa_pnc_unlinkability_charge_authorisation.spthy

theory DAA_PnC_Unlinkability_Charge_Authorization
begin

/*
  Protocol:	DAA_PnC
  Properties:	PR2 - Unlinkable Charge Authorization

This Tamarin model is used to verify the privacy of the charge authorisation 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_charge_authorisation.spthy\
 --quit-on-warning --diff --heuristic=O\
 --oraclename=ObsEquOracle_charge_authorisation.py +RTS -N8 -RTS

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


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

analyzed: daa_pnc_unlinkability_charge_authorisation.spthy

  RHS :  diff_correctness (exists-trace): verified (11 steps)
  LHS :  diff_correctness (exists-trace): verified (11 steps)
  DiffLemma:  Observational_equivalence : verified (40087 steps)

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

real	333m58,717s
user	852m10,529s
sys	531m58,938s

*/

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

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, //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)
// we do not allow key reveals for the issuer
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>)
			, !LtkCPS($CPS_I,~cps)
			, !PkCPS($CPS_I, pk(~cps))
			, Out(pk(~cps))
		]

/*
In this model, we install DAA credentials on two EVs. One with TPM1 and one with TPM2. We then generate
two charge authorization requests. One either for TPM1 or TPM2 (diff property) and one for TPM2.
The question is: Can the adversary decide whether the two generated charge authorisation value pairs <auth_m1, auth_m2>
have been generated by the same or different TPMs?
*/

// We generate two credential requests, one for TPM1 and one for TPM2
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))

		//TPM2 details		
		e2=KDF_EK(~TPM_EK_Seed2)
		pke2=pk(e2)
		E_PD2=<'EK_public_data',pke2>
		PC_PD2=<'PC_public_data',pk(~pc2)>
		Q2=multp(~f2, 'P1')
		Q_PD2=<'DAA_public_data', Q2>

		m2=<pke2,pk(~pc2), Q_PD2, ~res_n2, 'join_Issuer_1'>
		signed_m2=H_SHA256(<m2, pk(cps), n2>) // In(n)
		sig_over_m2=sign(signed_m2,~pc2)

		m_out2=aenc(<sig_over_m2,m2>,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)

			, Fr(~TPM_EK_Seed2)
			, Fr(~pc2)
			, Fr(~f2)
			, Fr(~res_n2)
      ]
    --[	Generate_TPM_Keys()
			, OnlyOnce( 'Generate_TPM_Keys' )
	]->	
	 [
		CertReq('req1', m_out1, n1)
		, CertReq('req2', m_out2, n2)
		, !TPM_EK_QPD('req1', <pke1, PC_PD1, Q_PD1>)
		, !TPM_EK_QPD('req2', <pke2, PC_PD2, Q_PD2>) 
	 ]

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

		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(req, 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(req)
	 	, CreateResSig(sig_m)
		, OnlyOnce(<'Issuer_Verify_Challenge', req>)
		]->
	 [ !CertRes(req, m_in, n, m_out, sig_m)
	 ]	

// The CPS receives two credential responses from the eMSP
// one from TPM1 and one from TPM2
// The CPS then signs the two responses and forwards one of them
// to the EV (diff property) together with an additional one of TPM2
// and outputs the public data to the adversary
rule Two_Cert_Res:
	let
		//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>
		sk_unique1=H_SHA256(<~obfuscationValue1, ~sk_emaid1>)
		sk_PD1=<'SK_EMAID_public_data', sk_unique1>

		//TPM2 details		
		e2=KDF_EK(~TPM_EK_Seed2)
		pke2=pk(e2)
		E_PD2=<'EK_public_data',pke2>
		PC_PD2=<'PC_public_data',pk(~pc2)>
		Q2=multp(~f2, 'P1')
		Q_PD2=<'DAA_public_data', Q2>
		sk_unique2=H_SHA256(<~obfuscationValue2, ~sk_emaid2>)
		sk_PD2=<'SK_EMAID_public_data', sk_unique2>


		m1=<pke1,pk(~pc1), Q_PD1, res_n1, 'join_Issuer_1'>
		m_in1=aenc(<sig_over_m1,m1>,pk(cps))

		m2=<pke2,pk(~pc2), Q_PD2, res_n2, 'join_Issuer_1'>
		m_in2=aenc(<sig_over_m2,m2>,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)
		
		sk_DUP2=<sk_PD2, sk_SENSITIVE_hmac2, sk_SENSITIVE_enc2, seed_3_enc2>
		m_out2=<EMSP_Cert2, curlyH2, curlyK_2_hat2, s_2_hat2, C_hat2, sk_DUP2, res_n2, 'Host_CompleteJoin'>
		sig_m2=sign(H_SHA256(m_out2),cps)
		
		// Difference property: The adversary cannot distinguish whether the
		// charge authorisation request was generated with TPM1 or TPM2
		Auth_DIFF=diff( <'req1', m_in1, n1, m_out1, sig_m1, <pke1, PC_PD1, Q_PD1>>,
		 				<'req2', m_in2, n2, m_out2, sig_m2, <pke2, PC_PD2, Q_PD2>>)
	in
     [ 
		!CertRes('req1', m_in1, n1, m_out1, sig_m1)
		, !CertRes('req2', m_in2, n2, m_out2, sig_m2)
		, !TPM_EK_QPD('req1',<pke1, PC_PD1, Q_PD1>)
		, !TPM_EK_QPD('req2',<pke2, PC_PD2, Q_PD2>) 	
		, !PkCPS(CPS_I,pk(cps))
	] 
	 --[ 
		Eq(verify(sig_m1,H_SHA256(m_out1),pk(cps)), true)	
		, Eq(verify(sig_m2,H_SHA256(m_out2),pk(cps)), true)	
		, Two_Cert_Res()
		, OnlyOnce('Two_Cert_Res')
		]->
	 [
	 	EV_Start_Auth( Auth_DIFF )
	 	, EV_Start_Auth( <'req3', m_in2, n2, m_out2, sig_m2, <pke2, PC_PD2, Q_PD2>> ) 	
		, Out(<'FirstTPM', pke1, pk(~pc1), Q1, sk_PD1>) 
		, Out(<'SecondTPM', pke2, pk(~pc2), Q2, sk_PD2>)
	 ]	

// The EV obtains a credential response (the rule is executed twice, once either for TPM1 or TPM2 (diff property)
// and one for TPM2.) It verifies the credentials and outputs charge authrization values auth_m1 and auth_m2
// for both credentials
rule EV_Auth:
	let
		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_DIFF=<req, m_in, n, m_out, sig_m, <pke, PC_PD, Q_PD>>

		//Host_Randomise_Credentials
		//bsn=BSN('bottom')
		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
		Qk=pk(~g)
		Qk_PD=<'SessionKey_public_data', Qk>
		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, E, sigma_K, 'PaymentDetailsReq'>

		//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, tM_auth, 'AuthorizationReq'>
	in
     [ 
	 	EV_Start_Auth(Auth_DIFF)
		, !PkCPS(CPS_I,pk(cps))
		, Fr(~l)
		, Fr(~r_cv1)
		, Fr(~g) 
		, In(~i_x_t)
		, In(<$CP, sid, <nonce, nonce_ix>, <'charge_data', dataID>>)
		, 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_m1, auth_m2>)
	]	



lemma diff_correctness: exists-trace
"	Ex #t1 #t3 #t4 #t5 #t6 #t7 .
		Issuer_Init() @ t1
		& Generate_TPM_Keys() @ t3
		& CreateRes('req1') @ t4
		& CreateRes('req2') @ t5
		& Two_Cert_Res() @ 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
		
		//and we had no key reveal
		
		//restrict rules to only run once in a trace
		& (All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j)
"

end