Newer
Older
theory DAA_PnC_Anonymity_Charge_Authorization
begin
/*
Protocol: DAA_PnC
Properties: Weaker version of PR2 - Anonymous 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_anonymity_charge_authorisation.spthy\
--quit-on-warning --diff --heuristic=O\
--oraclename=ObsEquOracle_charge_authorisation.py +RTS -N8 -RTS
time tamarin-prover daa_pnc_anonymity_charge_authorisation.spthy\
--quit-on-warning --diff --heuristic=O\
--oraclename=ObsEquOracle_charge_authorisation.py\
==============================================================================
summary of summaries:
analyzed: daa_pnc_anonymity_charge_authorisation.spthy
RHS : diff_correctness (exists-trace): verified (7 steps)
LHS : diff_correctness (exists-trace): verified (7 steps)
DiffLemma: Observational_equivalence : verified (25531 steps)
==============================================================================
real 117m54,696s
user 308m21,683s
sys 199m35,416s
*/
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 used 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)"
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
//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
a charge authorization requests, either for TPM1 or TPM2 (diff property).
The question is: Can the adversary decide whether the generated charge authorisation values <auth_m1, auth_m2>
have been generated by TPM1 or TPM2?
*/
// 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>)
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
]
// 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) //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)
// 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_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(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)
// 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>)
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
, !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 )
, Out(<'FirstTPM', pke1, PC_PD1, Q_PD1, sk_PD1>)
, Out(<'SecondTPM', pke2, PC_PD2, Q_PD2, sk_PD2>)
]
// The EV obtains a credential response either for TPM1 or TPM2 (diff property)
// It verifies the credentials and outputs the charge authrization values auth_m1 and auth_m2
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>
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
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(<$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()
, OnlyOnce('EV_Auth')
" Ex #t1 #t3 #t4 #t5 #t6 #t7 .
Issuer_Init() @ t1
& Generate_TPM_Keys() @ t3
& CreateRes('req1') @ t4
& CreateRes('req2') @ t5
& Two_Cert_Res() @ t6
& EV_Auth() @ 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