Newer
Older
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\
==============================================================================
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)
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
, 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)
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
, 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)
[
// 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
//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
//restrict rules to only run once in a trace
& (All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j)
"
end