Newer
Older
theory DAA_PnC_Anonymity_Credential_Installation
begin
/*
Protocol: DAA_PnC
Properties: Weaker version of PR2 - Anonymity of 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_anonymity_credential_installation.spthy\
--quit-on-warning --diff --heuristic=O\
--oraclename=ObsEquOracle_credential_installation.py +RTS -N8 -RTS
time tamarin-prover daa_pnc_anonymity_credential_installation.spthy\
--quit-on-warning --diff --heuristic=O\
--oraclename=ObsEquOracle_credential_installation.py\
==============================================================================
summary of summaries:
analyzed: daa_pnc_anonymity_credential_installation.spthy
RHS : reuse_ADV_Knows_Not (all-traces): verified (124 steps)
LHS : reuse_ADV_Knows_Not (all-traces): verified (124 steps)
LHS : diff_correctness (exists-trace): verified (7 steps)
RHS : diff_correctness (exists-trace): verified (7 steps)
DiffLemma: Observational_equivalence : verified (3363 steps)
==============================================================================
real 9m15,722s
user 24m11,795s
sys 17m23,696s
*/
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)
, !Pk(I, pkX,pkY)
, Out(<pkX,pkY>)
, !LtkCPS($CPS_I,~cps)
, !PkCPS($CPS_I, pk(~cps))
, Out(pk(~cps))
]
/*
In this model, we generate two 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 one of these requests.
The adversary obtains the credential request mesage, the issued credential, and the public information of TPM1 and TPM2.
The question is: Can the adversary decide whether the credentials have been issued for TPM1 or TPM2?
*/
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
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>)
sig_over_m2=sign(signed_m2,~pc2)
m_out2=aenc(<sig_over_m2,m2>,pk(cps))
// Difference property: The adversary cannot distinguish whether the
// credential installation was run with TPM1 or TPM2
CERT_REQ_DIFF=diff(<'req1', m_out1, n1>,
<'req2', m_out2, n2>)
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)
]
--[ 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' )
159
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
]->
[
CertReq(CERT_REQ_DIFF)
, 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)
, !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)
, 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 .
& CreateSigmas() @ t2
& CreateRes('req1') @ t3
//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 .
Issuer_Init() @ t1
& CreateSigmas() @ t2
& CreateRes('req2') @ t3
& #t1<#t2
& #t2<#t3
//restrict rules to only run once in a trace
& (All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j)
"
end