theory DAA_PnC_Unlinkability_Credential_Installation
begin

/*
  Protocol:	DAA_PnC
  Properties:	PR2 - Unlinkable Credential Installation

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

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

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


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

analyzed: daa_pnc_unlinkability_credential_installation.spthy

  RHS :  reuse_ADV_Knows_Not (all-traces): verified (125 steps)
  LHS :  reuse_ADV_Knows_Not (all-traces): verified (125 steps)
  LHS :  diff_correctness (exists-trace): verified (8 steps)
  RHS :  diff_correctness (exists-trace): verified (8 steps)
  DiffLemma:  Observational_equivalence : verified (5985 steps)

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

real	21m42,853s
user	63m12,054s
sys	40m28,114s

*/

builtins:   asymmetric-encryption, symmetric-encryption, signing//, 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
			 

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

// Initialisation of the eMSP (the DAA Issuer) and the CCH (acting as CPS)
// we do not allow key reveals for the issuer
rule Issuer_and_CPS_Init:
		let 
			I=$Iss
			pkX=PkX(~x,'P2')
			pkY=PkY(~y,'P2')
		in
		[ Fr(~x)
			, Fr(~y)
			, Fr(~cps)
		]
		--[Issuer_Init()
			, ADV_Knows_Not(~x)
			, ADV_Knows_Not(~y)
			, ADV_Knows_Not(~cps)
			, OnlyOnce('Issuer_Init')]->
		[ !Ltk(I,~x, ~y)
			, Out(<pkX,pkY>)
			, !LtkCPS($CPS_I,~cps)
			, Out(pk(~cps))
		]

/*
In this model, we generate three EV credential requests. One from EV1/TPM1 with the public endorsement key pke1
and one from EV2/TPM2 with the public endorsement key pke2. The eMSP then issues credentials for two of these requests.
The adversary obtains the credential request messages, the issued credentials, and the TPMs public information.
The question is: Can the adversary distinguish between the two systems, i.e. can he decide wether the two credentials 
have been issued to the same or different EVs?
*/
rule EV_Generate_Credential_Requests:
	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>

		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>)
		sig_over_m2=sign(signed_m2,~pc2)

		m_out2=aenc(<sig_over_m2,m2>,pk(cps))

		// Difference property: The adversary cannot distinguish whether the
		// first credential installation was run with TPM1 or TPM2
		CERT_REQ_DIFF=diff(<'req1', m_out1, n1>,
						   <'req2', m_out2, n2>)
		
		// Details for third request by TPM2 (same DAA key Q_PD2)
		m3=<pke2,pk(~pc2), Q_PD2, ~res_n3, 'join_Issuer_1'>
		signed_m3=H_SHA256(<m3, pk(cps), n3>) // In(n)
		sig_over_m3=sign(signed_m3,~pc2)
		m_out3=aenc(<sig_over_m3,m3>,pk(cps))
  in
        [	!LtkCPS(CPS_I, cps)		//the issuer's private 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)

			, In(n3)
			, Fr(~res_n3)
      ]
    --[	CreateSigmas()
			, ADV_Knows_Not(~TPM_EK_Seed1)
			, ADV_Knows_Not(e1)
			, ADV_Knows_Not(~pc1)
			, ADV_Knows_Not(~f1)
			, ADV_Knows_Not(~TPM_EK_Seed2)
			, ADV_Knows_Not(e2)
			, ADV_Knows_Not(~pc2)
			, ADV_Knows_Not(~f2)
			, OnlyOnce( 'SIGN' )
	]->	
	 [
		  CertReq(CERT_REQ_DIFF)
		, CertReq(<'req3', m_out3, n3>)
		, Out(<'FirstTPM', pke1, PC_PD1, Q_PD1>)
		, Out(<'SecondTPM', 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))

		CERT_REQ_DIFF=<req, m_in, n>

		//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))
		
		// We use RSA instead of ECDHE keys to keep the model simple
		s_2_hat=aenc(~s_2_dh, pke) //TODO
		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) //TODO len16
		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) //TODO
		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>

		//TODO len16
		//m_out=<EMSP_Cert, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, C_hat, sk_DUP, res_n, 'Host_CompleteJoin'>
		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(CERT_REQ_DIFF)
		, !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
		, !LtkCPS(CPS_I, ~cps)
	 ] 
	 --[ Eq(verify(sig,signed_m,pk(pc)), true)	
	 	, CreateRes(req)
		, ADV_Knows_Not(~r)
		, ADV_Knows_Not(~l)
		, ADV_Knows_Not(~s_2_dh)
		, ADV_Knows_Not(~K_2)
		, ADV_Knows_Not(~sk_emaid)
		, ADV_Knows_Not(~seed_3_dh)
		, ADV_Knows_Not(~obfuscationValue)
		, ADV_Knows_Not(curlyK_2)
		, ADV_Knows_Not(k_e)
		, ADV_Knows_Not(sk_k_e)
		, ADV_Knows_Not(k_h)
		, ADV_Knows_Not(sk_k_h)
		, OnlyOnce(<'Issuer_Verify_Challenge', req>)
		]->
	 [  
		// The adversary receives the credential requests (m_in) and 
		// responses (m_out, sig_m) from the eMSP/CPS for either 
		// TPM1 or TPM2 (diff property) and one more for TPM2
		Out(<m_in, m_out, sig_m>)
	 ]	

// Helper lemma for proof generation
lemma reuse_ADV_Knows_Not [diff_reuse]:
// Adversary does not know data marked with ADV_Knows_Not
"	All a #i . 
		ADV_Knows_Not(a) @ #i 
			==> 
				not(Ex #k1 . (KU(a) @k1) )
"

lemma diff_correctness [left]: exists-trace
"	Ex #t1 #t2 #t3 #t4 .
		Issuer_Init() @ t1
		& CreateSigmas() @ t2
		& CreateRes('req1') @ t3
		& CreateRes('req3') @ t4

		& #t1<#t2
		& #t2<#t3
		& #t3<#t4
		
		//restrict rules to only run once in a trace
		& (All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j)
"

lemma diff_correctness [right]: exists-trace
"	Ex #t1 #t2 #t3 #t4 .
		Issuer_Init() @ t1
		& CreateSigmas() @ t2
		& CreateRes('req2') @ t3
		& CreateRes('req3') @ t4

		& #t1<#t2
		& #t2<#t3
		& #t3<#t4
		
		//restrict rules to only run once in a trace
		& (All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j)
"

end