From f9ac654d7d3e94dbef5b320f59dc2d95c8d5a055 Mon Sep 17 00:00:00 2001
From: Dustin Kern <dustin.kern@h-da.de>
Date: Fri, 30 Jul 2021 18:54:09 +0200
Subject: [PATCH] changed names to better match paper
---
.../ObsEquOracle_charge_authorisation.py | 23 +-
.../ObsEquOracle_credential_installation.py | 19 +-
.../ObsEquOracle_ev_users_locations.py | 14 +-
.../daa_pnc_anonymity_cdrs.spthy | 39 +-
...a_pnc_anonymity_charge_authorisation.spthy | 76 +--
...nc_anonymity_credential_installation.spthy | 126 ++---
...daa_pnc_anonymity_ev_users_locations.spthy | 45 +-
.../daa_pnc_unlinkability_cdrs.spthy | 37 +-
...c_unlinkability_charge_authorisation.spthy | 67 ++-
...nlinkability_credential_installation.spthy | 135 ++---
...pnc_unlinkability_ev_users_locations.spthy | 44 +-
README.md | 22 +-
...daa_pnc_charge_authorisation_offline.spthy | 461 +++++++++---------
.../daa_pnc_charge_authorisation_online.spthy | 416 ++++++++--------
14 files changed, 795 insertions(+), 729 deletions(-)
diff --git a/Privacy_Properties/ObsEquOracle_charge_authorisation.py b/Privacy_Properties/ObsEquOracle_charge_authorisation.py
index cc90b18..f75cae7 100755
--- a/Privacy_Properties/ObsEquOracle_charge_authorisation.py
+++ b/Privacy_Properties/ObsEquOracle_charge_authorisation.py
@@ -31,21 +31,23 @@ if lemma!="AnyLemma":
elif re.match('.*!LtkCPS\(.*', line): rank[106].append(num)
elif re.match('.*!CP_Init\(.*', line): rank[106].append(num)
elif re.match('.*EV_Data_Keys.*', line): rank[109].append(num)
- elif re.match('.*EV_Start_Auth.*', line): rank[108].append(num)
+ elif re.match('.*EV_Start_Auth.*', line):
+ if re.match('.*corr.*', lemma): rank[111].append(num)
+ else: rank[92].append(num)
elif re.match('.*TPM_Keys.*', line): rank[109].append(num)
elif re.match('.*EV_Data.*', line): rank[108].append(num)
+ elif re.match('.*TPM_EK_QPD\( \'req1.*', line): rank[112].append(num)
elif re.match('.*TPM_EK_QPD.*', line): rank[108].append(num)
- elif re.match('.*!TPM_EK_QPD.*', line): rank[108].append(num)
- elif re.match('.*CertRes.*', line): rank[115].append(num)
- elif re.match('.*!CertRes.*', line): rank[115].append(num)
+ elif re.match('.*CertRes\( \'req1.*', line): rank[113].append(num)
+ elif re.match('.*CertRes.*', line): rank[110].append(num)
elif re.match('.*CertReq.*', line): rank[107].append(num) #?
elif re.match('.*!KU\( ~x.*', line): rank[101].append(num)
elif re.match('.*!KU\( ~y.*', line): rank[101].append(num)
elif re.match('.*!KU\( ~sk.*', line): rank[101].append(num)
elif re.match('.*!KU\( ~g.*', line): rank[101].append(num)
elif re.match('.*!KD\(.*', line): rank[121].append(num)
- elif re.match('.*!KU\( \'ch\w+\' \)', line): rank[120].append(num)
- elif re.match('.*!KU\( \$CP \)', line): rank[114].append(num)
+ elif re.match('.*!KU\( \'ch\w+\' \)', line): rank[97].append(num)
+ elif re.match('.*!KU\( \$CP \)', line): rank[96].append(num)
elif re.match('.*!KU\( \$\w+ .*', line): rank[95].append(num)
elif re.match('.*!KU\( \$.*', line): rank[85].append(num) #9?
elif re.match('.*~~>.*', line):
@@ -66,21 +68,24 @@ if lemma!="AnyLemma":
elif re.match('.*!KU\( plus.*', line): rank[33].append(num)
elif re.match('.*!KU\( Nonce.*', line): rank[33].append(num)
elif re.match('.*!KU\( sign.*', line): rank[33].append(num)
+ elif re.match('.*!KU\( h\(MAC\(.*', line): rank[32].append(num)
+ elif re.match('.*!KU\( h\(<\s*MAC\(.*', line): rank[32].append(num)
+ elif re.match('.*!KU\( MAC\(.*', line): rank[32].append(num)
elif re.match('.*!KU\( H_n_2.*', line): rank[22].append(num)
elif re.match('.*!KU\( pk\(.*', line): rank[23].append(num)
elif re.match('.*!KU\( H_k_7.*', line): rank[21].append(num)
elif re.match('.*!KU\( H_k_2.*', line): rank[21].append(num)
+ elif re.match('.*!KU\( H_6.*', line): rank[21].append(num)
elif re.match('.*!KU\( h\(<\$CP.*', line): rank[19].append(num)
elif re.match('.*!KU\( h\(.*', line): rank[20].append(num)
- elif re.match('.*!KU\( MAC\(.*', line): rank[20].append(num)
elif re.match('.*!KU\( H_SHA256.*', line): rank[19].append(num)
elif re.match('.*!KU\( BSN.*', line): rank[19].append(num)
- elif re.match('.*!KU\( ~i_x.*', line): rank[19].append(num)
+ elif re.match('.*!KU\( ~i_x.*', line): rank[92].append(num)
elif re.match('.*!KU\( QPub.*', line): rank[19].append(num)
elif re.match('.*!KU\( certData.*', line): rank[19].append(num)
elif re.match('.*!KU\( \$CP\..*', line): rank[24].append(num) #?
#
- elif re.match('.*!KU\( ~.*', line): rank[92].append(num)
+ elif re.match('.*!KU\( ~.*', line): rank[93].append(num)
elif re.match('.*!KU\( i_x_t.*', line): rank[8].append(num)
elif re.match('.*!KU\( dataID.*', line): rank[7].append(num)
elif re.match('.*!KU\( sid.*', line): rank[7].append(num)
diff --git a/Privacy_Properties/ObsEquOracle_credential_installation.py b/Privacy_Properties/ObsEquOracle_credential_installation.py
index d91da75..e46db3f 100755
--- a/Privacy_Properties/ObsEquOracle_credential_installation.py
+++ b/Privacy_Properties/ObsEquOracle_credential_installation.py
@@ -1,9 +1,9 @@
#!/usr/bin/python3.8
import re
-import os
+# import os
import sys
-debug = True
+# debug = True
lines = sys.stdin.readlines()
lemma = sys.argv[1]
@@ -16,13 +16,11 @@ lemma = sys.argv[1]
vk=dict()
-rank = [] # list of list of goals, main list is ordered by priority
maxPrio = 110
-for i in range(0,maxPrio):
- rank.append([])
+rank = [ [] for i in range(maxPrio)] # list of list of goals, main list is ordered by priority
if lemma!="AnyLemma":
- print("applying lemma")
+ # print("applying lemma")
for line in lines:
num = line.split(':')[0]
@@ -33,6 +31,7 @@ if lemma!="AnyLemma":
elif re.match('.*TPM_EK_QPD.*', line): rank[108].append(num)
elif re.match('.*CertRes\( req.*', line): rank[105].append(num)
elif re.match('.*CertRes.*', line): rank[107].append(num)
+ elif re.match('.*CertReq\( <req.*', line): rank[105].append(num)
elif re.match('.*CertReq.*', line): rank[107].append(num) #?
elif re.match('.*!KU\( ~cps.*', line): rank[108].append(num)
elif re.match('.*!KU\( ~res.*', line): rank[51].append(num)
@@ -66,6 +65,9 @@ if lemma!="AnyLemma":
elif re.match('.*!KU\( sign\(', line): rank[49].append(num)
elif re.match('.*!KU\( aenc\(~s', line): rank[49].append(num)
elif re.match('.*!KU\( aenc\(', line): rank[45].append(num)
+ elif re.match('.*!KU\( true.*', line): rank[20].append(num)
+ elif re.match('.*!KU\( PkY\(.*', line): rank[12].append(num)
+ elif re.match('.*!KU\( PkX\(.*', line): rank[11].append(num)
elif re.match('.*!KU\( x.*', line): rank[5].append(num)
elif re.match('.*!KU\( n.*', line): rank[4].append(num)
elif re.match('.*', line): rank[10].append(num)
@@ -77,5 +79,8 @@ else:
# Ordering all goals by ranking (higher first)
for listGoals in reversed(rank):
for goal in listGoals:
- sys.stderr.write(goal)
+ # sys.stderr.write(goal)
print(goal)
+ exit(0)
+
+# exit(0)
\ No newline at end of file
diff --git a/Privacy_Properties/ObsEquOracle_ev_users_locations.py b/Privacy_Properties/ObsEquOracle_ev_users_locations.py
index 9651112..b208013 100755
--- a/Privacy_Properties/ObsEquOracle_ev_users_locations.py
+++ b/Privacy_Properties/ObsEquOracle_ev_users_locations.py
@@ -46,8 +46,9 @@ if lemma!="AnyLemma":
elif re.match('.*!KU\( ~sk.*', line): rank[101].append(num)
elif re.match('.*!KU\( ~g.*', line): rank[101].append(num)
elif re.match('.*!KD\(.*', line): rank[121].append(num)
- elif re.match('.*!KU\( \'ch\w+\' \)', line): rank[89].append(num)
- elif re.match('.*!KU\( \$CP \)', line): rank[87].append(num)
+ elif re.match('.*!KU\( \'ch\w+\' \)', line): rank[93].append(num)
+ elif re.match('.*!KU\( \$CP \)', line): rank[92].append(num)
+ elif re.match('.*!KU\( \$CP\d \)', line): rank[92].append(num)
elif re.match('.*!KU\( \$\w+ .*', line): rank[86].append(num)
elif re.match('.*!KU\( \$.*', line): rank[85].append(num) #9?
elif re.match('.*~~>.*', line):
@@ -55,8 +56,8 @@ if lemma!="AnyLemma":
elif re.match('.*\(#vk\..*', line):
i=re.search('.*\(#vk\.(\d+),.*', line).group(1)
vk[int(i)]=num
- rank[92]=[vk[key] for key in sorted(vk.keys())]
- elif re.match('.*\(#vk.*', line): rank[93].append(num)
+ rank[94]=[vk[key] for key in sorted(vk.keys())]
+ elif re.match('.*\(#vk.*', line): rank[95].append(num)
else: rank[90].append(num) # 86?
#
elif re.match('.*!KU\( Pk.*', line): rank[22].append(num)
@@ -68,6 +69,8 @@ if lemma!="AnyLemma":
elif re.match('.*!KU\( plus.*', line): rank[33].append(num)
elif re.match('.*!KU\( Nonce.*', line): rank[33].append(num)
elif re.match('.*!KU\( sign.*', line): rank[33].append(num)
+ elif re.match('.*!KU\( KDF.*', line): rank[96].append(num)
+ elif re.match('.*!KU\( curlyK.*', line): rank[96].append(num)
elif re.match('.*!KU\( H_n_2.*', line): rank[22].append(num)
elif re.match('.*!KU\( pk\(.*', line): rank[23].append(num)
elif re.match('.*!KU\( H_k_7.*', line): rank[21].append(num)
@@ -75,6 +78,7 @@ if lemma!="AnyLemma":
elif re.match('.*!KU\( h\(<\$CP.*', line): rank[19].append(num)
elif re.match('.*!KU\( h\(.*', line): rank[20].append(num)
elif re.match('.*!KU\( MAC\(.*', line): rank[20].append(num)
+ elif re.match('.*!KU\( true.*', line): rank[20].append(num)
elif re.match('.*!KU\( H_SHA256.*', line): rank[19].append(num)
elif re.match('.*!KU\( BSN.*', line): rank[19].append(num)
elif re.match('.*!KU\( ~i_x.*', line): rank[19].append(num)
@@ -82,7 +86,7 @@ if lemma!="AnyLemma":
elif re.match('.*!KU\( certData.*', line): rank[19].append(num)
elif re.match('.*!KU\( \$CP\..*', line): rank[24].append(num)
#
- elif re.match('.*!KU\( ~.*', line): rank[92].append(num)
+ elif re.match('.*!KU\( ~.*', line): rank[96].append(num)
elif re.match('.*!KU\( i_x_t.*', line): rank[8].append(num)
elif re.match('.*!KU\( dataID.*', line): rank[7].append(num)
elif re.match('.*!KU\( sid.*', line): rank[7].append(num)
diff --git a/Privacy_Properties/daa_pnc_anonymity_cdrs.spthy b/Privacy_Properties/daa_pnc_anonymity_cdrs.spthy
index 2c38eb7..045647b 100644
--- a/Privacy_Properties/daa_pnc_anonymity_cdrs.spthy
+++ b/Privacy_Properties/daa_pnc_anonymity_cdrs.spthy
@@ -1,4 +1,4 @@
-theory DAA_PnC_Unlinkability_Charge_Data_Records
+theory DAA_PnC_Anonymity_Charge_Data_Records
begin
/*
@@ -28,7 +28,7 @@ time tamarin-prover interactive daa_pnc_anonymity_cdrs.spthy\
time tamarin-prover daa_pnc_anonymity_cdrs.spthy\
--quit-on-warning --diff --heuristic=O\
--oraclename=ObsEquOracle_cdrs.py\
- --prove=diff_signatures_no_verify +RTS -N8 -RTS
+ --prove=diff_correctness +RTS -N8 -RTS
==============================================================================
@@ -36,15 +36,15 @@ summary of summaries:
analyzed: daa_pnc_anonymity_cdrs.spthy
- RHS : diff_signatures_no_verify (exists-trace): verified (6 steps)
- LHS : diff_signatures_no_verify (exists-trace): verified (6 steps)
- DiffLemma: Observational_equivalence : verified (6331 steps)
+ RHS : diff_correctness (exists-trace): verified (4 steps)
+ LHS : diff_correctness (exists-trace): verified (4 steps)
+ DiffLemma: Observational_equivalence : verified (8901 steps)
==============================================================================
-real 12m37,807s
-user 33m49,625s
-sys 18m24,725s
+real 25m27,863s
+user 64m33,939s
+sys 49m34,617s
*/
@@ -335,9 +335,9 @@ rule EV_Auth:
E=E_S(~r_cv1,S)*/
//TPM_Create_Session_Key
- Qk=pk(~g)
+ pkCCsess=pk(~g)
/*
- Qk_PD=<'SessionKey_public_data', Qk>
+ Qk_PD=<'SessionKey_public_data', pkCCsess>
Qk_n=<'SHA256',H_SHA256(Qk_PD)>
Qk_SD=senc(~g,aes_key)
@@ -361,12 +361,12 @@ rule EV_Auth:
small_s=plus(~r_cv1, multp(h2, ~f))*/
//TPM2_HMAC1
- M_id=MAC(m_buffer, sk_emaid)
- X1=h(M_id)
+ 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, X1, sigma_K, 'TPM_Certificate_Of_Q_K'>
+ //auth_m1=<EMSP_Cert, M_id, sigma_K, 'TPM_Certificate_Of_Q_K'>
//Host_Auth
m_buffer2=<'01',i_x>
@@ -375,20 +375,21 @@ rule EV_Auth:
M_auth=MAC(m_buffer2, sk_emaid)
//Host_Auth2
- X2=h(h(<M_auth, nonce_ix>))
- //authH=h(<$CP, nonce, X2>)
+ 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, ~i_x, X2, 'AuthorizationReq'>
+ //auth_m2=<authH, sig_over_auth, ~i_x, tM_auth, 'AuthorizationReq'>
// CP_Verify
- auth_m_emsp=<I, X1, nonce_ix, X2, Qk, 'EMSP_Auth'>
+ auth_m_emsp=<I, M_id, nonce_ix, tM_auth, pkCCsess, 'EMSP_Auth'>
//EV_DataSign
- dataTBS=h(<'charge_data', dataID, M_auth>)
+ ev_h=h(<'EV_h',M_auth,pkCCsess>)
+ dataTBS=h(<'charge_data', dataID, ev_h>)
dataSig=sign(dataTBS,~g)
//CP_DataRec
@@ -416,7 +417,7 @@ rule EV_Auth:
]
-lemma diff_signatures_no_verify: exists-trace
+lemma diff_correctness: exists-trace
" Ex #t1 #t3 #t4 #t5 #t6 #t7 .
Issuer_Init() @ t1
& Generate_TPM_Keys() @ t3
diff --git a/Privacy_Properties/daa_pnc_anonymity_charge_authorisation.spthy b/Privacy_Properties/daa_pnc_anonymity_charge_authorisation.spthy
index 1c57e00..f539db2 100644
--- a/Privacy_Properties/daa_pnc_anonymity_charge_authorisation.spthy
+++ b/Privacy_Properties/daa_pnc_anonymity_charge_authorisation.spthy
@@ -1,4 +1,4 @@
-theory DAA_PnC_Unlinkability_Charge_Authorization
+theory DAA_PnC_Anonymity_Charge_Authorization
begin
/*
@@ -28,9 +28,7 @@ time tamarin-prover interactive daa_pnc_anonymity_charge_authorisation.spthy\
time tamarin-prover daa_pnc_anonymity_charge_authorisation.spthy\
--quit-on-warning --diff --heuristic=O\
--oraclename=ObsEquOracle_charge_authorisation.py\
- --prove=diff_signatures_no_verify +RTS -N8 -RTS
-
-
+ --prove=diff_correctness +RTS -N8 -RTS
==============================================================================
@@ -38,15 +36,15 @@ summary of summaries:
analyzed: daa_pnc_anonymity_charge_authorisation.spthy
- RHS : diff_signatures_no_verify (exists-trace): verified (5 steps)
- LHS : diff_signatures_no_verify (exists-trace): verified (5 steps)
- DiffLemma: Observational_equivalence : verified (16285 steps)
+ RHS : diff_correctness (exists-trace): verified (7 steps)
+ LHS : diff_correctness (exists-trace): verified (7 steps)
+ DiffLemma: Observational_equivalence : verified (25531 steps)
==============================================================================
-real 61m46,250s
-user 159m3,008s
-sys 98m57,900s
+real 117m54,696s
+user 308m21,683s
+sys 199m35,416s
*/
@@ -56,13 +54,14 @@ 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
- //TODO: , QPub/2, QName/2, certData/2
// 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)"
//the 'Issuer' should only be initialised once
restriction single_issuer_single_init:
@@ -156,8 +155,8 @@ rule EV_Generate_Credential_Requests:
[
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>)
+ , !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
@@ -244,7 +243,7 @@ rule Issuer_Issue_Credentials:
, CreateResSig(sig_m)
, OnlyOnce(<'Issuer_Verify_Challenge', req>)
]->
- [ CertRes(req, m_in, n, m_out, sig_m)
+ [ !CertRes(req, m_in, n, m_out, sig_m)
]
// The CPS receives two credential responses from the eMSP
@@ -254,6 +253,27 @@ rule Issuer_Issue_Credentials:
// 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))
@@ -274,10 +294,10 @@ rule Two_Cert_Res:
<'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>)
+ !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))
]
--[
@@ -304,7 +324,7 @@ rule EV_Auth:
Q=multp(~f, 'P1')
Q_PD=<'DAA_public_data', Q>
- i_x=h(<i_x_t, pke>)
+ 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>)
@@ -353,7 +373,6 @@ rule EV_Auth:
m_buffer=<'00',i_x>
//TPM2_Load_And_Certify
- //TODO qualified name allows attack if pke known
/*N1=QName('SHA256',H_SHA256('root'))
N2=QName('SHA256',H_SHA256(E_PD))
N3=H_SHA256(<N1, N2>)
@@ -367,12 +386,12 @@ rule EV_Auth:
small_s=plus(~r_cv1, multp(h2, ~f))
//TPM2_HMAC1
- M_id=MAC(m_buffer, sk_emaid)
- X1=h(M_id)
+ 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, X1, E, sigma_K, 'TPM_Certificate_Of_Q_K'> //TODO: $CP, ~sid?
+ auth_m1=<EMSP_Cert, M_id, E, sigma_K, 'PaymentDetailsReq'>
//Host_Auth
m_buffer2=<'01',i_x>
@@ -381,14 +400,14 @@ rule EV_Auth:
M_auth=MAC(m_buffer2, sk_emaid)
//Host_Auth2
- X2=h(h(<M_auth, nonce_ix>))
- authH=h(<$CP, nonce, X2>)
+ 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, X2, 'AuthorizationReq'> //TODO: ~sid?
+ auth_m2=<authH, sig_over_auth, tM_auth, 'AuthorizationReq'>
in
[
EV_Start_Auth(Auth_DIFF)
@@ -396,7 +415,7 @@ rule EV_Auth:
, Fr(~l)
, Fr(~r_cv1)
, Fr(~g)
- , In(i_x_t)
+ , In(~i_x_t)
, In(<$CP, sid, <nonce, nonce_ix>, <'charge_data', dataID>>)
, Fr(~rnd_n_C)
@@ -406,6 +425,7 @@ rule EV_Auth:
, Eq(verify(sig_over_m,signed_m,pk(pc)), true)
, EV_Auth()
, OnlyOnce('EV_Auth')
+ , OnlyOnce_ix('EV_Auth', i_x)
]->
[
Out(<auth_m1, auth_m2>)
@@ -413,7 +433,7 @@ rule EV_Auth:
-lemma diff_signatures_no_verify: exists-trace
+lemma diff_correctness: exists-trace
" Ex #t1 #t3 #t4 #t5 #t6 #t7 .
Issuer_Init() @ t1
& Generate_TPM_Keys() @ t3
diff --git a/Privacy_Properties/daa_pnc_anonymity_credential_installation.spthy b/Privacy_Properties/daa_pnc_anonymity_credential_installation.spthy
index 4225e8f..9b0c92a 100644
--- a/Privacy_Properties/daa_pnc_anonymity_credential_installation.spthy
+++ b/Privacy_Properties/daa_pnc_anonymity_credential_installation.spthy
@@ -28,7 +28,7 @@ time tamarin-prover interactive daa_pnc_anonymity_credential_installation.spthy\
time tamarin-prover daa_pnc_anonymity_credential_installation.spthy\
--quit-on-warning --diff --heuristic=O\
--oraclename=ObsEquOracle_credential_installation.py\
- --prove=diff_signatures_no_verify +RTS -N8 -RTS
+ --prove=diff_correctness +RTS -N8 -RTS
==============================================================================
@@ -36,15 +36,17 @@ summary of summaries:
analyzed: daa_pnc_anonymity_credential_installation.spthy
- RHS : diff_signatures_no_verify (exists-trace): verified (5 steps)
- LHS : diff_signatures_no_verify (exists-trace): verified (5 steps)
- DiffLemma: Observational_equivalence : verified (5200 steps)
+ 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 37m11,516s
-user 102m59,471s
-sys 81m59,863s
+real 9m15,722s
+user 24m11,795s
+sys 17m23,696s
*/
@@ -55,14 +57,8 @@ functions: MAC/2, KDF_EK/1,KDF_a/3, KDF_e/4, multp/2, plus/2, //len16/1,
// Protocol Restrictions (Axioms)
-
restriction equality: "All #i x y . Eq( x, y ) @ i ==> x = y"
-
-//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_and_CPS_Init:
@@ -76,6 +72,9 @@ rule Issuer_and_CPS_Init:
, 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)
@@ -91,7 +90,7 @@ and one from EV2/TPM2 with the public endorsement key pke2. The eMSP then issues
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?
*/
-rule Generate_TPM_DAA_CERTIFY:
+rule EV_Generate_Credential_Requests:
let
//inputs from Issuer PK
pkX=PkX(x,'P2')
@@ -124,9 +123,9 @@ rule Generate_TPM_DAA_CERTIFY:
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 request was generated with TPM1 or TPM2
+ // credential installation was run with TPM1 or TPM2
CERT_REQ_DIFF=diff(<'req1', m_out1, n1>,
<'req2', m_out2, n2>)
in
@@ -147,8 +146,16 @@ rule Generate_TPM_DAA_CERTIFY:
, Fr(~f2)
, Fr(~res_n2)
]
- --[ CreateSigmas(),
- OnlyOnce( 'SIGN' )
+ --[ 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)
@@ -235,53 +242,58 @@ rule Issuer_Issue_Credentials:
]
--[ Eq(verify(sig,signed_m,pk(pc)), true)
, CreateRes(req)
- , CreateResSig(sig_m)
+ , 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>)
]->
- [ CertRes(req, m_in, m_out, sig_m)
+ [
+ // 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>)
]
-// The CPS receives the credential responses from the eMSP
-// either from TPM1 or TPM2 (diff property)
-// The CPS then signs the response and forwards it to the
-// CPO (the adversary in this model) together with the original credential request
-rule Two_Res:
- let
- m1=<pke1,pk(~pc1), Q_PD1, res_n1, 'join_Issuer_1'>
- m_in1=aenc(<sig_over_m1,m1>,pk(cps))
- 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)
- in
- [
- CertRes(req, m_in1, m_out1, sig_m1)
- , !PkCPS(CPS_I,pk(cps))
- ]
- --[
- Eq(verify(sig_m1,H_SHA256(m_out1),pk(cps)), true)
- , Diff_Sigs()
- , OnlyOnce('Two_Res')
- ]->
- [ Out(<m_in1, m_out1, sig_m1>) ]
-
-
-lemma diff_signatures_no_verify: exists-trace
-" Ex #t1 #t3 #t6 .
+// 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 .
Issuer_Init() @ t1
- & CreateSigmas() @ t3
+ & CreateSigmas() @ t2
+ & CreateRes('req1') @ t3
- & (
- (Ex #k1 . (CreateRes('req1') @k1) )
- |
- (Ex #k1 . (CreateRes('req2') @k1) )
- )
+ & #t1<#t2
+ & #t2<#t3
- & Diff_Sigs() @ t6
- & #t1<#t3
- & #t3<#t6
-
- //we had no key reveal
- //& not( Ex RevealEvent ENTITY #k1 . KeyReveal(RevealEvent, ENTITY)@k1)
+ //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)
diff --git a/Privacy_Properties/daa_pnc_anonymity_ev_users_locations.spthy b/Privacy_Properties/daa_pnc_anonymity_ev_users_locations.spthy
index 06af6ad..fb0a11b 100644
--- a/Privacy_Properties/daa_pnc_anonymity_ev_users_locations.spthy
+++ b/Privacy_Properties/daa_pnc_anonymity_ev_users_locations.spthy
@@ -28,12 +28,12 @@ time tamarin-prover interactive daa_pnc_anonymity_ev_users_locations.spthy\
time tamarin-prover daa_pnc_anonymity_ev_users_locations.spthy\
--quit-on-warning --diff --heuristic=O\
--oraclename=ObsEquOracle_ev_users_locations.py\
- --prove=diff_signatures_no_verify +RTS -N8 -RTS
+ --prove=diff_correctness +RTS -N8 -RTS
time tamarin-prover daa_pnc_anonymity_ev_users_locations.spthy\
--quit-on-warning --diff --heuristic=O\
- --oraclename=ObsEquOracle_test5.py\
+ --oraclename=ObsEquOracle_ev_users_locations.py\
--prove +RTS -N8 -RTS
@@ -42,15 +42,15 @@ summary of summaries:
analyzed: daa_pnc_anonymity_ev_users_locations.spthy
- RHS : diff_signatures_no_verify (exists-trace): verified (8 steps)
- LHS : diff_signatures_no_verify (exists-trace): verified (8 steps)
- DiffLemma: Observational_equivalence : verified (11269 steps)
+ RHS : diff_correctness (exists-trace): verified (9 steps)
+ LHS : diff_correctness (exists-trace): verified (9 steps)
+ DiffLemma: Observational_equivalence : verified (13191 steps)
==============================================================================
-real 25m2,540s
-user 59m8,026s
-sys 49m40,471s
+real 42m48,143s
+user 100m43,897s
+sys 74m14,457s
*/
@@ -230,7 +230,7 @@ rule Issuer_Issue_Credentials:
, OnlyOnce(<'Issuer_Verify_Challenge', req>)
]->
[ CertRes(req, m_in, n, m_out, sig_m)
- , Out(sk_SENSITIVE) //adversary (honest-but-curious eMSP) knows this data
+ , Out(<sk_SENSITIVE, <A,B,C,D,u,j>, m>) //adversary (honest-but-curious eMSP) knows this data
]
// The CPS receives the credential responses from the eMSP
@@ -295,7 +295,7 @@ rule EV_Auth:
Q=multp(~f, 'P1')
Q_PD=<'DAA_public_data', Q>
- i_x=h(<i_x_t, pke>)
+ 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>)
@@ -333,9 +333,9 @@ rule EV_Auth:
E=E_S(~r_cv1,S)*/
//TPM_Create_Session_Key
- Qk=pk(~g)
+ pkCCsess=pk(~g)
/*
- Qk_PD=<'SessionKey_public_data', Qk>
+ Qk_PD=<'SessionKey_public_data', pkCCsess>
Qk_n=<'SHA256',H_SHA256(Qk_PD)>
Qk_SD=senc(~g,aes_key)
@@ -359,12 +359,12 @@ rule EV_Auth:
small_s=plus(~r_cv1, multp(h2, ~f))*/
//TPM2_HMAC1
- M_id=MAC(m_buffer, sk_emaid)
- X1=h(M_id)
+ 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, X1, sigma_K, 'TPM_Certificate_Of_Q_K'>
+ //auth_m1=<EMSP_Cert, M_id, sigma_K, 'TPM_Certificate_Of_Q_K'>
//Host_Auth
m_buffer2=<'01',i_x>
@@ -373,20 +373,21 @@ rule EV_Auth:
M_auth=MAC(m_buffer2, sk_emaid)
//Host_Auth2
- X2=h(h(<M_auth, nonce_ix>))
- //authH=h(<$CP, nonce, X2>)
+ 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, ~i_x, X2, 'AuthorizationReq'>
+ //auth_m2=<authH, sig_over_auth, ~i_x, tM_auth, 'AuthorizationReq'>
// CP_Verify
- auth_m_emsp=<I, X1, nonce_ix, X2, Qk, 'EMSP_Auth'>
+ auth_m_emsp=<I, M_id, nonce_ix, tM_auth, pkCCsess, 'EMSP_Auth'>
//EV_DataSign
- dataTBS=h(<'charge_data', dataID, M_auth>)
+ ev_h=h(<'EV_h',M_auth,pkCCsess>)
+ dataTBS=h(<'charge_data', dataID, ev_h>)
dataSig=sign(dataTBS,~g)
//CP_DataRec
@@ -398,7 +399,7 @@ rule EV_Auth:
//, Fr(~l)
//, Fr(~r_cv1)
, Fr(~g)
- , In(i_x_t) //In & onlyonce
+ , In(~i_x_t) //In & onlyonce
//, !CP_Init($CP)
, CP_In(CP_DIFF)
//, In(<$CP, sid>)
@@ -417,7 +418,7 @@ rule EV_Auth:
-lemma diff_signatures_no_verify: exists-trace
+lemma diff_correctness: exists-trace
" Ex #t1 #t3 #t4 #t5 #t6 #t7 .
Issuer_Init() @ t1
& Generate_TPM_Keys() @ t3
diff --git a/Privacy_Properties/daa_pnc_unlinkability_cdrs.spthy b/Privacy_Properties/daa_pnc_unlinkability_cdrs.spthy
index 29d23cd..1993c10 100644
--- a/Privacy_Properties/daa_pnc_unlinkability_cdrs.spthy
+++ b/Privacy_Properties/daa_pnc_unlinkability_cdrs.spthy
@@ -28,7 +28,7 @@ time tamarin-prover interactive daa_pnc_unlinkability_cdrs.spthy\
time tamarin-prover daa_pnc_unlinkability_cdrs.spthy\
--quit-on-warning --diff --heuristic=O\
--oraclename=ObsEquOracle_cdrs.py\
- --prove=diff_signatures_no_verify +RTS -N8 -RTS
+ --prove=diff_correctness +RTS -N8 -RTS
==============================================================================
@@ -36,15 +36,15 @@ summary of summaries:
analyzed: daa_pnc_unlinkability_cdrs.spthy
- RHS : diff_signatures_no_verify (exists-trace): verified (7 steps)
- LHS : diff_signatures_no_verify (exists-trace): verified (7 steps)
- DiffLemma: Observational_equivalence : verified (20033 steps)
+ RHS : diff_correctness (exists-trace): verified (7 steps)
+ LHS : diff_correctness (exists-trace): verified (7 steps)
+ DiffLemma: Observational_equivalence : verified (20433 steps)
==============================================================================
-real 62m21,387s
-user 161m9,209s
-sys 125m10,839s
+real 64m32,568s
+user 168m7,928s
+sys 127m47,033s
*/
@@ -340,9 +340,9 @@ rule EV_Auth:
E=E_S(~r_cv1,S)*/
//TPM_Create_Session_Key
- Qk=pk(~g)
+ pkCCsess=pk(~g)
/*
- Qk_PD=<'SessionKey_public_data', Qk>
+ Qk_PD=<'SessionKey_public_data', pkCCsess>
Qk_n=<'SHA256',H_SHA256(Qk_PD)>
Qk_SD=senc(~g,aes_key)
@@ -366,12 +366,12 @@ rule EV_Auth:
small_s=plus(~r_cv1, multp(h2, ~f))*/
//TPM2_HMAC1
- M_id=MAC(m_buffer, sk_emaid)
- X1=h(M_id)
+ 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, X1, sigma_K, 'TPM_Certificate_Of_Q_K'>
+ //auth_m1=<EMSP_Cert, M_id, sigma_K, 'TPM_Certificate_Of_Q_K'>
//Host_Auth
m_buffer2=<'01',i_x>
@@ -380,20 +380,21 @@ rule EV_Auth:
M_auth=MAC(m_buffer2, sk_emaid)
//Host_Auth2
- X2=h(h(<M_auth, nonce_ix>))
- //authH=h(<$CP, nonce, X2>)
+ 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, ~i_x, X2, 'AuthorizationReq'>
+ //auth_m2=<authH, sig_over_auth, ~i_x, tM_auth, 'AuthorizationReq'>
// CP_Verify
- auth_m_emsp=<I, X1, nonce_ix, X2, Qk, 'EMSP_Auth'>
+ auth_m_emsp=<I, M_id, nonce_ix, tM_auth, pkCCsess, 'EMSP_Auth'>
//EV_DataSign
- dataTBS=h(<'charge_data', dataID, M_auth>)
+ ev_h=h(<'EV_h',M_auth,pkCCsess>)
+ dataTBS=h(<'charge_data', dataID, ev_h>)
dataSig=sign(dataTBS,~g)
//CP_DataRec
@@ -422,7 +423,7 @@ rule EV_Auth:
]
-lemma diff_signatures_no_verify: exists-trace
+lemma diff_correctness: exists-trace
" Ex #t1 #t3 #t4 #t5 #t6 #t7 .
Issuer_Init() @ t1
& Generate_TPM_Keys() @ t3
diff --git a/Privacy_Properties/daa_pnc_unlinkability_charge_authorisation.spthy b/Privacy_Properties/daa_pnc_unlinkability_charge_authorisation.spthy
index 5133ef2..ec7d27a 100644
--- a/Privacy_Properties/daa_pnc_unlinkability_charge_authorisation.spthy
+++ b/Privacy_Properties/daa_pnc_unlinkability_charge_authorisation.spthy
@@ -28,7 +28,7 @@ time tamarin-prover interactive daa_pnc_unlinkability_charge_authorisation.spthy
time tamarin-prover daa_pnc_unlinkability_charge_authorisation.spthy\
--quit-on-warning --diff --heuristic=O\
--oraclename=ObsEquOracle_charge_authorisation.py\
- --prove=diff_signatures_no_verify +RTS -N8 -RTS
+ --prove=diff_correctness +RTS -N8 -RTS
==============================================================================
@@ -36,15 +36,15 @@ summary of summaries:
analyzed: daa_pnc_unlinkability_charge_authorisation.spthy
- RHS : diff_signatures_no_verify (exists-trace): verified (14 steps)
- LHS : diff_signatures_no_verify (exists-trace): verified (14 steps)
- DiffLemma: Observational_equivalence : verified (52617 steps)
+ RHS : diff_correctness (exists-trace): verified (11 steps)
+ LHS : diff_correctness (exists-trace): verified (11 steps)
+ DiffLemma: Observational_equivalence : verified (40087 steps)
==============================================================================
-real 263m45,211s
-user 446m37,142s
-sys 96m14,406s
+real 333m58,717s
+user 852m10,529s
+sys 531m58,938s
*/
@@ -67,10 +67,6 @@ restriction only_once_ix: "All event i_x #i #j . (OnlyOnce_ix(event, i_x) @ i &
restriction single_issuer_single_init:
"All #i #j . (Issuer_Init() @ i & Issuer_Init() @ j) ==> (#i=#j)"
-// TPM keys for the two TPMs are only generated once
-restriction two_TPM_single_init:
- "All #i #j . (Generate_TPM_Keys() @ i & Generate_TPM_Keys() @ 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:
@@ -159,8 +155,8 @@ rule EV_Generate_Credential_Requests:
[
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>)
+ , !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
@@ -242,7 +238,7 @@ rule Issuer_Issue_Credentials:
, CreateResSig(sig_m)
, OnlyOnce(<'Issuer_Verify_Challenge', req>)
]->
- [ CertRes(req, m_in, n, m_out, sig_m)
+ [ !CertRes(req, m_in, n, m_out, sig_m)
]
// The CPS receives two credential responses from the eMSP
@@ -252,13 +248,30 @@ rule Issuer_Issue_Credentials:
// 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>
- m1=<pke1,pk(~pc1), Q_PD1, res_n1, 'join_Issuer_1'>
- m_in1=aenc(<sig_over_m1,m1>,pk(cps))
+ 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))
@@ -276,10 +289,10 @@ rule Two_Cert_Res:
<'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>)
+ !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))
]
--[
@@ -370,12 +383,12 @@ rule EV_Auth:
small_s=plus(~r_cv1, multp(h2, ~f))
//TPM2_HMAC1
- M_id=MAC(m_buffer, sk_emaid)
- X1=h(M_id)
+ 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, X1, E, sigma_K, 'TPM_Certificate_Of_Q_K'>
+ auth_m1=<EMSP_Cert, M_id, E, sigma_K, 'PaymentDetailsReq'>
//Host_Auth
m_buffer2=<'01',i_x>
@@ -384,14 +397,14 @@ rule EV_Auth:
M_auth=MAC(m_buffer2, sk_emaid)
//Host_Auth2
- X2=h(h(<M_auth, nonce_ix>))
- authH=h(<$CP, nonce, X2>)
+ 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, X2, 'AuthorizationReq'>
+ auth_m2=<authH, sig_over_auth, tM_auth, 'AuthorizationReq'>
in
[
EV_Start_Auth(Auth_DIFF)
@@ -417,7 +430,7 @@ rule EV_Auth:
-lemma diff_signatures_no_verify: exists-trace
+lemma diff_correctness: exists-trace
" Ex #t1 #t3 #t4 #t5 #t6 #t7 .
Issuer_Init() @ t1
& Generate_TPM_Keys() @ t3
diff --git a/Privacy_Properties/daa_pnc_unlinkability_credential_installation.spthy b/Privacy_Properties/daa_pnc_unlinkability_credential_installation.spthy
index 7eda7b0..3d687b1 100644
--- a/Privacy_Properties/daa_pnc_unlinkability_credential_installation.spthy
+++ b/Privacy_Properties/daa_pnc_unlinkability_credential_installation.spthy
@@ -28,7 +28,7 @@ time tamarin-prover interactive daa_pnc_unlinkability_credential_installation.sp
time tamarin-prover daa_pnc_unlinkability_credential_installation.spthy\
--quit-on-warning --diff --heuristic=O\
--oraclename=ObsEquOracle_credential_installation.py\
- --prove=diff_signatures_no_verify +RTS -N8 -RTS
+ --prove=diff_correctness +RTS -N8 -RTS
==============================================================================
@@ -36,15 +36,17 @@ summary of summaries:
analyzed: daa_pnc_unlinkability_credential_installation.spthy
- RHS : diff_signatures_no_verify (exists-trace): verified (6 steps)
- LHS : diff_signatures_no_verify (exists-trace): verified (6 steps)
- DiffLemma: Observational_equivalence : verified (7004 steps)
+ 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 111m33,253s
-user 307m3,414s
-sys 226m37,795s
+real 21m42,853s
+user 63m12,054s
+sys 40m28,114s
*/
@@ -55,14 +57,8 @@ functions: MAC/2, KDF_EK/1,KDF_a/3, KDF_e/4, multp/2, plus/2, //len16/1,
// Protocol Restrictions (Axioms)
-
restriction equality: "All #i x y . Eq( x, y ) @ i ==> x = y"
-
-//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_and_CPS_Init:
@@ -76,6 +72,9 @@ rule Issuer_and_CPS_Init:
, 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>)
@@ -119,19 +118,19 @@ rule EV_Generate_Credential_Requests:
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 request was generated with TPM1 or TPM2
+ // 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
+
+ // 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
+ [ !LtkCPS(CPS_I, cps) //the issuer's private key
, In(n1)
, In(n2)
@@ -150,6 +149,14 @@ rule EV_Generate_Credential_Requests:
, 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' )
]->
[
@@ -236,61 +243,61 @@ rule Issuer_Issue_Credentials:
]
--[ Eq(verify(sig,signed_m,pk(pc)), true)
, CreateRes(req)
- , CreateResSig(sig_m)
+ , 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>)
]->
- [ CertRes(req, m_in, m_out, sig_m)
+ [
+ // 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>)
]
-// The CPS receives two credential responses from the eMSP
-// one either from TPM1 or TPM2 (diff property) and the other
-// from TPM2
-// The CPS then signs the two responses and forwards them to the
-// CPO (the adversary in this model) together with the original credential request
-rule Two_Res:
- let
- m1=<pke1,pk(~pc1), Q_PD1, res_n1, 'join_Issuer_1'>
- m_in1=aenc(<sig_over_m1,m1>,pk(cps))
+// 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) )
+"
- m2=<pke2,pk(~pc2), Q_PD2, res_n2, 'join_Issuer_1'>
- m_in2=aenc(<sig_over_m2,m2>,pk(cps))
+lemma diff_correctness [left]: exists-trace
+" Ex #t1 #t2 #t3 #t4 .
+ Issuer_Init() @ t1
+ & CreateSigmas() @ t2
+ & CreateRes('req1') @ t3
+ & CreateRes('req3') @ t4
- 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)
+ & #t1<#t2
+ & #t2<#t3
+ & #t3<#t4
- 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)
- in
- [
- CertRes(req, m_in1, m_out1, sig_m1)
- , CertRes('req3', m_in2, m_out2, sig_m2)
- , !LtkCPS(CPS_I, cps)
- ]
- --[
- Eq(verify(sig_m1,H_SHA256(m_out1),pk(cps)), true)
- , Eq(verify(sig_m2,H_SHA256(m_out2),pk(cps)), true)
- , Diff_Sigs()
- , OnlyOnce('Two_Res')
- ]->
- [ Out(<<m_in1, m_out1, sig_m1>, <m_in2, m_out2, sig_m2>>) ]
-
-
-lemma diff_signatures_no_verify: exists-trace
-" Ex #t1 #t3 #t6 .
- Issuer_Init() @ t1
- & CreateSigmas() @ t3
+ //restrict rules to only run once in a trace
+ & (All event #i #j . OnlyOnce(event)@i & OnlyOnce(event)@j ==> #i=#j)
+"
- & (
- (Ex #k1 . (CreateRes('req1') @k1) )
- |
- (Ex #k1 . (CreateRes('req2') @k1) )
- )
+lemma diff_correctness [right]: exists-trace
+" Ex #t1 #t2 #t3 #t4 .
+ Issuer_Init() @ t1
+ & CreateSigmas() @ t2
+ & CreateRes('req2') @ t3
+ & CreateRes('req3') @ t4
- & Diff_Sigs() @ t6
- & #t1<#t3
- & #t3<#t6
-
- //and we had no key reveal
+ & #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)
diff --git a/Privacy_Properties/daa_pnc_unlinkability_ev_users_locations.spthy b/Privacy_Properties/daa_pnc_unlinkability_ev_users_locations.spthy
index 539d019..4af691d 100644
--- a/Privacy_Properties/daa_pnc_unlinkability_ev_users_locations.spthy
+++ b/Privacy_Properties/daa_pnc_unlinkability_ev_users_locations.spthy
@@ -28,7 +28,7 @@ time tamarin-prover interactive daa_pnc_unlinkability_ev_users_locations.spthy\
time tamarin-prover daa_pnc_unlinkability_ev_users_locations.spthy\
--quit-on-warning --diff --heuristic=O\
--oraclename=ObsEquOracle_ev_users_locations.py\
- --prove=diff_signatures_no_verify +RTS -N8 -RTS
+ --prove=diff_correctness +RTS -N8 -RTS
time tamarin-prover daa_pnc_unlinkability_ev_users_locations.spthy\
@@ -42,15 +42,15 @@ summary of summaries:
analyzed: daa_pnc_unlinkability_ev_users_locations.spthy
- RHS : diff_signatures_no_verify (exists-trace): verified (12 steps)
- LHS : diff_signatures_no_verify (exists-trace): verified (12 steps)
- DiffLemma: Observational_equivalence : verified (29159 steps)
+ RHS : diff_correctness (exists-trace): verified (14 steps)
+ LHS : diff_correctness (exists-trace): verified (14 steps)
+ DiffLemma: Observational_equivalence : verified (24945 steps)
==============================================================================
-real 70m43,390s
-user 170m52,150s
-sys 143m5,176s
+real 82m35,001s
+user 196m23,500s
+sys 142m41,129s
*/
@@ -229,7 +229,7 @@ rule Issuer_Issue_Credentials:
, OnlyOnce('Issuer_Verify_Challenge')
]->
[ CertRes(m_in, n, m_out, sig_m)
- , Out(sk_SENSITIVE) //adversary (honest-but-curious eMSP) knows this data
+ , Out(<sk_SENSITIVE, <A,B,C,D,u,j>, m>) //adversary (honest-but-curious eMSP) knows this data
]
// The CPS receives the credential responses from the eMSP
@@ -297,7 +297,7 @@ rule EV_Auth:
Q=multp(~f, 'P1')
Q_PD=<'DAA_public_data', Q>
- i_x=h(<i_x_t, pke>)
+ 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>)
@@ -335,9 +335,9 @@ rule EV_Auth:
E=E_S(~r_cv1,S)*/
//TPM_Create_Session_Key
- Qk=pk(~g)
+ pkCCsess=pk(~g)
/*
- Qk_PD=<'SessionKey_public_data', Qk>
+ Qk_PD=<'SessionKey_public_data', pkCCsess>
Qk_n=<'SHA256',H_SHA256(Qk_PD)>
Qk_SD=senc(~g,aes_key)
@@ -347,7 +347,6 @@ rule EV_Auth:
m_buffer=<'00',i_x>
//TPM2_Load_And_Certify
- //TODO qualified name allows attack if pke known
/*N1=QName('SHA256',H_SHA256('root'))
N2=QName('SHA256',H_SHA256(E_PD))
N3=H_SHA256(<N1, N2>)
@@ -362,12 +361,12 @@ rule EV_Auth:
small_s=plus(~r_cv1, multp(h2, ~f))*/
//TPM2_HMAC1
- M_id=MAC(m_buffer, sk_emaid)
- X1=h(M_id)
+ 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, X1, sigma_K, 'TPM_Certificate_Of_Q_K'>
+ //auth_m1=<EMSP_Cert, M_id, sigma_K, 'TPM_Certificate_Of_Q_K'>
//Host_Auth
m_buffer2=<'01',i_x>
@@ -376,20 +375,21 @@ rule EV_Auth:
M_auth=MAC(m_buffer2, sk_emaid)
//Host_Auth2
- X2=h(h(<M_auth, nonce_ix>))
- //authH=h(<$CP, nonce, X2>)
+ 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, ~i_x, X2, 'AuthorizationReq'>
+ //auth_m2=<authH, sig_over_auth, ~i_x, tM_auth, 'AuthorizationReq'>
// CP_Verify
- auth_m_emsp=<I, X1, nonce_ix, X2, Qk, 'EMSP_Auth'>
+ auth_m_emsp=<I, M_id, nonce_ix, tM_auth, pkCCsess, 'EMSP_Auth'>
//EV_DataSign
- dataTBS=h(<'charge_data', dataID, M_auth>)
+ ev_h=h(<'EV_h',M_auth,pkCCsess>)
+ dataTBS=h(<'charge_data', dataID, ev_h>)
dataSig=sign(dataTBS,~g)
//CP_DataRec
@@ -401,7 +401,7 @@ rule EV_Auth:
//, Fr(~l)
//, Fr(~r_cv1)
, Fr(~g)
- , In(i_x_t) //In & onlyonce
+ , In(~i_x_t) //In & onlyonce
//, !CP_Init($CP)
, CP_In(CP_DIFF)
//, In(<$CP, sid>)
@@ -420,7 +420,7 @@ rule EV_Auth:
-lemma diff_signatures_no_verify: exists-trace
+lemma diff_correctness: exists-trace
" Ex #t1 #t3 #t4 #t5 #t6 #t7 .
Issuer_Init() @ t1
& Generate_TPM_Keys() @ t3
diff --git a/README.md b/README.md
index 8679bf6..077e458 100644
--- a/README.md
+++ b/README.md
@@ -17,17 +17,17 @@ The Tamarin prover (https://tamarin-prover.github.io/) is required to verify the
In the following, we list which property of our extension is addressed by which Tamarin model.
**Security_Properties**
-| Security Property | Tamarin File(s) |
-|:-------------------------------------|:--------------------------------------|
-| SR2 - Secure Credential Installation | daa_pnc_credential_installation.spthy |
-| SR3 - Secure Charge Autorization | daa_pnc_charge_authorisation_online.spthy <br> daa_pnc_charge_authorisation_offline.spthy |
-| SR4 - Charge Data Authenticity | daa_pnc_charge_authorisation_online.spthy <br> daa_pnc_charge_authorisation_offline.spthy |
+| Security Property | Tamarin File(s) |
+|:----------------------------------------|:-----------------------------------|
+| _SR<sub>2</sub>_ - Secure Credential Installation | daa_pnc_credential_installation.spthy |
+| _SR<sub>3</sub>_ - Secure Charge Autorization | daa_pnc_charge_authorisation_online.spthy <br> daa_pnc_charge_authorisation_offline.spthy |
+| _SR<sub>4</sub>_ - Charge Data Authenticity | daa_pnc_charge_authorisation_online.spthy <br> daa_pnc_charge_authorisation_offline.spthy |
**Privacy_Properties**
The files with the keyword *anonymity* in their file name contain a model for a weaker version of the properties.
-| Privacy Property | Tamarin File(s) | Oracle |
-|:----------------------------------------------|:---------------------------------------------------------------------------------------------------------|:-|
-| PR2 - Unlinkable Credential Installation | daa_pnc_anonymity_credential_installation.spthy <br> daa_pnc_unlinkability_credential_installation.spthy | oracle_credential_installation.py |
-| PR3 - Unlinkable Charge Autorization | daa_pnc_anonymity_charge_authorisation.spthy <br> daa_pnc_unlinkability_charge_authorisation.spthy | oracle_charge_authorisation.py |
-| PR4 - Unlinkable CDRs | daa_pnc_anonymity_cdrs.spthy <br> daa_pnc_unlinkability_cdrs.spthy | oracle_cdrs.py |
-| PR5 - Unlinkability of EV Users and Locations | daa_pnc_anonymity_ev_users_locations.spthy <br> daa_pnc_unlinkability_ev_users_locations.spthy | oracle_ev_users_locations.py |
+| Privacy Property | Tamarin File(s) | Oracle |
+|:-------------------------------------------------|:---------------------------------------------------------------------------------------------------------|:-|
+| _PR<sub>2</sub>_ - Unlinkable Credential Installation | daa_pnc_anonymity_credential_installation.spthy <br> daa_pnc_unlinkability_credential_installation.spthy | oracle_credential_installation.py |
+| _PR<sub>3</sub>_ - Unlinkable Charge Autorization | daa_pnc_anonymity_charge_authorisation.spthy <br> daa_pnc_unlinkability_charge_authorisation.spthy | oracle_charge_authorisation.py |
+| _PR<sub>4</sub>_ - Unlinkable CDRs | daa_pnc_anonymity_cdrs.spthy <br> daa_pnc_unlinkability_cdrs.spthy | oracle_cdrs.py |
+| _PR<sub>5</sub>_ - Unlinkability of EV Users and Locations | daa_pnc_anonymity_ev_users_locations.spthy <br> daa_pnc_unlinkability_ev_users_locations.spthy | oracle_ev_users_locations.py |
diff --git a/Security_Properties/daa_pnc_charge_authorisation_offline.spthy b/Security_Properties/daa_pnc_charge_authorisation_offline.spthy
index b6ddd57..55b2048 100644
--- a/Security_Properties/daa_pnc_charge_authorisation_offline.spthy
+++ b/Security_Properties/daa_pnc_charge_authorisation_offline.spthy
@@ -6,7 +6,7 @@ Protocol: DAA_PnC
Properties: SR3 - Secure Charge Authorisation (offline)
SR4 - Charge Data Authenticity (offline)
-This Tamarin model is used to verify the security of the charge authorisation
+This Tamarin model is used to verify the security of the charge authorization
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".
@@ -67,13 +67,13 @@ analyzed: daa_pnc_charge_authorisation_offline.spthy
auth_secrecy_cre (all-traces): verified (24 steps)
auth_secrecy_emaid (all-traces): verified (17 steps)
auth_aliveness_charge (all-traces): verified (35 steps)
- auth_weak_agreement_charge (all-traces): verified (125 steps)
- auth_non_injective_agreement_charge (all-traces): verified (125 steps)
- auth_injective_agreement_charge (all-traces): verified (143 steps)
- auth_aliveness_charge_data (all-traces): verified (95 steps)
- auth_weak_agreement_charge_data (all-traces): verified (95 steps)
- auth_non_injective_agreement_charge_data (all-traces): verified (131 steps)
- auth_injective_agreement_charge_data (all-traces): verified (139 steps)
+ auth_weak_agreement_charge (all-traces): verified (112 steps)
+ auth_non_injective_agreement_charge (all-traces): verified (112 steps)
+ auth_injective_agreement_charge (all-traces): verified (118 steps)
+ auth_aliveness_charge_data (all-traces): verified (110 steps)
+ auth_weak_agreement_charge_data (all-traces): verified (110 steps)
+ auth_non_injective_agreement_charge_data (all-traces): verified (146 steps)
+ auth_injective_agreement_charge_data (all-traces): verified (154 steps)
SP3_Unforgeability_Off (all-traces): verified (100 steps)
test_auth_non_injective_agreement_CP_sessKey (all-traces): verified (46 steps)
test_auth_non_injective_agreement_CP (all-traces): verified (47 steps)
@@ -89,9 +89,9 @@ analyzed: daa_pnc_charge_authorisation_offline.spthy
==============================================================================
-real 30m4,204s
-user 145m23,618s
-sys 47m42,781s
+real 25m16,817s
+user 131m36,396s
+sys 38m37,382s
*/
@@ -181,7 +181,7 @@ equations:
calcL_J_cert(
plus(r_cv1,multp(h2,f)), //s
PointG1(H_p(F1(bsn)),F2(bsn)), //J
- H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,Qk_n)))), //h2
+ H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,pkCCsess_n)))), //h2
multp(f,J) //K
)
=
@@ -192,9 +192,9 @@ equations:
// =(r_cv1+h2f)lyrP1-h2(lryfP1)
// =r_cv1lyrP1
- calcE_S_cert(plus(r_cv1,multp(H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,Qk_n)))),f)), //small_s
+ calcE_S_cert(plus(r_cv1,multp(H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,pkCCsess_n)))),f)), //small_s
multp(l,multp(y,multp(r,P1))), //S
- H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,Qk_n)))), //h2
+ H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,pkCCsess_n)))), //h2
multp(l,multp(multp(r,y),multp(f, P1))) //W
)
=
@@ -563,8 +563,8 @@ This is obviously not sensible but allowed.
rule TPM2_CreateDAA:
let
Q=multp(~f, 'P1')
- Q_PD=<'DAA_public_data', Q>
- Q_SD=senc(~f,aes_key)
+ CCdaa_PD=<'DAA_public_data', Q>
+ CCdaa_SD=senc(~f,aes_key)
in
[In_S($AS, $PS, < pke, 'createDAAKey'>)
, !TPM_AES_Key($PS, aes_key)
@@ -574,7 +574,7 @@ rule TPM2_CreateDAA:
, DeriveDAAKey($PS, $AS, pke, ~f)
, OnlyOnce('TPM2_CreateDAA')
]->
- [ Out_S($PS, $AS,< Q_SD,Q_PD, 'returnDAAKey'>),
+ [ Out_S($PS, $AS,< CCdaa_SD,CCdaa_PD, 'returnDAAKey'>),
!TPM_DAA_SK($PS, pke, ~f),
Out(Q)
]
@@ -599,13 +599,13 @@ rule Host_Store_DAA:
let
PC_PD=<'PC_public_data',pk(~pc)>
- m=<pke,pk(~pc), Q_PD, 'join_Issuer_1'>
+ m=<pke,pk(~pc), CCdaa_PD, 'join_Issuer_1'>
in
- [In_S($PS, $AS, < Q_SD,Q_PD, 'returnDAAKey'>)
+ [In_S($PS, $AS, < CCdaa_SD,CCdaa_PD, 'returnDAAKey'>)
, Host_State_02( $PS, $AS, pke, PC_PD, PC_SD )
]
--[
- PlatformSendKeys($PS, $AS, pke, Q_PD, pk(~pc))
+ PlatformSendKeys($PS, $AS, pke, CCdaa_PD, pk(~pc))
, Alive($AS)
, Role('Platform')
, Store_DAA($PS, $AS)
@@ -613,7 +613,7 @@ rule Host_Store_DAA:
]->
[
Out_S_B($AS, $I, <m, 'CPS_Fwd_Req'>) //CPS_I is included as CS and CSO know chosen CPS
- , Host_State_05($PS, $AS, $I, pke, Q_PD, Q_SD)
+ , Host_State_05($PS, $AS, $I, pke, CCdaa_PD, CCdaa_SD)
]
//Issuer: verify the curlyK and the signature before issuing the proper credentials
@@ -622,8 +622,8 @@ rule Issuer_Issue_Credentials:
let
//inputs
Q=multp(f, 'P1')
- Q_PD=<'DAA_public_data', Q>
- m=<pke,pk(pc), Q_PD, 'join_Issuer_1'>
+ CCdaa_PD=<'DAA_public_data', Q>
+ m=<pke,pk(pc), CCdaa_PD, 'join_Issuer_1'>
//inputs from Issuer PK
pkX=PkX(~x,'P2')
@@ -644,7 +644,7 @@ rule Issuer_Issue_Credentials:
s_2_hat='g'^~s_2_dh //pub ecdhe key
s_2_temp=pke^~s_2_dh //Z
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
+ Q_N=<'SHA256',H_SHA256(CCdaa_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)
@@ -686,7 +686,7 @@ rule Issuer_Issue_Credentials:
, Honest ( I )
, Honest ( pke )
, Check_Ek(pke)
- , IssuerReceivedKeys(I, pke, pk(pc), Q_PD)
+ , IssuerReceivedKeys(I, pke, pk(pc), CCdaa_PD)
, IssuerCertDAAKey(I, pke, f)
, Secret_EMAID(I, pke, ~sk_emaid)
, Secret_Cred(I, pke, <A, B, C, D>)
@@ -718,14 +718,14 @@ rule Host_Passthrough_2:
in
[ In_S_B($I, $AS, m)
- , Host_State_05($PS, $AS, $I, pke, Q_PD, Q_SD)
+ , Host_State_05($PS, $AS, $I, pke, CCdaa_PD, CCdaa_SD)
]
--[ Passthrough_ActivateCred2($PS, $AS)
, OnlyOnce('Host_Passthrough_2')
]->
[ Out_S($AS,$PS,< sk_DUP, 'TPM2_Import'>)
- , Out_S($AS,$PS,< Q_SD, Q_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, 'TPM2_ActivateCredentials_2'>)
- , Host_State_06($PS, $AS, pke, Q_SD, Q_PD, C_hat, sk_PD, EMSP_Cert) //activateData
+ , Out_S($AS,$PS,< CCdaa_SD, CCdaa_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, 'TPM2_ActivateCredentials_2'>)
+ , Host_State_06($PS, $AS, pke, CCdaa_SD, CCdaa_PD, C_hat, sk_PD, EMSP_Cert) //activateData
]
//The TPM decrypts the EMAID secret key and returns it to the host/EV
@@ -779,18 +779,18 @@ rule TPM2_ActivateCredential_2:
//unwrap the inputs where needed
curlyK_2_hat=senc(curlyK(K_2),k_e)
Q=multp(~f, 'P1')
- Q_PD=<'DAA_public_data', Q>
+ CCdaa_PD=<'DAA_public_data', Q>
//recompute
s_2_rec_temp=s_2_hat^e //retrieve s
s_2_rec=KDF_e(s_2_rec_temp,'IDENTITY',s_2_hat,pke)
- Q_N_rec=<'SHA256',H_SHA256(Q_PD)> //calculate Q_N_rec which should be the same as Q_N
+ Q_N_rec=<'SHA256',H_SHA256(CCdaa_PD)> //calculate Q_N_rec which should be the same as Q_N
k_e_1=KDF_a(s_2_rec,'STORAGE',Q_N_rec) //calculate k_e_1 which should be the same as k_e
k_h_1=KDF_a(s_2_rec,'INTEGRITY','NULL') //calculate k_h_1 which should be the same as k_h
curlyH_1=MAC(<len16(curlyK_2_hat),curlyK_2_hat,Q_N_rec>,k_h_1)
curlyK_2_rec=sdec(curlyK_2_hat,k_e_1)
in
- [ In_S($AS,$PS,< Q_SD, Q_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, 'TPM2_ActivateCredentials_2'>)
+ [ In_S($AS,$PS,< CCdaa_SD, CCdaa_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, 'TPM2_ActivateCredentials_2'>)
, !TPM_AES_Key($PS, aes_key)
, !TPM_ENDORSEMENT_SK($PS,e, pke)
]
@@ -820,7 +820,7 @@ rule Host_JoinComplete:
//input from Host_State
Q=multp(~f, 'P1')
- Q_PD=<'DAA_public_data', Q>
+ CCdaa_PD=<'DAA_public_data', Q>
C_hat=senc(<A,B,C,D,u,j>,curlyK_2) //we decrypt these credentials by checking that curlyK_2_rec = curlyK_2
//recompute the hash
@@ -830,8 +830,8 @@ rule Host_JoinComplete:
in
[ In_S($PS,$AS, < curlyK_2_rec, 'ret_TPM2_ActivateCredentials_2'>)
, In_S($PS,$AS, < sk_PD, sk_SD, 'ret_TPM2_Import'>)
- , Host_State_06($PS, $AS, pke, Q_SD, Q_PD, C_hat, sk_PD, EMSP_Cert)
- //, Host_State_07($PS, $AS, pke, Q_PD, C_hat, sk_PD, sk_SD, EMSP_Cert)
+ , Host_State_06($PS, $AS, pke, CCdaa_SD, CCdaa_PD, C_hat, sk_PD, EMSP_Cert)
+ //, Host_State_07($PS, $AS, pke, CCdaa_PD, C_hat, sk_PD, sk_SD, EMSP_Cert)
]
--[
Eq(curlyK_2, curlyK_2_rec) //this allows C_hat to be decrypted
@@ -849,7 +849,7 @@ rule Host_JoinComplete:
, Commit_Test(pke, I, ~f)
, OnlyOnce('Host_JoinComplete')
]->
- [ !Host_Store_Credentials($PS, $AS, pke, EMSP_Cert, A, B, C, D, Q_SD, Q_PD, sk_PD, sk_SD)
+ [ !Host_Store_Credentials($PS, $AS, pke, EMSP_Cert, A, B, C, D, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD)
, Host_Org_Creds($PS, $AS, pke, A, B, C, D)
]
@@ -884,13 +884,13 @@ rule EMSP_CSO_Offline_Calc:
let
i_x=h(i_x_t)
- M_id=MAC(<'00', i_x>, ~sk_emaid)
- X1=h(M_id) //id_ix
- idCPix=h(<X1, $CP>)
+ tM_id=MAC(<'00', i_x>, ~sk_emaid)
+ M_id=h(tM_id) //id_ix
+ CPM_id=h(<M_id, $CP>)
M_auth=MAC(<'01',i_x>, ~sk_emaid) //auth_ix
- X2=h(h(<M_auth, ~nonce_ix>))
- authCPix=h(X2)
- localAuth_ix=<idCPix, ~nonce_ix, authCPix>
+ tM_auth=h(<M_auth, ~nonce_ix>)
+ CPM_auth=h(tM_auth)
+ localAuth_ix=<CPM_id, ~nonce_ix, CPM_auth>
in
[ !OutIX(i_x_t)
, !Issuer_EMAID_SK(I, pke, ~sk_emaid)
@@ -898,7 +898,7 @@ rule EMSP_CSO_Offline_Calc:
, Fr(~nonce_ix)
]
--[ EMSP_Offline_Calc(I, pke, ~sk_emaid, i_x)
- , EMSP_Offline_Calc2(I, $CP, pke, X2)
+ , EMSP_Offline_Calc2(I, $CP, pke, tM_auth)
, CertifyOnlyOnce('EMSP_Offline_Calc')
]->
[
@@ -908,8 +908,8 @@ rule EMSP_CSO_Offline_Calc:
rule CP_Start:
let
m=<$CP, ~sid, 'ISO_SID'>
- localAuth_ix=<idCPix, nonce_ix, authCPix>
- localAuth=<I, idCPix, nonce_ix, authCPix>
+ localAuth_ix=<CPM_id, nonce_ix, CPM_auth>
+ localAuth=<I, CPM_id, nonce_ix, CPM_auth>
in
[ Fr(~sid)
, In_A(I, $CP, <localAuth_ix>)
@@ -944,7 +944,7 @@ rule Host_Randomise_Credentials:
//J=PointG1(H_p(s_2_bar),y_2)
in
[
- !Host_Store_Credentials($PS, $AS, pke, EMSP_Cert, A, B, C, D, Q_SD, Q_PD, sk_PD, sk_SD)
+ !Host_Store_Credentials($PS, $AS, pke, EMSP_Cert, A, B, C, D, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD)
, Fr(~l)
]
--[
@@ -954,7 +954,7 @@ rule Host_Randomise_Credentials:
[
//Out_S($AS,$PS,<s_2_bar,y_2,S, 'TPM2_Commit_rand'>)
//, Out_S($AS, $PS, <pke, 'createSessionKey'>)
- !Host_State_08a( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, s_2_bar, y_2)
+ !Host_State_08a( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, s_2_bar, y_2)
, Host_Rnd_Creds($PS, $AS, pke, bsn, R, S, T, W)
]
@@ -971,7 +971,7 @@ rule Host_RandomCredentialsReveal:
//as Host we randomise the credentials
rule Host_Randomise_Credentials2:
[
- !Host_State_08a( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, s_2_bar, y_2)
+ !Host_State_08a( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, s_2_bar, y_2)
]
--[
RandomisedCredentials2($PS, $AS, pke)
@@ -980,7 +980,7 @@ rule Host_Randomise_Credentials2:
[
Out_S($AS,$PS,<s_2_bar,y_2,S, 'TPM2_Commit_rand'>)
, Out_S($AS, $PS, <pke, 'createSessionKey'>)
- , Host_State_08( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD)
+ , Host_State_08( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD)
]
@@ -1015,9 +1015,9 @@ rule TPM2_Commit_2:
rule TPM_Create_Session_Key:
let
kID=DAAKeyID(~keyID) // just a tracker to help Tamarin
- Qk=pk(~g)
- Qk_PD=<'SessionKey_public_data', Qk>
- Qk_SD=senc(~g,aes_key)
+ pkCCsess=pk(~g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ CCsess_SD=senc(~g,aes_key)
in
[In_S($AS, $PS, < pke, 'createSessionKey'>)
, !TPM_AES_Key($PS, aes_key) //our AES key
@@ -1025,24 +1025,24 @@ rule TPM_Create_Session_Key:
, Fr(~keyID) // id to help Tamarin pick the correct response later
]
--[
- TPM2_SessionKey_Created($PS, $AS, kID, Qk_PD)
+ TPM2_SessionKey_Created($PS, $AS, kID, pkCCsess_PD)
, DeriveSessionKey($PS, $AS, ~g)
, CertifyOnlyOnce('Create_Session_Key')
]->
[
- Out_S($PS, $AS,< kID, Qk_SD,Qk_PD, 'createdSessionKey'>)
- , !TPM_Session_SK($PS, pke, Qk, ~g)
+ Out_S($PS, $AS,< kID, CCsess_SD,pkCCsess_PD, 'createdSessionKey'>)
+ , !TPM_Session_SK($PS, pke, pkCCsess, ~g)
]
//simpe rule to leak the Session secret key:
rule TPM_SessionKeyReveal:
- [ !TPM_Session_SK($PS, pke, Qk, ~g) ]
+ [ !TPM_Session_SK($PS, pke, pkCCsess, ~g) ]
--[
KeyReveal('TPM_SessionReveal_tpm', $PS)
, KeyReveal('TPM_SessionReveal_pke', pke)
- , KeyReveal('TPM_SessionReveal_Qk', Qk)
+ , KeyReveal('TPM_SessionReveal_pkCCsess', pkCCsess)
]->
[Out(~g)]
@@ -1058,8 +1058,8 @@ rule Host_Store_Randomised_Credentials:
in*/
[
In_S($PS,$AS, <S, E,cv1val, 'ret_TPM2_Commit_rand'>)
- , In_S($PS, $AS,< kID, Qk_SD,Qk_PD, 'createdSessionKey'>)
- , Host_State_08( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD)
+ , In_S($PS, $AS,< kID, CCsess_SD,pkCCsess_PD, 'createdSessionKey'>)
+ , Host_State_08( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD)
]
--[
@@ -1067,23 +1067,23 @@ rule Host_Store_Randomised_Credentials:
, CertifyOnlyOnce('Host_Store_Randomised_Credentials')
]->
- [ !Host_State_09_a($PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, Q_SD, Q_PD, sk_PD,
- sk_SD, kID, Qk_SD,Qk_PD )
+ [ !Host_State_09_a($PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD,
+ sk_SD, kID, CCsess_SD,pkCCsess_PD )
]
// the host asks the TPM to certify the session key pair with its DAA credential
// and to compute an hmac over the authorization counter using the EMAID secret key
-rule Host_Load_Qk_For_Ceritfication:
+rule Host_Load_pkCCsess_For_Ceritfication:
let
EMSP_Cert=<I,pkX,pkY>
m=<$CP, sid, 'ISO_SID'>
//received values
cv1val=Nonce(cv1) //explicitly stating this prevents partial deconstructions
- Qk=pk(g)
- Qk_PD=<'SessionKey_public_data', Qk>
- // Qk_SD=senc(g,aes_key) //the host needs to store this on behalf of the TPM
+ pkCCsess=pk(g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ // CCsess_SD=senc(g,aes_key) //the host needs to store this on behalf of the TPM
kID=DAAKeyID(keyID)
//existing values
@@ -1106,33 +1106,33 @@ rule Host_Load_Qk_For_Ceritfication:
m_buffer=<'00',i_x>
in
[
- !Host_State_09_a($PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, kID, Qk_SD,Qk_PD )
+ !Host_State_09_a($PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD )
, In(m)
, !OutIX(i_x_t)
]
--[
- LoadKeyForCertification($PS, $AS, kID, Qk_PD)
- , LoadKeyForCertification2($PS, $AS, Qk)
+ LoadKeyForCertification($PS, $AS, kID, pkCCsess_PD)
+ , LoadKeyForCertification2($PS, $AS, pkCCsess)
, AliveEV($PS, $AS, pke)
, OnlyOnce_i_x(pke, I, i_x)
- , CertifyOnlyOnce('Host_Load_Qk_For_Ceritfication')
+ , CertifyOnlyOnce('Host_Load_pkCCsess_For_Ceritfication')
]->
- [ Out_S($AS, $PS, < pke, kID, Qk_SD, Qk_PD, c, cv1val, 'TPM2_Certify'>)
+ [ Out_S($AS, $PS, < pke, kID, CCsess_SD, pkCCsess_PD, c, cv1val, 'TPM2_Certify'>)
, Out_S($AS, $PS, < pke, sk_PD, sk_SD, m_buffer, 'TPM2_HMAC'>)
- , Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, c, sid, $CP, i_x )]
+ , Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, c, sid, $CP, i_x )]
//TPM: receives key, c, cv1 and certifies the Session key with the DAA credential
rule TPM2_Load_And_Certify:
let
- Qk_SD=senc(~g,aes_key) //loaded but not used as such
+ CCsess_SD=senc(~g,aes_key) //loaded but not used as such
kID=DAAKeyID(keyID) //only needed to keep track of multiple calls
- Qk=pk(~g)
- Qk_PD=<'SessionKey_public_data', Qk>
- Qk_n=QName('SHA256',H_SHA256(Qk_PD))
+ pkCCsess=pk(~g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ pkCCsess_n=QName('SHA256',H_SHA256(pkCCsess_PD))
- curlyA=certData('certificationData',Qk_n)
+ curlyA=certData('certificationData',pkCCsess_n)
credData='CredentialData'
c=H_k_7(credData,R,S,T,W,E, sid)
@@ -1142,7 +1142,7 @@ rule TPM2_Load_And_Certify:
small_s=plus(~r_cv1, multp(h2, ~f))
in
[
- In_S($AS, $PS, < pke, kID, Qk_SD, Qk_PD, c, cv1val_in, 'TPM2_Certify'>)
+ In_S($AS, $PS, < pke, kID, CCsess_SD, pkCCsess_PD, c, cv1val_in, 'TPM2_Certify'>)
, !TPM_DAA_SK($PS, pke, ~f)
, !TPM_AES_Key($PS, aes_key) //our AES key
, TPM_Commit_RCV1( $PS, $AS, pke, cv1val, ~r_cv1)
@@ -1150,9 +1150,9 @@ rule TPM2_Load_And_Certify:
]
--[
- TPM2_Created_Cert_TPM($PS, $AS, kID, Qk_PD)
+ TPM2_Created_Cert_TPM($PS, $AS, kID, pkCCsess_PD)
, Eq(cv1val_in, cv1val) //ensures we have the right ~r_cv1
- , TPM_Certify_q($PS, $AS, pke, Qk, ~f)
+ , TPM_Certify_q($PS, $AS, pke, pkCCsess, ~f)
, TPM_Cert_Test2(pke, small_s, ~f)
, CertifyOnlyOnce('TPM2_Load_And_Certify')
]->
@@ -1194,14 +1194,14 @@ rule TPM2_HMAC_Adv:
rule Host_Receive_Certified_Q_k2:
[
In_S($PS, $AS, < kID, curlyA, small_s, n_C, 'ret_TPM2_Certify'>)
- , In_S($PS, $AS, < sk_PD, M_id, 'ret_TPM2_HMAC'>)
- , Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, small_c, sid, $CP, i_x )
+ , In_S($PS, $AS, < sk_PD, tM_id, 'ret_TPM2_HMAC'>)
+ , Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, small_c, sid, $CP, i_x )
]
--[
- Host_Receive_Certified_Q_k2($PS, $AS, Qk_PD)
+ Host_Receive_Certified_Q_k2($PS, $AS, pkCCsess_PD)
, CertifyOnlyOnce('Host_Receive_Certified_Q_k2')
]->
- [ Host_State_10a( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, small_c, sid, $CP, i_x, curlyA, small_s, n_C, M_id ) ]
+ [ Host_State_10a( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, small_c, sid, $CP, i_x, curlyA, small_s, n_C, tM_id ) ]
//Host: completes the signature and sends the PaymentDetailsReq message to the CP
rule Host_Receive_Certified_Q_k:
@@ -1214,11 +1214,11 @@ rule Host_Receive_Certified_Q_k:
/*sk_unique=H_SHA256(<obfuscationValue, sk_emaid>)
sk_PD=<'SK_EMAID_public_data', sk_unique>
- M_id=MAC(m, sk_emaid)*/
+ tM_id=MAC(m, sk_emaid)*/
bsn=BSN('bottom') //basename='bottom'
E=E_S(r_cv1,S)
- //Qk=Q_K(rndKey)
+ //pkCCsess=Q_K(rndKey)
R=multp(sl,A)
S=multp(sl,B)
T=multp(sl,C)
@@ -1226,10 +1226,10 @@ rule Host_Receive_Certified_Q_k:
credData='CredentialData'
kID=DAAKeyID(keyID) //needed to associate the response with the right key
- Qk=pk(g)
- Qk_PD=<'SessionKey_public_data', Qk>
- Qk_n=QName('SHA256',H_SHA256(Qk_PD))
- curlyA=certData('certificationData',Qk_n)
+ pkCCsess=pk(g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ pkCCsess_n=QName('SHA256',H_SHA256(pkCCsess_PD))
+ curlyA=certData('certificationData',pkCCsess_n)
//received value
n_C=Nonce(rnd_n_C)
@@ -1240,17 +1240,17 @@ rule Host_Receive_Certified_Q_k:
//computed values
h1_host=H_k_2(small_c, H_6(curlyA))
h2_host=H_n_2(n_C, h1_host)
- sigma_K=<Qk_PD, curlyA, bsn, R, S, T, W, h2_host, small_s, n_C>
+ sigma_K=<pkCCsess_PD, curlyA, bsn, R, S, T, W, h2_host, small_s, n_C>
in
[
//In_S($PS, $AS, < kID, curlyA, small_s, n_C, 'ret_TPM2_Certify'>)
- //, In_S($PS, $AS, < sk_PD, M_id, 'ret_TPM2_HMAC'>)
- //, Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, small_c, sid, $CP, i_x )
- Host_State_10a( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, small_c, sid, $CP, i_x, curlyA, small_s, n_C, M_id )
+ //, In_S($PS, $AS, < sk_PD, tM_id, 'ret_TPM2_HMAC'>)
+ //, Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, small_c, sid, $CP, i_x )
+ Host_State_10a( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, small_c, sid, $CP, i_x, curlyA, small_s, n_C, tM_id )
]
- --[ Host_Receive_Certified_Q_K($PS, $AS, pke, kID, Qk_PD)
+ --[ Host_Receive_Certified_Q_K($PS, $AS, pke, kID, pkCCsess_PD)
, Host_Sends_Certified_Q_K($PS, $AS, pke, sigma_K)
, Host_Sends_Certified_Q_K2($PS, $AS, pke, sigma_K, g)
, Host_Sends_Certified_Q_K_cred($PS, $AS, pke, R, S, T, W, sigma_K)
@@ -1262,8 +1262,8 @@ rule Host_Receive_Certified_Q_k:
, CertifyOnlyOnce('Host_Receive_Certified_Q_K')
]->
- [Out(<$CP, sid, EMSP_Cert, h(M_id), sigma_K, 'PaymentDetailsReq'>)
- , Host_State_11( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, sid, $CP, i_x )]
+ [Out(<$CP, sid, EMSP_Cert, h(tM_id), sigma_K, 'PaymentDetailsReq'>)
+ , Host_State_11( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, i_x )]
// CP verifies the PaymentDetailsReq message, generates a fresh nonce_ix and sends it
// with the usual V2G PnC nonce to the EV in the PayDetailsRes message
@@ -1278,16 +1278,16 @@ rule CP_Check_TPM_Certificate:
T=multp(sl,C)
W=multp(sl,D)
- Qk=pk(g)
- Qk_PD=<'SessionKey_public_data', Qk>
- Qk_n=QName('SHA256',H_SHA256(Qk_PD))
- curlyA=certData('certificationData',Qk_n)
+ pkCCsess=pk(g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ pkCCsess_n=QName('SHA256',H_SHA256(pkCCsess_PD))
+ curlyA=certData('certificationData',pkCCsess_n)
small_s=plus(r_cv1, multp(h2,f))
n_C=Nonce(rnd_n_C)
credData='CredentialData'
- sigma_K=<Qk_PD, curlyA, bsn_in, R, S, T, W, h2_host, small_s, n_C>
+ sigma_K=<pkCCsess_PD, curlyA, bsn_in, R, S, T, W, h2_host, small_s, n_C>
- localAuth=<I, idCPix, nonce_ix, authCPix>
+ localAuth=<I, CPM_id, nonce_ix, CPM_auth>
//computed values
//E_dash=minus(multp(small_s, S), multp(h2_host, W)) = E
@@ -1302,11 +1302,11 @@ rule CP_Check_TPM_Certificate:
h1_dash=H_k_2(c_dash, H_6(curlyA))
h2_dash=H_n_2(n_C, h1_dash)
- idCPix_in=h(<X1, $CP>)
+ CPM_id_in=h(<M_id, $CP>)
m_out=<$CP, ~sid, ~nonce, nonce_ix, 'PaymentDetailsRes'>
in
- [In(<$CP, ~sid, EMSP_Cert, X1, sigma_K, 'PaymentDetailsReq'>)
+ [In(<$CP, ~sid, EMSP_Cert, M_id, sigma_K, 'PaymentDetailsReq'>)
, !Pk(I, pkX, pkY) // Authentic from EMSP cert
, CP_State_00($CP, ~sid, localAuth)
, Fr(~nonce)]
@@ -1314,7 +1314,7 @@ rule CP_Check_TPM_Certificate:
Eq(check1,accept) //check that h_hat(R,Y)=h_hat(lA,yP2)=h_hat(lyA,P2)=h_hat(lB,P2)=h_hat(S,P2)
, Eq(check2,accept) //check that h_hat(R+W,X)=h_hat(T,P2)
, Eq(h2_dash, h2_host) //ensure that the recomputed hash matches the one provided
- , Eq(idCPix_in, idCPix)
+ , Eq(CPM_id_in, CPM_id)
, VerifiedCertificate($CP, sigma_K)
, VerifiedCertificate2($CP, sigma_K, pk(g), f)
, VerifiedCertificateDeAnonymised(bsn_in, sigma_K, f) //allows us to reason about the secret key used in signatures
@@ -1322,7 +1322,7 @@ rule CP_Check_TPM_Certificate:
]->
[
Out(m_out)
- , CP_State_01($CP, ~sid, I, sigma_K, ~nonce,X1, localAuth)
+ , CP_State_01($CP, ~sid, I, sigma_K, ~nonce,M_id, localAuth)
]
//host receives PaymentDetailsRes message from CP and asks TPM to compute the mac_out
@@ -1334,7 +1334,7 @@ rule Host_Auth:
m_buffer=<'01',i_x>
in
[ In(m),
- Host_State_11( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, sid, $CP, i_x )
+ Host_State_11( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, i_x )
]
--[
Host_Auth($PS, $AS, sid)
@@ -1342,79 +1342,79 @@ rule Host_Auth:
]->
[
Out_S($AS, $PS, < pke, sk_PD, sk_SD, m_buffer, 'TPM2_HMAC'>),
- Host_State_12( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, sid, $CP, nonce, nonce_ix) ]
+ Host_State_12( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, nonce, nonce_ix) ]
// host receives mac from TPM and asks the TPM to sign the charge authorisation request
// with the session key
rule Host_Auth2:
let
- Qk=pk(g)
- Qk_PD=<'SessionKey_public_data', Qk>
- X2=h(h(<M_auth, nonce_ix>))
- authH=h(<'AuthorizationReq', $CP, nonce, X2>)
+ pkCCsess=pk(g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ tM_auth=h(<M_auth, nonce_ix>)
+ authH=h(<'AuthorizationReq', $CP, nonce, tM_auth>)
in
[
In_S($PS, $AS, < sk_PD, M_auth, 'ret_TPM2_HMAC'>),
- Host_State_12( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, sid, $CP, nonce, nonce_ix)
+ Host_State_12( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, nonce, nonce_ix)
]
--[
Host_Auth2($PS, $AS, sid)
, Host_Auth22($PS, $AS, authH)
, CertifyOnlyOnce('Host_Auth2')
]->
- [ Out_S($AS, $PS, < Qk_SD, Qk_PD, authH, 'TPM2_Sign_S'>),
- Host_State_13( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, sid, $CP, nonce, nonce_ix, M_auth)
+ [ Out_S($AS, $PS, < CCsess_SD, pkCCsess_PD, authH, 'TPM2_Sign_S'>),
+ Host_State_13( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, nonce, nonce_ix, M_auth)
]
// TPM signs the authorization request with the session key and returns signature to host
rule TPM2_Sign_SessionKey:
let
- Qk_SD=senc(~g,aes_key)
- Qk=pk(~g)
- Qk_PD=<'SessionKey_public_data', Qk>
+ CCsess_SD=senc(~g,aes_key)
+ pkCCsess=pk(~g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
in
- [ In_S($AS, $PS, < Qk_SD, Qk_PD, hash_in, 'TPM2_Sign_S'>)
+ [ In_S($AS, $PS, < CCsess_SD, pkCCsess_PD, hash_in, 'TPM2_Sign_S'>)
, !TPM_AES_Key($PS, aes_key)
- , !TPM_Session_SK($PS, pke, Qk, ~g)
+ , !TPM_Session_SK($PS, pke, pkCCsess, ~g)
]
--[
- TPM2_Sign_S($PS, $AS, Qk_PD)
- , TPM2_Sign_S2($PS, $AS, Qk_PD, hash_in)
+ TPM2_Sign_S($PS, $AS, pkCCsess_PD)
+ , TPM2_Sign_S2($PS, $AS, pkCCsess_PD, hash_in)
, CertifyOnlyOnce(<'TPM2_Sign_SessionKey', hash_in>)
]->
- [Out_S($PS, $AS, < Qk_PD, sign(hash_in,~g), 'ret_TPM2_Sign_S'>)]
+ [Out_S($PS, $AS, < pkCCsess_PD, sign(hash_in,~g), 'ret_TPM2_Sign_S'>)]
// host receives signature for authorization request from TPM and sends the
// signed authorization request to the CP
rule Host_Auth3:
let
EMSP_Cert=<I,pkX,pkY>
- Qk=pk(g)
- Qk_PD=<'SessionKey_public_data', Qk>
+ pkCCsess=pk(g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
/*sk_unique=H_SHA256(<obfuscationValue, sk_emaid>)
sk_PD=<'SK_EMAID_public_data', sk_unique>
M_auth=MAC(m, sk_emaid)*/
- X2=h(h(<M_auth, nonce_ix>))
- authH=h(<'AuthorizationReq', $CP, nonce, X2>)
+ tM_auth=h(<M_auth, nonce_ix>)
+ authH=h(<'AuthorizationReq', $CP, nonce, tM_auth>)
in
- [ In_S($PS,$AS, < Qk_PD, sig_over_auth, 'ret_TPM2_Sign_S'>),
- Host_State_13( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, sid, $CP, nonce, nonce_ix, M_auth)
+ [ In_S($PS,$AS, < pkCCsess_PD, sig_over_auth, 'ret_TPM2_Sign_S'>),
+ Host_State_13( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, nonce, nonce_ix, M_auth)
]
--[
- Eq(verify(sig_over_auth,authH,Qk), true) //TPM response is for prev call
+ Eq(verify(sig_over_auth,authH,pkCCsess), true) //TPM response is for prev call
, Host_Auth3($PS, $AS, sid)
//, CounterH(i_x_t)
, RunningEV_Sign( pke , $CP, authH )
, RunningEV_Sign2( $PS, $AS, $CP, authH )
- , RunningEV_Sign3( $PS, $AS, $CP, authH, Qk, sig_over_auth )
+ , RunningEV_Sign3( $PS, $AS, $CP, authH, pkCCsess, sig_over_auth )
, RunningEV_Auth( $PS, $AS, pke, I, M_auth )
- , RunningEV_Auth2( $PS, $AS, pke, I, M_auth, Qk_PD )
+ , RunningEV_Auth2( $PS, $AS, pke, I, M_auth, pkCCsess_PD )
, CertifyOnlyOnce('Host_Auth3')
]->
- [ Out(<sid, authH, sig_over_auth, X2, 'AuthorizationReq'>)
- , !Host_State_14( $PS, $AS, pke, EMSP_Cert, kID, Qk_SD,Qk_PD, sid, $CP, M_auth)
+ [ Out(<sid, authH, sig_over_auth, tM_auth, 'AuthorizationReq'>)
+ , !Host_State_14( $PS, $AS, pke, EMSP_Cert, kID, CCsess_SD,pkCCsess_PD, sid, $CP, M_auth)
]
//=============================================================
@@ -1431,61 +1431,61 @@ rule CP_Verify:
T=multp(sl,C)
W=multp(sl,D)
- Qk=pk(g)
- Qk_PD=<'SessionKey_public_data', Qk>
- Qk_n=QName('SHA256',H_SHA256(Qk_PD))
- curlyA=certData('certificationData',Qk_n)
+ pkCCsess=pk(g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ pkCCsess_n=QName('SHA256',H_SHA256(pkCCsess_PD))
+ curlyA=certData('certificationData',pkCCsess_n)
small_s=plus(r_cv1, multp(h2,f))
n_C=Nonce(rnd_n_C)
- sigma_K=<Qk_PD, curlyA, bsn_in, R, S, T, W, h2_host, small_s, n_C>
+ sigma_K=<pkCCsess_PD, curlyA, bsn_in, R, S, T, W, h2_host, small_s, n_C>
- localAuth=<I, idCPix, nonce_ix, authCPix>
+ localAuth=<I, CPM_id, nonce_ix, CPM_auth>
- m_in=<~sid, authH_in, sig_over_auth, X2, 'AuthorizationReq'>
+ m_in=<~sid, authH_in, sig_over_auth, tM_auth, 'AuthorizationReq'>
- authCPix_in=h(X2)
- authH=h(<'AuthorizationReq', $CP, ~nonce, X2>)
+ CPM_auth_in=h(tM_auth)
+ authH=h(<'AuthorizationReq', $CP, ~nonce, tM_auth>)
- m_out=<X1, nonce_ix, X2, Qk>
+ m_out=<M_id, nonce_ix, tM_auth, pkCCsess>
in
[ In(m_in)
- , CP_State_01($CP, ~sid, I, sigma_K, ~nonce, X1, localAuth)
+ , CP_State_01($CP, ~sid, I, sigma_K, ~nonce, M_id, localAuth)
]
--[
Eq(authH_in, authH)
- , Eq(verify(sig_over_auth,authH,Qk), true)
- , Eq(authCPix_in, authCPix)
+ , Eq(verify(sig_over_auth,authH,pkCCsess), true)
+ , Eq(CPM_auth_in, CPM_auth)
, CP_Verify($CP, ~sid)
- , CommitCP($CP, Qk, authH)
- , CommitCP2($CP, Qk, authH, sig_over_auth)
- , CommitCP3($CP, I, X2, Qk)
+ , CommitCP($CP, pkCCsess, authH)
+ , CommitCP2($CP, pkCCsess, authH, sig_over_auth)
+ , CommitCP3($CP, I, tM_auth, pkCCsess)
, Honest(I)
, Honest($CP)
, CertifyOnlyOnce('CP_Verify')
]->
[ Out(<I, <m_out, 'EMSP_Auth'>>)
- , !CP_State_02($CP, ~sid, I, Qk, X2) ]
+ , !CP_State_02($CP, ~sid, I, pkCCsess, tM_auth) ]
// the eMSP verifies the authorization request
rule EMSP_Auth:
let
i_x=h(i_x_t)
- m=<X1_in, nonce_ix, X2_in, Qk>
- Qk_PD=<'SessionKey_public_data', Qk>
+ m=<M_id_in, nonce_ix, tM_auth_in, pkCCsess>
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
- M_id=MAC(<'00', i_x>, ~sk_emaid)
- X1=h(M_id)
+ tM_id=MAC(<'00', i_x>, ~sk_emaid)
+ M_id=h(tM_id)
M_auth=MAC(<'01',i_x>, ~sk_emaid)
- X2=h(h(<M_auth, nonce_ix>))
+ tM_auth=h(<M_auth, nonce_ix>)
in
[ In(<I, <m, 'EMSP_Auth'>>)
, !OutIX(i_x_t)
, !Issuer_EMAID_SK(I, pke, ~sk_emaid)
]
- --[ Eq(X1, X1_in)
- , Eq(X2, X2_in)
+ --[ Eq(M_id, M_id_in)
+ , Eq(tM_auth, tM_auth_in)
, CommitEMSP(I, pke, M_auth)
- , CommitEMSP2(I, pke, M_auth, Qk_PD)
+ , CommitEMSP2(I, pke, M_auth, pkCCsess_PD)
, CommitEMSP_sk(I, pke, ~sk_emaid)
, CommitEMSP_sk2(I, pke, M_auth, ~sk_emaid)
, Honest(I)
@@ -1494,7 +1494,7 @@ rule EMSP_Auth:
, CertifyOnlyOnce('EMSP_Auth')
]->
[
- !Issuer_State_Charge(I, pke, ~sk_emaid, i_x, M_auth, Qk)
+ !Issuer_State_Charge(I, pke, ~sk_emaid, i_x, M_auth, pkCCsess)
]
// the CP sends the charge data to the vehicle for attestation
@@ -1503,14 +1503,14 @@ rule CP_DataSend:
data=<$CP, ~sid, 'charge_data',~dataID>
in
[ Fr(~dataID)
- , !CP_State_02($CP, ~sid, I, Qk, X2)
+ , !CP_State_02($CP, ~sid, I, pkCCsess, tM_auth)
]
--[
CP_DataSend($CP, ~sid, ~dataID),
CertifyOnlyOnce('CP_DataSend')
]->
[ Out(data)
- , CP_State_03($CP, ~sid, I, Qk, X2, ~dataID) ]
+ , CP_State_03($CP, ~sid, I, pkCCsess, tM_auth, ~dataID) ]
// the EV (using its TPM) signs the charge data together with ev_h, a hash over the authorisation
// value used during charge authorisation and its public session key to bind them
@@ -1518,22 +1518,22 @@ rule CP_DataSend:
rule EV_DataSign:
let
EMSP_Cert=<I,pkX,pkY>
- Qk=pk(~g)
- Qk_PD=<'SessionKey_public_data', Qk>
+ pkCCsess=pk(~g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
data=<$CP, sid, 'charge_data',dataID>
- ev_h=h(<M_auth,Qk>)
+ ev_h=h(<'EV_h',M_auth,pkCCsess>)
dataTBS=h(<'charge_data',dataID, ev_h>)
in
[ In(data)
- , !Host_State_14( $PS, $AS, pke, EMSP_Cert, kID, Qk_SD,Qk_PD, sid, $CP, M_auth)
+ , !Host_State_14( $PS, $AS, pke, EMSP_Cert, kID, CCsess_SD,pkCCsess_PD, sid, $CP, M_auth)
]
- --[ EV_DataSign($PS, $AS, kID, Qk_PD, sid, dataID)
+ --[ EV_DataSign($PS, $AS, kID, pkCCsess_PD, sid, dataID)
, CertifyOnlyOnce('EV_DataSign')
]->
- [ Out_S($AS, $PS, < Qk_SD, Qk_PD, dataTBS, 'TPM2_Sign_S'>)
- , Host_State_15( $PS, $AS, pke, EMSP_Cert, kID, Qk_SD,Qk_PD, sid, $CP, M_auth, data, dataTBS)
+ [ Out_S($AS, $PS, < CCsess_SD, pkCCsess_PD, dataTBS, 'TPM2_Sign_S'>)
+ , Host_State_15( $PS, $AS, pke, EMSP_Cert, kID, CCsess_SD,pkCCsess_PD, sid, $CP, M_auth, data, dataTBS)
]
// the EV receives the signed charge data from the TPM, sends the signature
@@ -1541,24 +1541,24 @@ rule EV_DataSign:
rule EV_DataSign_Send:
let
EMSP_Cert=<I,pkX,pkY>
- Qk=pk(~g)
- Qk_PD=<'SessionKey_public_data', Qk>
+ pkCCsess=pk(~g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
data=<$CP, sid, 'charge_data',dataID>
- ev_h=h(<M_auth,Qk>)
+ ev_h=h(<'EV_h',M_auth,pkCCsess>)
dataTBS=h(<'charge_data',dataID, ev_h>)
m_out=<ev_h, dataTBS, dataSig>
m_o2=<'charge_data',dataID, dataSig, ev_h>
in
- [ In_S($PS, $AS, < Qk_PD, dataSig, 'ret_TPM2_Sign_S'>)
- , Host_State_15( $PS, $AS, pke, EMSP_Cert, kID, Qk_SD,Qk_PD, sid, $CP, M_auth, data, dataTBS)
+ [ In_S($PS, $AS, < pkCCsess_PD, dataSig, 'ret_TPM2_Sign_S'>)
+ , Host_State_15( $PS, $AS, pke, EMSP_Cert, kID, CCsess_SD,pkCCsess_PD, sid, $CP, M_auth, data, dataTBS)
]
--[
- Eq(verify(dataSig,dataTBS,Qk), true), //TPM response is for prev call
- EV_DataSign_Send($PS, $AS, kID, Qk_PD, sid, dataID),
- EV_DataSign_Send2($PS, $AS, Qk),
+ Eq(verify(dataSig,dataTBS,pkCCsess), true), //TPM response is for prev call
+ EV_DataSign_Send($PS, $AS, kID, pkCCsess_PD, sid, dataID),
+ EV_DataSign_Send2($PS, $AS, pkCCsess),
RunningEV_Data($PS, $AS, pke, I, <M_auth, 'charge_data', dataID>),
RunningEV_Data2(pke, I, <M_auth, 'charge_data', dataID>),
RunningEV_Data3($PS, $AS, $CP, dataTBS),
@@ -1575,19 +1575,19 @@ rule CP_DataRec:
dataTBS=h(<'charge_data',~dataID, ev_h>)
M_auth=MAC(<'01',i_x>, sk_emaid)
- X2=h(h(<M_auth, nonce_ix>))
+ tM_auth=h(<M_auth, nonce_ix>)
m_out=<'charge_data',~dataID, dataSig, ev_h>
in
[ In(m_in)
- , CP_State_03($CP, ~sid, I, Qk, X2, ~dataID)
+ , CP_State_03($CP, ~sid, I, pkCCsess, tM_auth, ~dataID)
]
--[
Eq(dataTBS_in, dataTBS)
- , Eq(verify(dataSig,dataTBS,Qk), true)
+ , Eq(verify(dataSig,dataTBS,pkCCsess), true)
, CP_DataRec($CP, ~sid, ~dataID)
- , CP_DataRec2($CP, Qk, sk_emaid)
- , CP_DataRec3($CP, Qk, dataTBS)
+ , CP_DataRec2($CP, pkCCsess, sk_emaid)
+ , CP_DataRec3($CP, pkCCsess, dataTBS)
, Honest(I)
, CertifyOnlyOnce('CP_DataRec')
]->
@@ -1601,19 +1601,19 @@ rule EMSP_Data:
M_auth=MAC(<'01',i_x>, ~sk_emaid)
m=<'charge_data',dataID, dataSig, ev_h_in>
- Qk_PD=<'SessionKey_public_data', Qk>
- ev_h=h(<M_auth,Qk>)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ ev_h=h(<'EV_h',M_auth,pkCCsess>)
dataTBS=h(<'charge_data', dataID, ev_h>)
in
[ In(<I, <m, 'EMSP_Data'>>)
- , !Issuer_State_Charge(I, pke, ~sk_emaid, i_x, M_auth, Qk)
+ , !Issuer_State_Charge(I, pke, ~sk_emaid, i_x, M_auth, pkCCsess)
]
--[ Eq(ev_h, ev_h_in)
- , Eq(verify(dataSig,dataTBS,Qk), true)
+ , Eq(verify(dataSig,dataTBS,pkCCsess), true)
, Honest(I)
, Honest(pke)
, CommitEMSP_Data(I, pke, <M_auth, 'charge_data', dataID>)
- , CommitEMSP_Data2(I, pke, <M_auth, 'charge_data', dataID>, Qk_PD)
+ , CommitEMSP_Data2(I, pke, <M_auth, 'charge_data', dataID>, pkCCsess_PD)
, OnlyOnce_i_x(I, M_auth, dataID)
, CertifyOnlyOnce('EMSP_Data')
]->
@@ -1675,7 +1675,7 @@ lemma restriction_one_tpm_per_host:
// any endorsement key that is presented to the issuer must have been generated
// by a TPM. This restrictions represents the fact that the issuer will check
// each endorsement key and only allow ones that were created by a TPM
-lemma restricition_pke_comes_from_tpm:
+lemma restriction_pke_comes_from_tpm:
"All pke #i .
Check_Ek(pke) @ i
==>
@@ -1987,7 +1987,7 @@ lemma correctness_charge_authorisation_req_1: exists-trace
#t20
#t21 #t22
//certify steps
- kID Qk_PD sigma
+ kID pkCCsess_PD sigma
#t23 #t24 #t25 #t26 #t27 #t28
.
@@ -2019,7 +2019,7 @@ lemma correctness_charge_authorisation_req_1: exists-trace
//stored the DAA key with the host
//& Store_Keys(TPM, Host) @ t10
- //check the EK and Q_PD as the issuer
+ //check the EK and CCdaa_PD as the issuer
& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t12
@@ -2035,11 +2035,11 @@ lemma correctness_charge_authorisation_req_1: exists-trace
& TPMCommitRandomised(TPM, Host, pke) @ t24
- & TPM2_SessionKey_Created(TPM, Host, kID, Qk_PD) @ t25
+ & TPM2_SessionKey_Created(TPM, Host, kID, pkCCsess_PD) @ t25
- & LoadKeyForCertification(TPM, Host, kID, Qk_PD) @ t26
+ & LoadKeyForCertification(TPM, Host, kID, pkCCsess_PD) @ t26
- & TPM2_Created_Cert_TPM(TPM, Host, kID, Qk_PD) @ t27
+ & TPM2_Created_Cert_TPM(TPM, Host, kID, pkCCsess_PD) @ t27
& Host_Sends_Certified_Q_K(TPM, Host, pke, sigma) @ t28
@@ -2077,7 +2077,7 @@ lemma correctness_charge_authorisation_req_2: exists-trace
#t12 // #t14 #t15 #t16 #t17 #t18 #t19
#t20 #t21 #t22
//certify and verify steps
- kID Qk_PD sigma CP
+ kID pkCCsess_PD sigma CP
#t23 #t24 #t25 #t26 #t27 #t28 #t29
.
@@ -2109,7 +2109,7 @@ lemma correctness_charge_authorisation_req_2: exists-trace
//stored the DAA key with the host
//& Store_Keys(TPM, Host) @ t10
- //check the EK and Q_PD as the issuer
+ //check the EK and CCdaa_PD as the issuer
& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t12
@@ -2125,11 +2125,11 @@ lemma correctness_charge_authorisation_req_2: exists-trace
& TPMCommitRandomised(TPM, Host, pke) @ t24
- & TPM2_SessionKey_Created(TPM, Host, kID, Qk_PD) @ t25
+ & TPM2_SessionKey_Created(TPM, Host, kID, pkCCsess_PD) @ t25
- & LoadKeyForCertification(TPM, Host, kID, Qk_PD) @ t26
+ & LoadKeyForCertification(TPM, Host, kID, pkCCsess_PD) @ t26
- & TPM2_Created_Cert_TPM(TPM, Host, kID, Qk_PD) @ t27
+ & TPM2_Created_Cert_TPM(TPM, Host, kID, pkCCsess_PD) @ t27
& Host_Sends_Certified_Q_K(TPM, Host, pke, sigma) @ t28
@@ -2172,7 +2172,7 @@ lemma correctness_charge_authorisation: exists-trace
#t12 // #t14 #t15 #t16 #t17 #t18 #t19
#t20 #t21 #t22
//certify and verify steps
- kID Qk_PD sigma
+ kID pkCCsess_PD sigma
#t23 #t24 #t25 #t26 #t27 #t28 #t29
CP sid #t01_2
sk_emaid
@@ -2209,7 +2209,7 @@ lemma correctness_charge_authorisation: exists-trace
//stored the DAA key with the host
//& Store_Keys(TPM, Host) @ t10
- //check the EK and Q_PD as the issuer
+ //check the EK and CCdaa_PD as the issuer
& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t12
@@ -2225,11 +2225,11 @@ lemma correctness_charge_authorisation: exists-trace
& TPMCommitRandomised(TPM, Host, pke) @ t24
- & TPM2_SessionKey_Created(TPM, Host, kID, Qk_PD) @ t25
+ & TPM2_SessionKey_Created(TPM, Host, kID, pkCCsess_PD) @ t25
- & LoadKeyForCertification(TPM, Host, kID, Qk_PD) @ t26
+ & LoadKeyForCertification(TPM, Host, kID, pkCCsess_PD) @ t26
- & TPM2_Created_Cert_TPM(TPM, Host, kID, Qk_PD) @ t27
+ & TPM2_Created_Cert_TPM(TPM, Host, kID, pkCCsess_PD) @ t27
& Host_Sends_Certified_Q_K(TPM, Host, pke, sigma) @ t28
@@ -2239,7 +2239,7 @@ lemma correctness_charge_authorisation: exists-trace
& Host_Auth(TPM, Host, sid) @ t30
& TPM_HMAC(TPM, Host, pke, sk_emaid) @ t31
& Host_Auth2(TPM, Host, sid) @ t32
- & TPM2_Sign_S(TPM, Host, Qk_PD) @ t33
+ & TPM2_Sign_S(TPM, Host, pkCCsess_PD) @ t33
& RunningEV_Auth(TPM, Host, pke, I, M_auth ) @ t34
& CP_Verify(CP, sid) @t35
& CommitEMSP(I, pke, M_auth) @t36
@@ -2287,7 +2287,7 @@ lemma correctness_charge_data_authentication: exists-trace
#t12 // #t14 #t15 #t16 #t17 #t18 #t19
#t20 #t21 #t22
//certify and verify steps
- kID Qk_PD sigma
+ kID pkCCsess_PD sigma
#t23 #t24 #t25 #t26 #t27 #t28 #t29
CP sid #t01_2
sk_emaid
@@ -2326,7 +2326,7 @@ lemma correctness_charge_data_authentication: exists-trace
//stored the DAA key with the host
//& Store_Keys(TPM, Host) @ t10
- //check the EK and Q_PD as the issuer
+ //check the EK and CCdaa_PD as the issuer
& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t12
@@ -2342,11 +2342,11 @@ lemma correctness_charge_data_authentication: exists-trace
& TPMCommitRandomised(TPM, Host, pke) @ t24
- & TPM2_SessionKey_Created(TPM, Host, kID, Qk_PD) @ t25
+ & TPM2_SessionKey_Created(TPM, Host, kID, pkCCsess_PD) @ t25
- & LoadKeyForCertification(TPM, Host, kID, Qk_PD) @ t26
+ & LoadKeyForCertification(TPM, Host, kID, pkCCsess_PD) @ t26
- & TPM2_Created_Cert_TPM(TPM, Host, kID, Qk_PD) @ t27
+ & TPM2_Created_Cert_TPM(TPM, Host, kID, pkCCsess_PD) @ t27
& Host_Sends_Certified_Q_K(TPM, Host, pke, sigma) @ t28
@@ -2356,15 +2356,15 @@ lemma correctness_charge_data_authentication: exists-trace
& Host_Auth(TPM, Host, sid) @ t30
& TPM_HMAC(TPM, Host, pke, sk_emaid) @ t31
& Host_Auth2(TPM, Host, sid) @ t32
- & TPM2_Sign_S(TPM, Host, Qk_PD) @ t33
+ & TPM2_Sign_S(TPM, Host, pkCCsess_PD) @ t33
& RunningEV_Auth(TPM, Host, pke, I, M_auth ) @ t34
& CP_Verify(CP, sid) @t35
& CommitEMSP(I, pke, M_auth) @t36
& CP_DataSend(CP, sid, dataID) @t37
- & EV_DataSign(TPM, Host, kID, Qk_PD, sid, dataID) @t38
- & TPM2_Sign_S(TPM, Host, Qk_PD) @t39
- & EV_DataSign_Send(TPM, Host, kID, Qk_PD, sid, dataID) @t40
+ & EV_DataSign(TPM, Host, kID, pkCCsess_PD, sid, dataID) @t38
+ & TPM2_Sign_S(TPM, Host, pkCCsess_PD) @t39
+ & EV_DataSign_Send(TPM, Host, kID, pkCCsess_PD, sid, dataID) @t40
& CP_DataRec(CP, sid, dataID) @t41
& CommitEMSP_Data(I, pke, <M_auth, 'charge_data', dataID>) @t42
@@ -2417,7 +2417,7 @@ lemma correctness_with_adv: exists-trace
#t12 // #t14 #t15 #t16 #t17 #t18 #t19
#t20 #t21 #t22
//certify and verify steps
- kID Qk_PD
+ kID pkCCsess_PD
#t23 #t24 #t25 #t26 #t27 #t28
sid sk_emaid
#t30 #t31 #t32 #t33 #t34 #t36
@@ -2453,7 +2453,7 @@ lemma correctness_with_adv: exists-trace
//stored the DAA key with the host
//& Store_Keys(TPM, Host) @ t10
- //check the EK and Q_PD as the issuer
+ //check the EK and CCdaa_PD as the issuer
& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t12
@@ -2469,26 +2469,26 @@ lemma correctness_with_adv: exists-trace
& TPMCommitRandomised(TPM, Host, pke) @ t24
- & TPM2_SessionKey_Created(TPM, Host, kID, Qk_PD) @ t25
+ & TPM2_SessionKey_Created(TPM, Host, kID, pkCCsess_PD) @ t25
- & LoadKeyForCertification(TPM, Host, kID, Qk_PD) @ t26
+ & LoadKeyForCertification(TPM, Host, kID, pkCCsess_PD) @ t26
- & TPM2_Created_Cert_TPM(TPM, Host, kID, Qk_PD) @ t27
+ & TPM2_Created_Cert_TPM(TPM, Host, kID, pkCCsess_PD) @ t27
- & Host_Receive_Certified_Q_K(TPM, Host, pke, kID, Qk_PD) @ t28
+ & Host_Receive_Certified_Q_K(TPM, Host, pke, kID, pkCCsess_PD) @ t28
& Host_Auth(TPM, Host, sid) @ t30
& TPM_HMAC(TPM, Host, pke, sk_emaid) @ t31
& Host_Auth2(TPM, Host, sid) @ t32
- & TPM2_Sign_S(TPM, Host, Qk_PD) @ t33
- & RunningEV_Auth2(TPM, Host, pke, I, M_auth, Qk_PD ) @ t34
- & CommitEMSP2(I, pke, M_auth, Qk_PD) @t36
+ & TPM2_Sign_S(TPM, Host, pkCCsess_PD) @ t33
+ & RunningEV_Auth2(TPM, Host, pke, I, M_auth, pkCCsess_PD ) @ t34
+ & CommitEMSP2(I, pke, M_auth, pkCCsess_PD) @t36
- & EV_DataSign(TPM, Host, kID, Qk_PD, sid, dataID) @t38
- & TPM2_Sign_S(TPM, Host, Qk_PD) @t39
- & EV_DataSign_Send(TPM, Host, kID, Qk_PD, sid, dataID) @t40
- & CommitEMSP_Data2(I, pke, <M_auth, 'charge_data', dataID>, Qk_PD) @t42
+ & EV_DataSign(TPM, Host, kID, pkCCsess_PD, sid, dataID) @t38
+ & TPM2_Sign_S(TPM, Host, pkCCsess_PD) @t39
+ & EV_DataSign_Send(TPM, Host, kID, pkCCsess_PD, sid, dataID) @t40
+ & CommitEMSP_Data2(I, pke, <M_auth, 'charge_data', dataID>, pkCCsess_PD) @t42
& t01<t02 //Issuer gets created before CPS
& t02<t04 //Host gets created before Bind
@@ -2529,7 +2529,6 @@ lemma correctness_with_adv: exists-trace
-
//======================================================================================
// In the following section we look at the security properties for
// the charge authorization and charge data authorization in our model
@@ -2934,8 +2933,6 @@ lemma SP3_Unforgeability_Off [heuristic=o]:
"
-
-
//------------------
/*
test_auth_non_injective_agreement_CP_sessKey (all-traces): verified (39 steps)
@@ -3144,10 +3141,10 @@ All CP g dataTBS TPM Host #i #i2 .
lemma test_auth_injective_agreement_CP_test2 [heuristic=o]:
"
-All CP Iss X2 g TPM Host #i #i2 .
+All CP Iss tM_auth g TPM Host #i #i2 .
(
(
- CommitCP3( CP, Iss, X2, pk(g)) @ i
+ CommitCP3( CP, Iss, tM_auth, pk(g)) @ i
&
DeriveSessionKey(TPM, Host, g) @ i2
)
@@ -3155,13 +3152,13 @@ All CP Iss X2 g TPM Host #i #i2 .
(
// Implies there exists a running issuer on the same term
(
- Ex pke #j . EMSP_Offline_Calc2(Iss, CP, pke, X2) @ j
+ Ex pke #j . EMSP_Offline_Calc2(Iss, CP, pke, tM_auth) @ j
&
(#j<#i)
&
// And each commited JOIN session corresponds to a unique issuer run
( not(
- Ex CP2 Iss2 g2 #i3 . ( CommitCP3( CP2, Iss2, X2, pk(g2)) @ i3 & not(#i3=#i)
+ Ex CP2 Iss2 g2 #i3 . ( CommitCP3( CP2, Iss2, tM_auth, pk(g2)) @ i3 & not(#i3=#i)
&
not(Ex RevealEvent Entity #kr . KeyReveal(RevealEvent, Entity) @ kr & Honest(Entity) @ i3))
)
diff --git a/Security_Properties/daa_pnc_charge_authorisation_online.spthy b/Security_Properties/daa_pnc_charge_authorisation_online.spthy
index 21116b9..9d40817 100644
--- a/Security_Properties/daa_pnc_charge_authorisation_online.spthy
+++ b/Security_Properties/daa_pnc_charge_authorisation_online.spthy
@@ -6,7 +6,7 @@ Protocol: DAA_PnC
Properties: SR3 - Secure Charge Authorisation (online)
SR4 - Charge Data Authenticity (online)
-This Tamarin model is used to verify the security of the charge authorisation
+This Tamarin model is used to verify the security of the charge authorization
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".
@@ -66,20 +66,20 @@ analyzed: daa_pnc_charge_authorisation_online.spthy
auth_secrecy_cre (all-traces): verified (24 steps)
auth_secrecy_emaid (all-traces): verified (17 steps)
auth_aliveness_charge (all-traces): verified (35 steps)
- auth_weak_agreement_charge (all-traces): verified (125 steps)
- auth_non_injective_agreement_charge (all-traces): verified (125 steps)
- auth_injective_agreement_charge (all-traces): verified (143 steps)
- auth_aliveness_charge_data (all-traces): verified (95 steps)
- auth_weak_agreement_charge_data (all-traces): verified (95 steps)
- auth_non_injective_agreement_charge_data (all-traces): verified (131 steps)
- auth_injective_agreement_charge_data (all-traces): verified (139 steps)
+ auth_weak_agreement_charge (all-traces): verified (112 steps)
+ auth_non_injective_agreement_charge (all-traces): verified (112 steps)
+ auth_injective_agreement_charge (all-traces): verified (118 steps)
+ auth_aliveness_charge_data (all-traces): verified (110 steps)
+ auth_weak_agreement_charge_data (all-traces): verified (110 steps)
+ auth_non_injective_agreement_charge_data (all-traces): verified (146 steps)
+ auth_injective_agreement_charge_data (all-traces): verified (154 steps)
SP3_Unforgeability (all-traces): verified (36 steps)
==============================================================================
-real 23m53,797s
-user 106m6,863s
-sys 36m55,826s
+real 18m55,553s
+user 90m15,520s
+sys 27m49,332s
*/
@@ -169,7 +169,7 @@ equations:
calcL_J_cert(
plus(r_cv1,multp(h2,f)), //s
PointG1(H_p(F1(bsn)),F2(bsn)), //J
- H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,Qk_n)))), //h2
+ H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,pkCCsess_n)))), //h2
multp(f,J) //K
)
=
@@ -180,9 +180,9 @@ equations:
// =(r_cv1+h2f)lyrP1-h2(lryfP1)
// =r_cv1lyrP1
- calcE_S_cert(plus(r_cv1,multp(H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,Qk_n)))),f)), //small_s
+ calcE_S_cert(plus(r_cv1,multp(H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,pkCCsess_n)))),f)), //small_s
multp(l,multp(y,multp(r,P1))), //S
- H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,Qk_n)))), //h2
+ H_n_2(n_C, H_k_2(small_c, H_6(certData(certificationData,pkCCsess_n)))), //h2
multp(l,multp(multp(r,y),multp(f, P1))) //W
)
=
@@ -527,8 +527,8 @@ This is obviously not sensible but allowed.
rule TPM2_CreateDAA:
let
Q=multp(~f, 'P1')
- Q_PD=<'DAA_public_data', Q>
- Q_SD=senc(~f,aes_key)
+ CCdaa_PD=<'DAA_public_data', Q>
+ CCdaa_SD=senc(~f,aes_key)
in
[In_S($AS, $PS, < pke, 'createDAAKey'>)
, !TPM_AES_Key($PS, aes_key)
@@ -538,7 +538,7 @@ rule TPM2_CreateDAA:
, DeriveDAAKey($PS, $AS, pke, ~f)
, OnlyOnce('TPM2_CreateDAA')
]->
- [ Out_S($PS, $AS,< Q_SD,Q_PD, 'returnDAAKey'>),
+ [ Out_S($PS, $AS,< CCdaa_SD,CCdaa_PD, 'returnDAAKey'>),
!TPM_DAA_SK($PS, pke, ~f),
Out(Q)
]
@@ -563,13 +563,13 @@ rule Host_Store_DAA:
let
PC_PD=<'PC_public_data',pk(~pc)>
- m=<pke,pk(~pc), Q_PD, 'join_Issuer_1'>
+ m=<pke,pk(~pc), CCdaa_PD, 'join_Issuer_1'>
in
- [In_S($PS, $AS, < Q_SD,Q_PD, 'returnDAAKey'>)
+ [In_S($PS, $AS, < CCdaa_SD,CCdaa_PD, 'returnDAAKey'>)
, Host_State_02( $PS, $AS, pke, PC_PD, PC_SD )
]
--[
- PlatformSendKeys($PS, $AS, pke, Q_PD, pk(~pc))
+ PlatformSendKeys($PS, $AS, pke, CCdaa_PD, pk(~pc))
, Alive($AS)
, Role('Platform')
, Store_DAA($PS, $AS)
@@ -577,7 +577,7 @@ rule Host_Store_DAA:
]->
[
Out_S_B($AS, $I, <m, 'CPS_Fwd_Req'>) //CPS_I is included as CS and CSO know chosen CPS
- , Host_State_05($PS, $AS, $I, pke, Q_PD, Q_SD)
+ , Host_State_05($PS, $AS, $I, pke, CCdaa_PD, CCdaa_SD)
]
//Issuer: verify the curlyK and the signature before issuing the proper credentials
@@ -586,8 +586,8 @@ rule Issuer_Issue_Credentials:
let
//inputs
Q=multp(f, 'P1')
- Q_PD=<'DAA_public_data', Q>
- m=<pke,pk(pc), Q_PD, 'join_Issuer_1'>
+ CCdaa_PD=<'DAA_public_data', Q>
+ m=<pke,pk(pc), CCdaa_PD, 'join_Issuer_1'>
//inputs from Issuer PK
pkX=PkX(~x,'P2')
@@ -608,7 +608,7 @@ rule Issuer_Issue_Credentials:
s_2_hat='g'^~s_2_dh //pub ecdhe key
s_2_temp=pke^~s_2_dh //Z
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
+ Q_N=<'SHA256',H_SHA256(CCdaa_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)
@@ -650,7 +650,7 @@ rule Issuer_Issue_Credentials:
, Honest ( I )
, Honest ( pke )
, Check_Ek(pke)
- , IssuerReceivedKeys(I, pke, pk(pc), Q_PD)
+ , IssuerReceivedKeys(I, pke, pk(pc), CCdaa_PD)
, IssuerCertDAAKey(I, pke, f)
, Secret_EMAID(I, pke, ~sk_emaid)
, Secret_Cred(I, pke, <A, B, C, D>)
@@ -682,14 +682,14 @@ rule Host_Passthrough_2:
in
[ In_S_B($I, $AS, m)
- , Host_State_05($PS, $AS, $I, pke, Q_PD, Q_SD)
+ , Host_State_05($PS, $AS, $I, pke, CCdaa_PD, CCdaa_SD)
]
--[ Passthrough_ActivateCred2($PS, $AS)
, OnlyOnce('Host_Passthrough_2')
]->
[ Out_S($AS,$PS,< sk_DUP, 'TPM2_Import'>)
- , Out_S($AS,$PS,< Q_SD, Q_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, 'TPM2_ActivateCredentials_2'>)
- , Host_State_06($PS, $AS, pke, Q_SD, Q_PD, C_hat, sk_PD, EMSP_Cert) //activateData
+ , Out_S($AS,$PS,< CCdaa_SD, CCdaa_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, 'TPM2_ActivateCredentials_2'>)
+ , Host_State_06($PS, $AS, pke, CCdaa_SD, CCdaa_PD, C_hat, sk_PD, EMSP_Cert) //activateData
]
//The TPM decrypts the EMAID secret key and returns it to the host/EV
@@ -743,18 +743,18 @@ rule TPM2_ActivateCredential_2:
//unwrap the inputs where needed
curlyK_2_hat=senc(curlyK(K_2),k_e)
Q=multp(~f, 'P1')
- Q_PD=<'DAA_public_data', Q>
+ CCdaa_PD=<'DAA_public_data', Q>
//recompute
s_2_rec_temp=s_2_hat^e //retrieve s
s_2_rec=KDF_e(s_2_rec_temp,'IDENTITY',s_2_hat,pke)
- Q_N_rec=<'SHA256',H_SHA256(Q_PD)> //calculate Q_N_rec which should be the same as Q_N
+ Q_N_rec=<'SHA256',H_SHA256(CCdaa_PD)> //calculate Q_N_rec which should be the same as Q_N
k_e_1=KDF_a(s_2_rec,'STORAGE',Q_N_rec) //calculate k_e_1 which should be the same as k_e
k_h_1=KDF_a(s_2_rec,'INTEGRITY','NULL') //calculate k_h_1 which should be the same as k_h
curlyH_1=MAC(<len16(curlyK_2_hat),curlyK_2_hat,Q_N_rec>,k_h_1)
curlyK_2_rec=sdec(curlyK_2_hat,k_e_1)
in
- [ In_S($AS,$PS,< Q_SD, Q_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, 'TPM2_ActivateCredentials_2'>)
+ [ In_S($AS,$PS,< CCdaa_SD, CCdaa_PD, curlyH, len16(curlyK_2_hat), curlyK_2_hat, s_2_hat, 'TPM2_ActivateCredentials_2'>)
, !TPM_AES_Key($PS, aes_key)
, !TPM_ENDORSEMENT_SK($PS,e, pke)
]
@@ -784,7 +784,7 @@ rule Host_JoinComplete:
//input from Host_State
Q=multp(~f, 'P1')
- Q_PD=<'DAA_public_data', Q>
+ CCdaa_PD=<'DAA_public_data', Q>
C_hat=senc(<A,B,C,D,u,j>,curlyK_2) //we decrypt these credentials by checking that curlyK_2_rec = curlyK_2
//recompute the hash
@@ -794,8 +794,8 @@ rule Host_JoinComplete:
in
[ In_S($PS,$AS, < curlyK_2_rec, 'ret_TPM2_ActivateCredentials_2'>)
, In_S($PS,$AS, < sk_PD, sk_SD, 'ret_TPM2_Import'>)
- , Host_State_06($PS, $AS, pke, Q_SD, Q_PD, C_hat, sk_PD, EMSP_Cert)
- //, Host_State_07($PS, $AS, pke, Q_PD, C_hat, sk_PD, sk_SD, EMSP_Cert)
+ , Host_State_06($PS, $AS, pke, CCdaa_SD, CCdaa_PD, C_hat, sk_PD, EMSP_Cert)
+ //, Host_State_07($PS, $AS, pke, CCdaa_PD, C_hat, sk_PD, sk_SD, EMSP_Cert)
]
--[
Eq(curlyK_2, curlyK_2_rec) //this allows C_hat to be decrypted
@@ -813,7 +813,7 @@ rule Host_JoinComplete:
, Commit_Test(pke, I, ~f)
, OnlyOnce('Host_JoinComplete')
]->
- [ !Host_Store_Credentials($PS, $AS, pke, EMSP_Cert, A, B, C, D, Q_SD, Q_PD, sk_PD, sk_SD)
+ [ !Host_Store_Credentials($PS, $AS, pke, EMSP_Cert, A, B, C, D, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD)
, Host_Org_Creds($PS, $AS, pke, A, B, C, D)
]
@@ -871,14 +871,14 @@ rule Host_Randomise_Credentials:
//J=PointG1(H_p(s_2_bar),y_2)
in
[
- !Host_Store_Credentials($PS, $AS, pke, EMSP_Cert, A, B, C, D, Q_SD, Q_PD, sk_PD, sk_SD)
+ !Host_Store_Credentials($PS, $AS, pke, EMSP_Cert, A, B, C, D, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD)
, Fr(~l)
]
--[
RandomisedCredentials($PS, $AS, pke)
,CertifyOnlyOnce('Host_Randomise_Credentials')
]->
- [!Host_State_08a( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, s_2_bar, y_2)
+ [!Host_State_08a( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, s_2_bar, y_2)
, Host_Rnd_Creds($PS, $AS, pke, bsn, R, S, T, W)
]
@@ -896,7 +896,7 @@ rule Host_RandomCredentialsReveal:
//and to create a session key
rule Host_Randomise_Credentials2:
[
- !Host_State_08a( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, s_2_bar, y_2)
+ !Host_State_08a( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, s_2_bar, y_2)
]
--[
RandomisedCredentials2($PS, $AS, pke)
@@ -905,7 +905,7 @@ rule Host_Randomise_Credentials2:
[
Out_S($AS,$PS,<s_2_bar,y_2,S, 'TPM2_Commit_rand'>)
, Out_S($AS, $PS, <pke, 'createSessionKey'>)
- , Host_State_08( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD)
+ , Host_State_08( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD)
]
@@ -940,9 +940,9 @@ rule TPM2_Commit_2:
rule TPM_Create_Session_Key:
let
kID=DAAKeyID(~keyID) // just a tracker to help Tamarin
- Qk=pk(~g)
- Qk_PD=<'SessionKey_public_data', Qk>
- Qk_SD=senc(~g,aes_key)
+ pkCCsess=pk(~g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ CCsess_SD=senc(~g,aes_key)
in
[In_S($AS, $PS, < pke, 'createSessionKey'>)
, !TPM_AES_Key($PS, aes_key) //our AES key
@@ -950,23 +950,23 @@ rule TPM_Create_Session_Key:
, Fr(~keyID) // id to help Tamarin pick the correct response later
]
--[
- TPM2_SessionKey_Created($PS, $AS, kID, Qk_PD)
+ TPM2_SessionKey_Created($PS, $AS, kID, pkCCsess_PD)
, DeriveSessionKey($PS, $AS, ~g)
, CertifyOnlyOnce('Create_Session_Key')
]->
[
- Out_S($PS, $AS,< kID, Qk_SD,Qk_PD, 'createdSessionKey'>)
- , !TPM_Session_SK($PS, pke, Qk, ~g)
+ Out_S($PS, $AS,< kID, CCsess_SD,pkCCsess_PD, 'createdSessionKey'>)
+ , !TPM_Session_SK($PS, pke, pkCCsess, ~g)
]
//simpe rule to leak the Session secret key:
rule TPM_SessionKeyReveal:
- [ !TPM_Session_SK($PS, pke, Qk, ~g) ]
+ [ !TPM_Session_SK($PS, pke, pkCCsess, ~g) ]
--[
KeyReveal('TPM_SessionReveal_tpm', $PS)
, KeyReveal('TPM_SessionReveal_pke', pke)
- , KeyReveal('TPM_SessionReveal_Qk', Qk)
+ , KeyReveal('TPM_SessionReveal_pkCCsess', pkCCsess)
]->
[Out(~g)]
@@ -977,8 +977,8 @@ rule TPM_SessionKeyReveal:
rule Host_Store_Randomised_Credentials:
[
In_S($PS,$AS, <S, E,cv1val, 'ret_TPM2_Commit_rand'>)
- , In_S($PS, $AS,< kID, Qk_SD,Qk_PD, 'createdSessionKey'>)
- , Host_State_08( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD)
+ , In_S($PS, $AS,< kID, CCsess_SD,pkCCsess_PD, 'createdSessionKey'>)
+ , Host_State_08( $PS, $AS, pke, bsn, R, S, T, W, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD)
]
--[
@@ -986,8 +986,8 @@ rule Host_Store_Randomised_Credentials:
, CertifyOnlyOnce('Host_Store_Randomised_Credentials')
]->
- [ !Host_State_09_a($PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, Q_SD, Q_PD, sk_PD,
- sk_SD, kID, Qk_SD,Qk_PD )
+ [ !Host_State_09_a($PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD,
+ sk_SD, kID, CCsess_SD,pkCCsess_PD )
]
@@ -1002,15 +1002,15 @@ rule CounterAdv:
// the host asks the TPM to certify the session key pair with its DAA credential
// and to compute an hmac over the authorization counter using the EMAID secret key
-rule Host_Load_Qk_For_Ceritfication:
+rule Host_Load_pkCCsess_For_Ceritfication:
let
m=<$CP, sid, 'ISO_SID'>
//received values
cv1val=Nonce(cv1) //explicitly stating this prevents partial deconstructions
- Qk=pk(g)
- Qk_PD=<'SessionKey_public_data', Qk>
- // Qk_SD=senc(g,aes_key) //the host needs to store this on behalf of the TPM
+ pkCCsess=pk(g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ // CCsess_SD=senc(g,aes_key) //the host needs to store this on behalf of the TPM
kID=DAAKeyID(keyID)
//existing values
@@ -1033,32 +1033,32 @@ rule Host_Load_Qk_For_Ceritfication:
m_buffer=<'00',i_x>
in
[
- !Host_State_09_a($PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, kID, Qk_SD,Qk_PD )
+ !Host_State_09_a($PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD )
, In(m)
, !OutIX(i_x_t)
]
--[
- LoadKeyForCertification($PS, $AS, kID, Qk_PD)
- , LoadKeyForCertification2($PS, $AS, Qk)
+ LoadKeyForCertification($PS, $AS, kID, pkCCsess_PD)
+ , LoadKeyForCertification2($PS, $AS, pkCCsess)
, AliveEV($PS, $AS, pke)
- , CertifyOnlyOnce('Host_Load_Qk_For_Ceritfication')
+ , CertifyOnlyOnce('Host_Load_pkCCsess_For_Ceritfication')
]->
- [ Out_S($AS, $PS, < pke, kID, Qk_SD, Qk_PD, c, cv1val, 'TPM2_Certify'>)
+ [ Out_S($AS, $PS, < pke, kID, CCsess_SD, pkCCsess_PD, c, cv1val, 'TPM2_Certify'>)
, Out_S($AS, $PS, < pke, sk_PD, sk_SD, m_buffer, 'TPM2_HMAC'>)
- , Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, c, sid, $CP, i_x )]
+ , Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, c, sid, $CP, i_x )]
//TPM: receives key, c, cv1 and certifies the Session key with the DAA credential
rule TPM2_Load_And_Certify:
let
- Qk_SD=senc(~g,aes_key) //loaded but not used as such
+ CCsess_SD=senc(~g,aes_key) //loaded but not used as such
kID=DAAKeyID(keyID) //only needed to keep track of multiple calls
- Qk=pk(~g)
- Qk_PD=<'SessionKey_public_data', Qk>
- Qk_n=QName('SHA256',H_SHA256(Qk_PD))
+ pkCCsess=pk(~g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ pkCCsess_n=QName('SHA256',H_SHA256(pkCCsess_PD))
- curlyA=certData('certificationData',Qk_n)
+ curlyA=certData('certificationData',pkCCsess_n)
credData='CredentialData'
c=H_k_7(credData,R,S,T,W,E, sid)
@@ -1068,7 +1068,7 @@ rule TPM2_Load_And_Certify:
small_s=plus(~r_cv1, multp(h2, ~f))
in
[
- In_S($AS, $PS, < pke, kID, Qk_SD, Qk_PD, c, cv1val_in, 'TPM2_Certify'>)
+ In_S($AS, $PS, < pke, kID, CCsess_SD, pkCCsess_PD, c, cv1val_in, 'TPM2_Certify'>)
, !TPM_DAA_SK($PS, pke, ~f)
, !TPM_AES_Key($PS, aes_key) //our AES key
, TPM_Commit_RCV1( $PS, $AS, pke, cv1val, ~r_cv1)
@@ -1076,9 +1076,9 @@ rule TPM2_Load_And_Certify:
]
--[
- TPM2_Created_Cert_TPM($PS, $AS, kID, Qk_PD)
+ TPM2_Created_Cert_TPM($PS, $AS, kID, pkCCsess_PD)
, Eq(cv1val_in, cv1val) //ensures we have the right ~r_cv1
- , TPM_Certify_q($PS, $AS, pke, Qk, ~f)
+ , TPM_Certify_q($PS, $AS, pke, pkCCsess, ~f)
, TPM_Cert_Test2(pke, small_s, ~f)
, CertifyOnlyOnce('TPM2_Load_And_Certify')
]->
@@ -1120,14 +1120,14 @@ rule TPM2_HMAC_Adv:
rule Host_Receive_Certified_Q_k2:
[
In_S($PS, $AS, < kID, curlyA, small_s, n_C, 'ret_TPM2_Certify'>)
- , In_S($PS, $AS, < sk_PD, M_id, 'ret_TPM2_HMAC'>)
- , Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, small_c, sid, $CP, i_x )
+ , In_S($PS, $AS, < sk_PD, tM_id, 'ret_TPM2_HMAC'>)
+ , Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, small_c, sid, $CP, i_x )
]
--[
- Host_Receive_Certified_Q_k2($PS, $AS, Qk_PD)
+ Host_Receive_Certified_Q_k2($PS, $AS, pkCCsess_PD)
, CertifyOnlyOnce('Host_Receive_Certified_Q_k2')
]->
- [ !Host_State_10a( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, small_c, sid, $CP, i_x, curlyA, small_s, n_C, M_id ) ]
+ [ !Host_State_10a( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, small_c, sid, $CP, i_x, curlyA, small_s, n_C, tM_id ) ]
//Host: completes the signature and sends the PaymentDetailsReq message to the CP
rule Host_Receive_Certified_Q_k:
@@ -1140,11 +1140,11 @@ rule Host_Receive_Certified_Q_k:
/*sk_unique=H_SHA256(<obfuscationValue, sk_emaid>)
sk_PD=<'SK_EMAID_public_data', sk_unique>
- M_id=MAC(m, sk_emaid)*/
+ tM_id=MAC(m, sk_emaid)*/
bsn=BSN('bottom') //basename='bottom'
E=E_S(r_cv1,S)
- //Qk=Q_K(rndKey)
+ //pkCCsess=Q_K(rndKey)
R=multp(sl,A)
S=multp(sl,B)
T=multp(sl,C)
@@ -1152,10 +1152,10 @@ rule Host_Receive_Certified_Q_k:
credData='CredentialData'
kID=DAAKeyID(keyID) //needed to associate the response with the right key
- Qk=pk(g)
- Qk_PD=<'SessionKey_public_data', Qk>
- Qk_n=QName('SHA256',H_SHA256(Qk_PD))
- curlyA=certData('certificationData',Qk_n)
+ pkCCsess=pk(g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ pkCCsess_n=QName('SHA256',H_SHA256(pkCCsess_PD))
+ curlyA=certData('certificationData',pkCCsess_n)
//received value
n_C=Nonce(rnd_n_C)
@@ -1166,17 +1166,17 @@ rule Host_Receive_Certified_Q_k:
//computed values
h1_host=H_k_2(small_c, H_6(curlyA))
h2_host=H_n_2(n_C, h1_host)
- sigma_K=<Qk_PD, curlyA, bsn, R, S, T, W, h2_host, small_s, n_C>
+ sigma_K=<pkCCsess_PD, curlyA, bsn, R, S, T, W, h2_host, small_s, n_C>
in
[
//In_S($PS, $AS, < kID, curlyA, small_s, n_C, 'ret_TPM2_Certify'>)
- //, In_S($PS, $AS, < sk_PD, M_id, 'ret_TPM2_HMAC'>)
- //, Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, small_c, sid, $CP, i_x )
- !Host_State_10a( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, Q_SD, Q_PD, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, small_c, sid, $CP, i_x, curlyA, small_s, n_C, M_id )
+ //, In_S($PS, $AS, < sk_PD, tM_id, 'ret_TPM2_HMAC'>)
+ //, Host_State_10( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, small_c, sid, $CP, i_x )
+ !Host_State_10a( $PS, $AS, pke, bsn, R, S, T, W, E, cv1val, EMSP_Cert, CCdaa_SD, CCdaa_PD, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, small_c, sid, $CP, i_x, curlyA, small_s, n_C, tM_id )
]
- --[ Host_Receive_Certified_Q_K($PS, $AS, pke, kID, Qk_PD)
+ --[ Host_Receive_Certified_Q_K($PS, $AS, pke, kID, pkCCsess_PD)
, Host_Sends_Certified_Q_K($PS, $AS, pke, sigma_K)
, Host_Sends_Certified_Q_K_cred($PS, $AS, pke, R, S, T, W, sigma_K)
, Honest ($PS)
@@ -1187,8 +1187,8 @@ rule Host_Receive_Certified_Q_k:
, CertifyOnlyOnce('Host_Receive_Certified_Q_K')
]->
- [Out(<$CP, sid, EMSP_Cert, h(M_id), sigma_K, 'PaymentDetailsReq'>)
- , Host_State_11( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, sid, $CP, i_x )]
+ [Out(<$CP, sid, EMSP_Cert, h(tM_id), sigma_K, 'PaymentDetailsReq'>)
+ , Host_State_11( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, i_x )]
// CP verifies the PaymentDetailsReq message, generates a fresh nonce_ix and sends it
// with the usual V2G PnC nonce to the EV in the PayDetailsRes message
@@ -1203,14 +1203,14 @@ rule CP_Check_TPM_Certificate:
T=multp(sl,C)
W=multp(sl,D)
- Qk=pk(g)
- Qk_PD=<'SessionKey_public_data', Qk>
- Qk_n=QName('SHA256',H_SHA256(Qk_PD))
- curlyA=certData('certificationData',Qk_n)
+ pkCCsess=pk(g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ pkCCsess_n=QName('SHA256',H_SHA256(pkCCsess_PD))
+ curlyA=certData('certificationData',pkCCsess_n)
small_s=plus(r_cv1, multp(h2,f))
n_C=Nonce(rnd_n_C)
credData='CredentialData'
- sigma_K=<Qk_PD, curlyA, bsn_in, R, S, T, W, h2_host, small_s, n_C>
+ sigma_K=<pkCCsess_PD, curlyA, bsn_in, R, S, T, W, h2_host, small_s, n_C>
//computed values
//E_dash=minus(multp(small_s, S), multp(h2_host, W)) = E
@@ -1227,7 +1227,7 @@ rule CP_Check_TPM_Certificate:
m_out=<$CP, ~sid, ~nonce, ~nonce_ix, 'PaymentDetailsRes'>
in
- [In(<$CP, ~sid, EMSP_Cert, X1, sigma_K, 'PaymentDetailsReq'>)
+ [In(<$CP, ~sid, EMSP_Cert, M_id, sigma_K, 'PaymentDetailsReq'>)
, !Pk(I, pkX, pkY) // Authentic from EMSP cert
, CP_State_00($CP, ~sid)
, Fr(~nonce), Fr(~nonce_ix)]
@@ -1241,7 +1241,7 @@ rule CP_Check_TPM_Certificate:
]->
[
Out(m_out)
- , CP_State_01($CP, ~sid, I, sigma_K, ~nonce,X1, ~nonce_ix)
+ , CP_State_01($CP, ~sid, I, sigma_K, ~nonce,M_id, ~nonce_ix)
]
//host receives PaymentDetailsRes message from CP and asks TPM to compute the mac_out
@@ -1253,7 +1253,7 @@ rule Host_Auth:
m_buffer=<'01',i_x>
in
[ In(m),
- Host_State_11( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, sid, $CP, i_x )
+ Host_State_11( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, i_x )
]
--[
Host_Auth($PS, $AS, sid)
@@ -1261,75 +1261,75 @@ rule Host_Auth:
]->
[
Out_S($AS, $PS, < pke, sk_PD, sk_SD, m_buffer, 'TPM2_HMAC'>),
- Host_State_12( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, sid, $CP, nonce, nonce_ix) ]
+ Host_State_12( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, nonce, nonce_ix) ]
// host receives mac from TPM and asks the TPM to sign the charge authorisation request
// with the session key
rule Host_Auth2:
let
- Qk=pk(g)
- Qk_PD=<'SessionKey_public_data', Qk>
- X2=h(h(<M_auth, nonce_ix>))
- authH=h(<'AuthorizationReq', $CP, nonce, X2>)
+ pkCCsess=pk(g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ tM_auth=h(<M_auth, nonce_ix>)
+ authH=h(<'AuthorizationReq', $CP, nonce, tM_auth>)
in
[
In_S($PS, $AS, < sk_PD, M_auth, 'ret_TPM2_HMAC'>),
- Host_State_12( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, sid, $CP, nonce, nonce_ix)
+ Host_State_12( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, nonce, nonce_ix)
]
--[
Host_Auth2($PS, $AS, sid)
, CertifyOnlyOnce('Host_Auth2')
]->
- [ Out_S($AS, $PS, < Qk_SD, Qk_PD, authH, 'TPM2_Sign_S'>),
- Host_State_13( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, sid, $CP, nonce, nonce_ix, M_auth)
+ [ Out_S($AS, $PS, < CCsess_SD, pkCCsess_PD, authH, 'TPM2_Sign_S'>),
+ Host_State_13( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, nonce, nonce_ix, M_auth)
]
// TPM signs the authorization request with the session key and returns signature to host
rule TPM2_Sign_SessionKey:
let
- Qk_SD=senc(~g,aes_key)
- Qk=pk(~g)
- Qk_PD=<'SessionKey_public_data', Qk>
+ CCsess_SD=senc(~g,aes_key)
+ pkCCsess=pk(~g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
in
- [ In_S($AS, $PS, < Qk_SD, Qk_PD, hash_in, 'TPM2_Sign_S'>)
+ [ In_S($AS, $PS, < CCsess_SD, pkCCsess_PD, hash_in, 'TPM2_Sign_S'>)
, !TPM_AES_Key($PS, aes_key)
- , !TPM_Session_SK($PS, pke, Qk, ~g)
+ , !TPM_Session_SK($PS, pke, pkCCsess, ~g)
]
--[
- TPM2_Sign_S($PS, $AS, Qk_PD)
+ TPM2_Sign_S($PS, $AS, pkCCsess_PD)
, CertifyOnlyOnce(<'TPM2_Sign_SessionKey', hash_in>)
]->
- [Out_S($PS, $AS, < Qk_PD, sign(hash_in,~g), 'ret_TPM2_Sign_S'>)]
+ [Out_S($PS, $AS, < pkCCsess_PD, sign(hash_in,~g), 'ret_TPM2_Sign_S'>)]
// host receives signature for authorization request from TPM and sends the
// signed authorization request to the CP
rule Host_Auth3:
let
EMSP_Cert=<I,pkX,pkY>
- Qk=pk(g)
- Qk_PD=<'SessionKey_public_data', Qk>
+ pkCCsess=pk(g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
/*sk_unique=H_SHA256(<obfuscationValue, sk_emaid>)
sk_PD=<'SK_EMAID_public_data', sk_unique>
M_auth=MAC(m, sk_emaid)*/
- X2=h(h(<M_auth, nonce_ix>))
- authH=h(<'AuthorizationReq', $CP, nonce, X2>)
+ tM_auth=h(<M_auth, nonce_ix>)
+ authH=h(<'AuthorizationReq', $CP, nonce, tM_auth>)
in
- [ In_S($PS,$AS, < Qk_PD, sig_over_auth, 'ret_TPM2_Sign_S'>),
- Host_State_13( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, Qk_SD,Qk_PD, sid, $CP, nonce, nonce_ix, M_auth)
+ [ In_S($PS,$AS, < pkCCsess_PD, sig_over_auth, 'ret_TPM2_Sign_S'>),
+ Host_State_13( $PS, $AS, pke, EMSP_Cert, sk_PD, sk_SD, kID, CCsess_SD,pkCCsess_PD, sid, $CP, nonce, nonce_ix, M_auth)
]
--[
- Eq(verify(sig_over_auth,authH,Qk), true) //TPM response is for prev call
+ Eq(verify(sig_over_auth,authH,pkCCsess), true) //TPM response is for prev call
, Host_Auth3($PS, $AS, sid)
//, CounterH(i_x_t)
- , RunningEV_Sign( Qk , $CP, authH )
+ , RunningEV_Sign( pkCCsess , $CP, authH )
, RunningEV_Auth( $PS, $AS, pke, I, M_auth )
- , RunningEV_Auth2( $PS, $AS, pke, I, M_auth, Qk_PD )
+ , RunningEV_Auth2( $PS, $AS, pke, I, M_auth, pkCCsess_PD )
, CertifyOnlyOnce('Host_Auth3')
]->
- [ Out(<sid, authH, sig_over_auth, X2, 'AuthorizationReq'>)
- , !Host_State_14( $PS, $AS, pke, EMSP_Cert, kID, Qk_SD,Qk_PD, sid, $CP, M_auth)
+ [ Out(<sid, authH, sig_over_auth, tM_auth, 'AuthorizationReq'>)
+ , !Host_State_14( $PS, $AS, pke, EMSP_Cert, kID, CCsess_SD,pkCCsess_PD, sid, $CP, M_auth)
]
//=============================================================
@@ -1346,56 +1346,56 @@ rule CP_Verify:
T=multp(sl,C)
W=multp(sl,D)
- Qk=pk(g)
- Qk_PD=<'SessionKey_public_data', Qk>
- Qk_n=QName('SHA256',H_SHA256(Qk_PD))
- curlyA=certData('certificationData',Qk_n)
+ pkCCsess=pk(g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ pkCCsess_n=QName('SHA256',H_SHA256(pkCCsess_PD))
+ curlyA=certData('certificationData',pkCCsess_n)
small_s=plus(r_cv1, multp(h2,f))
n_C=Nonce(rnd_n_C)
- sigma_K=<Qk_PD, curlyA, bsn_in, R, S, T, W, h2_host, small_s, n_C>
+ sigma_K=<pkCCsess_PD, curlyA, bsn_in, R, S, T, W, h2_host, small_s, n_C>
- m_in=<~sid, authH_in, sig_over_auth, X2, 'AuthorizationReq'>
+ m_in=<~sid, authH_in, sig_over_auth, tM_auth, 'AuthorizationReq'>
- authH=h(<'AuthorizationReq', $CP, ~nonce, X2>)
+ authH=h(<'AuthorizationReq', $CP, ~nonce, tM_auth>)
- m_out=<X1, ~nonce_ix, X2, Qk>
+ m_out=<M_id, ~nonce_ix, tM_auth, pkCCsess>
in
[ In(m_in)
- , CP_State_01($CP, ~sid, I, sigma_K, ~nonce, X1, ~nonce_ix)
+ , CP_State_01($CP, ~sid, I, sigma_K, ~nonce, M_id, ~nonce_ix)
]
--[
Eq(authH_in, authH)
- , Eq(verify(sig_over_auth,authH,Qk), true)
+ , Eq(verify(sig_over_auth,authH,pkCCsess), true)
, CP_Verify($CP, ~sid)
- , CommitCP($CP, Qk, authH)
- , Honest(Qk)
+ , CommitCP($CP, pkCCsess, authH)
+ , Honest(pkCCsess)
, Honest($CP)
, Honest(I)
, CertifyOnlyOnce('CP_Verify')
]->
[ Out(<I, <m_out, 'EMSP_Auth'>>)
- , !CP_State_02($CP, ~sid, I, Qk, X2) ]
+ , !CP_State_02($CP, ~sid, I, pkCCsess, tM_auth) ]
// the eMSP verifies the authorization request
rule EMSP_Auth:
let
i_x=h(i_x_t)
- m=<X1_in, nonce_ix, X2_in, Qk>
- Qk_PD=<'SessionKey_public_data', Qk>
+ m=<M_id_in, nonce_ix, tM_auth_in, pkCCsess>
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
- M_id=MAC(<'00', i_x>, ~sk_emaid)
- X1=h(M_id)
+ tM_id=MAC(<'00', i_x>, ~sk_emaid)
+ M_id=h(tM_id)
M_auth=MAC(<'01',i_x>, ~sk_emaid)
- X2=h(h(<M_auth, nonce_ix>))
+ tM_auth=h(<M_auth, nonce_ix>)
in
[ In(<I, <m, 'EMSP_Auth'>>)
, !OutIX(i_x_t)
, !Issuer_EMAID_SK(I, pke, ~sk_emaid)
]
- --[ Eq(X1, X1_in)
- , Eq(X2, X2_in)
+ --[ Eq(M_id, M_id_in)
+ , Eq(tM_auth, tM_auth_in)
, CommitEMSP(I, pke, M_auth)
- , CommitEMSP2(I, pke, M_auth, Qk_PD)
+ , CommitEMSP2(I, pke, M_auth, pkCCsess_PD)
, CommitEMSP_sk(I, pke, ~sk_emaid)
, CommitEMSP_sk2(I, pke, M_auth, ~sk_emaid)
, Honest(I)
@@ -1404,7 +1404,7 @@ rule EMSP_Auth:
, CertifyOnlyOnce('EMSP_Auth')
]->
[
- !Issuer_State_Charge(I, pke, ~sk_emaid, i_x, M_auth, Qk)
+ !Issuer_State_Charge(I, pke, ~sk_emaid, i_x, M_auth, pkCCsess)
]
// the CP sends the charge data to the vehicle for attestation
@@ -1413,14 +1413,14 @@ rule CP_DataSend:
data=<$CP, ~sid, 'charge_data',~dataID>
in
[ Fr(~dataID)
- , !CP_State_02($CP, ~sid, I, Qk, X2)
+ , !CP_State_02($CP, ~sid, I, pkCCsess, tM_auth)
]
--[
CP_DataSend($CP, ~sid, ~dataID),
CertifyOnlyOnce('CP_DataSend')
]->
[ Out(data)
- , CP_State_03($CP, ~sid, I, Qk, X2, ~dataID) ]
+ , CP_State_03($CP, ~sid, I, pkCCsess, tM_auth, ~dataID) ]
// the EV (using its TPM) signs the charge data together with ev_h, a hash over the authorisation
// value used during charge authorisation and its public session key to bind them
@@ -1428,22 +1428,22 @@ rule CP_DataSend:
rule EV_DataSign:
let
EMSP_Cert=<I,pkX,pkY>
- Qk=pk(~g)
- Qk_PD=<'SessionKey_public_data', Qk>
+ pkCCsess=pk(~g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
data=<$CP, sid, 'charge_data',dataID>
- ev_h=h(<M_auth,Qk>)
+ ev_h=h(<'EV_h',M_auth,pkCCsess>)
dataTBS=h(<'charge_data',dataID, ev_h>)
in
[ In(data)
- , !Host_State_14( $PS, $AS, pke, EMSP_Cert, kID, Qk_SD,Qk_PD, sid, $CP, M_auth)
+ , !Host_State_14( $PS, $AS, pke, EMSP_Cert, kID, CCsess_SD,pkCCsess_PD, sid, $CP, M_auth)
]
- --[ EV_DataSign($PS, $AS, kID, Qk_PD, sid, dataID)
+ --[ EV_DataSign($PS, $AS, kID, pkCCsess_PD, sid, dataID)
, CertifyOnlyOnce('EV_DataSign')
]->
- [ Out_S($AS, $PS, < Qk_SD, Qk_PD, dataTBS, 'TPM2_Sign_S'>)
- , Host_State_15( $PS, $AS, pke, EMSP_Cert, kID, Qk_SD,Qk_PD, sid, $CP, M_auth, data, dataTBS)
+ [ Out_S($AS, $PS, < CCsess_SD, pkCCsess_PD, dataTBS, 'TPM2_Sign_S'>)
+ , Host_State_15( $PS, $AS, pke, EMSP_Cert, kID, CCsess_SD,pkCCsess_PD, sid, $CP, M_auth, data, dataTBS)
]
// the EV receives the signed charge data from the TPM, sends the signature
@@ -1451,24 +1451,24 @@ rule EV_DataSign:
rule EV_DataSign_Send:
let
EMSP_Cert=<I,pkX,pkY>
- Qk=pk(~g)
- Qk_PD=<'SessionKey_public_data', Qk>
+ pkCCsess=pk(~g)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
data=<$CP, sid, 'charge_data',dataID>
- ev_h=h(<M_auth,Qk>)
+ ev_h=h(<'EV_h',M_auth,pkCCsess>)
dataTBS=h(<'charge_data',dataID, ev_h>)
m_out=<ev_h, dataTBS, dataSig>
m_o2=<'charge_data',dataID, dataSig, ev_h>
in
- [ In_S($PS, $AS, < Qk_PD, dataSig, 'ret_TPM2_Sign_S'>)
- , Host_State_15( $PS, $AS, pke, EMSP_Cert, kID, Qk_SD,Qk_PD, sid, $CP, M_auth, data, dataTBS)
+ [ In_S($PS, $AS, < pkCCsess_PD, dataSig, 'ret_TPM2_Sign_S'>)
+ , Host_State_15( $PS, $AS, pke, EMSP_Cert, kID, CCsess_SD,pkCCsess_PD, sid, $CP, M_auth, data, dataTBS)
]
--[
- Eq(verify(dataSig,dataTBS,Qk), true), //TPM response is for prev call
- EV_DataSign_Send($PS, $AS, kID, Qk_PD, sid, dataID),
- EV_DataSign_Send2($PS, $AS, Qk),
+ Eq(verify(dataSig,dataTBS,pkCCsess), true), //TPM response is for prev call
+ EV_DataSign_Send($PS, $AS, kID, pkCCsess_PD, sid, dataID),
+ EV_DataSign_Send2($PS, $AS, pkCCsess),
RunningEV_Data($PS, $AS, pke, I, <M_auth, 'charge_data', dataID>),
RunningEV_Data2(pke, I, <M_auth, 'charge_data', dataID>),
CertifyOnlyOnce('EV_DataSign_Send')
@@ -1484,18 +1484,18 @@ rule CP_DataRec:
dataTBS=h(<'charge_data',~dataID, ev_h>)
M_auth=MAC(<'01',i_x>, sk_emaid)
- X2=h(h(<M_auth, nonce_ix>))
+ tM_auth=h(<M_auth, nonce_ix>)
m_out=<'charge_data',~dataID, dataSig, ev_h>
in
[ In(m_in)
- , CP_State_03($CP, ~sid, I, Qk, X2, ~dataID)
+ , CP_State_03($CP, ~sid, I, pkCCsess, tM_auth, ~dataID)
]
--[
Eq(dataTBS_in, dataTBS)
- , Eq(verify(dataSig,dataTBS,Qk), true)
+ , Eq(verify(dataSig,dataTBS,pkCCsess), true)
, CP_DataRec($CP, ~sid, ~dataID)
- , CP_DataRec2($CP, Qk, sk_emaid)
+ , CP_DataRec2($CP, pkCCsess, sk_emaid)
, CertifyOnlyOnce('CP_DataRec')
]->
[ Out(<I, <m_out, 'EMSP_Data'>>) ]
@@ -1508,19 +1508,19 @@ rule EMSP_Data:
M_auth=MAC(<'01',i_x>, ~sk_emaid)
m=<'charge_data',dataID, dataSig, ev_h_in>
- Qk_PD=<'SessionKey_public_data', Qk>
- ev_h=h(<M_auth,Qk>)
+ pkCCsess_PD=<'SessionKey_public_data', pkCCsess>
+ ev_h=h(<'EV_h',M_auth,pkCCsess>)
dataTBS=h(<'charge_data', dataID, ev_h>)
in
[ In(<I, <m, 'EMSP_Data'>>)
- , !Issuer_State_Charge(I, pke, ~sk_emaid, i_x, M_auth, Qk)
+ , !Issuer_State_Charge(I, pke, ~sk_emaid, i_x, M_auth, pkCCsess)
]
--[ Eq(ev_h, ev_h_in)
- , Eq(verify(dataSig,dataTBS,Qk), true)
+ , Eq(verify(dataSig,dataTBS,pkCCsess), true)
, Honest(I)
, Honest(pke)
, CommitEMSP_Data(I, pke, <M_auth, 'charge_data', dataID>)
- , CommitEMSP_Data2(I, pke, <M_auth, 'charge_data', dataID>, Qk_PD)
+ , CommitEMSP_Data2(I, pke, <M_auth, 'charge_data', dataID>, pkCCsess_PD)
, OnlyOnce_i_x(I, M_auth, dataID)
, CertifyOnlyOnce('EMSP_Data')
]->
@@ -1582,7 +1582,7 @@ lemma restriction_one_tpm_per_host:
// any endorsement key that is presented to the issuer must have been generated
// by a TPM. This restrictions represents the fact that the issuer will check
// each endorsement key and only allow ones that were created by a TPM
-lemma restricition_pke_comes_from_tpm:
+lemma restriction_pke_comes_from_tpm:
"All pke #i .
Check_Ek(pke) @ i
==>
@@ -1894,7 +1894,7 @@ lemma correctness_charge_authorisation_req_1: exists-trace
#t20
#t21 #t22
//certify steps
- kID Qk_PD sigma
+ kID pkCCsess_PD sigma
#t23 #t24 #t25 #t26 #t27 #t28
.
@@ -1926,7 +1926,7 @@ lemma correctness_charge_authorisation_req_1: exists-trace
//stored the DAA key with the host
//& Store_Keys(TPM, Host) @ t10
- //check the EK and Q_PD as the issuer
+ //check the EK and CCdaa_PD as the issuer
& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t12
@@ -1942,11 +1942,11 @@ lemma correctness_charge_authorisation_req_1: exists-trace
& TPMCommitRandomised(TPM, Host, pke) @ t24
- & TPM2_SessionKey_Created(TPM, Host, kID, Qk_PD) @ t25
+ & TPM2_SessionKey_Created(TPM, Host, kID, pkCCsess_PD) @ t25
- & LoadKeyForCertification(TPM, Host, kID, Qk_PD) @ t26
+ & LoadKeyForCertification(TPM, Host, kID, pkCCsess_PD) @ t26
- & TPM2_Created_Cert_TPM(TPM, Host, kID, Qk_PD) @ t27
+ & TPM2_Created_Cert_TPM(TPM, Host, kID, pkCCsess_PD) @ t27
& Host_Sends_Certified_Q_K(TPM, Host, pke, sigma) @ t28
@@ -1984,7 +1984,7 @@ lemma correctness_charge_authorisation_req_2: exists-trace
#t12 // #t14 #t15 #t16 #t17 #t18 #t19
#t20 #t21 #t22
//certify and verify steps
- kID Qk_PD sigma CP
+ kID pkCCsess_PD sigma CP
#t23 #t24 #t25 #t26 #t27 #t28 #t29
.
@@ -2016,7 +2016,7 @@ lemma correctness_charge_authorisation_req_2: exists-trace
//stored the DAA key with the host
//& Store_Keys(TPM, Host) @ t10
- //check the EK and Q_PD as the issuer
+ //check the EK and CCdaa_PD as the issuer
& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t12
@@ -2032,11 +2032,11 @@ lemma correctness_charge_authorisation_req_2: exists-trace
& TPMCommitRandomised(TPM, Host, pke) @ t24
- & TPM2_SessionKey_Created(TPM, Host, kID, Qk_PD) @ t25
+ & TPM2_SessionKey_Created(TPM, Host, kID, pkCCsess_PD) @ t25
- & LoadKeyForCertification(TPM, Host, kID, Qk_PD) @ t26
+ & LoadKeyForCertification(TPM, Host, kID, pkCCsess_PD) @ t26
- & TPM2_Created_Cert_TPM(TPM, Host, kID, Qk_PD) @ t27
+ & TPM2_Created_Cert_TPM(TPM, Host, kID, pkCCsess_PD) @ t27
& Host_Sends_Certified_Q_K(TPM, Host, pke, sigma) @ t28
@@ -2079,7 +2079,7 @@ lemma correctness_charge_authorisation: exists-trace
#t12 // #t14 #t15 #t16 #t17 #t18 #t19
#t20 #t21 #t22
//certify and verify steps
- kID Qk_PD sigma
+ kID pkCCsess_PD sigma
#t23 #t24 #t25 #t26 #t27 #t28 #t29
CP sid #t01_2
sk_emaid
@@ -2116,7 +2116,7 @@ lemma correctness_charge_authorisation: exists-trace
//stored the DAA key with the host
//& Store_Keys(TPM, Host) @ t10
- //check the EK and Q_PD as the issuer
+ //check the EK and CCdaa_PD as the issuer
& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t12
@@ -2132,11 +2132,11 @@ lemma correctness_charge_authorisation: exists-trace
& TPMCommitRandomised(TPM, Host, pke) @ t24
- & TPM2_SessionKey_Created(TPM, Host, kID, Qk_PD) @ t25
+ & TPM2_SessionKey_Created(TPM, Host, kID, pkCCsess_PD) @ t25
- & LoadKeyForCertification(TPM, Host, kID, Qk_PD) @ t26
+ & LoadKeyForCertification(TPM, Host, kID, pkCCsess_PD) @ t26
- & TPM2_Created_Cert_TPM(TPM, Host, kID, Qk_PD) @ t27
+ & TPM2_Created_Cert_TPM(TPM, Host, kID, pkCCsess_PD) @ t27
& Host_Sends_Certified_Q_K(TPM, Host, pke, sigma) @ t28
@@ -2146,7 +2146,7 @@ lemma correctness_charge_authorisation: exists-trace
& Host_Auth(TPM, Host, sid) @ t30
& TPM_HMAC(TPM, Host, pke, sk_emaid) @ t31
& Host_Auth2(TPM, Host, sid) @ t32
- & TPM2_Sign_S(TPM, Host, Qk_PD) @ t33
+ & TPM2_Sign_S(TPM, Host, pkCCsess_PD) @ t33
& RunningEV_Auth(TPM, Host, pke, I, M_auth ) @ t34
& CP_Verify(CP, sid) @t35
& CommitEMSP(I, pke, M_auth) @t36
@@ -2194,7 +2194,7 @@ lemma correctness_charge_data_authentication: exists-trace
#t12 // #t14 #t15 #t16 #t17 #t18 #t19
#t20 #t21 #t22
//certify and verify steps
- kID Qk_PD sigma
+ kID pkCCsess_PD sigma
#t23 #t24 #t25 #t26 #t27 #t28 #t29
CP sid #t01_2
sk_emaid
@@ -2233,7 +2233,7 @@ lemma correctness_charge_data_authentication: exists-trace
//stored the DAA key with the host
//& Store_Keys(TPM, Host) @ t10
- //check the EK and Q_PD as the issuer
+ //check the EK and CCdaa_PD as the issuer
& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t12
@@ -2249,11 +2249,11 @@ lemma correctness_charge_data_authentication: exists-trace
& TPMCommitRandomised(TPM, Host, pke) @ t24
- & TPM2_SessionKey_Created(TPM, Host, kID, Qk_PD) @ t25
+ & TPM2_SessionKey_Created(TPM, Host, kID, pkCCsess_PD) @ t25
- & LoadKeyForCertification(TPM, Host, kID, Qk_PD) @ t26
+ & LoadKeyForCertification(TPM, Host, kID, pkCCsess_PD) @ t26
- & TPM2_Created_Cert_TPM(TPM, Host, kID, Qk_PD) @ t27
+ & TPM2_Created_Cert_TPM(TPM, Host, kID, pkCCsess_PD) @ t27
& Host_Sends_Certified_Q_K(TPM, Host, pke, sigma) @ t28
@@ -2263,15 +2263,15 @@ lemma correctness_charge_data_authentication: exists-trace
& Host_Auth(TPM, Host, sid) @ t30
& TPM_HMAC(TPM, Host, pke, sk_emaid) @ t31
& Host_Auth2(TPM, Host, sid) @ t32
- & TPM2_Sign_S(TPM, Host, Qk_PD) @ t33
+ & TPM2_Sign_S(TPM, Host, pkCCsess_PD) @ t33
& RunningEV_Auth(TPM, Host, pke, I, M_auth ) @ t34
& CP_Verify(CP, sid) @t35
& CommitEMSP(I, pke, M_auth) @t36
& CP_DataSend(CP, sid, dataID) @t37
- & EV_DataSign(TPM, Host, kID, Qk_PD, sid, dataID) @t38
- & TPM2_Sign_S(TPM, Host, Qk_PD) @t39
- & EV_DataSign_Send(TPM, Host, kID, Qk_PD, sid, dataID) @t40
+ & EV_DataSign(TPM, Host, kID, pkCCsess_PD, sid, dataID) @t38
+ & TPM2_Sign_S(TPM, Host, pkCCsess_PD) @t39
+ & EV_DataSign_Send(TPM, Host, kID, pkCCsess_PD, sid, dataID) @t40
& CP_DataRec(CP, sid, dataID) @t41
& CommitEMSP_Data(I, pke, <M_auth, 'charge_data', dataID>) @t42
@@ -2324,7 +2324,7 @@ lemma correctness_with_adv: exists-trace
#t12 // #t14 #t15 #t16 #t17 #t18 #t19
#t20 #t21 #t22
//certify and verify steps
- kID Qk_PD
+ kID pkCCsess_PD
#t23 #t24 #t25 #t26 #t27 #t28
sid sk_emaid
#t30 #t31 #t32 #t33 #t34 #t36
@@ -2360,7 +2360,7 @@ lemma correctness_with_adv: exists-trace
//stored the DAA key with the host
//& Store_Keys(TPM, Host) @ t10
- //check the EK and Q_PD as the issuer
+ //check the EK and CCdaa_PD as the issuer
& IssuerReceivedKeys(I, pke, pcpd, qpd) @ t12
@@ -2376,26 +2376,26 @@ lemma correctness_with_adv: exists-trace
& TPMCommitRandomised(TPM, Host, pke) @ t24
- & TPM2_SessionKey_Created(TPM, Host, kID, Qk_PD) @ t25
+ & TPM2_SessionKey_Created(TPM, Host, kID, pkCCsess_PD) @ t25
- & LoadKeyForCertification(TPM, Host, kID, Qk_PD) @ t26
+ & LoadKeyForCertification(TPM, Host, kID, pkCCsess_PD) @ t26
- & TPM2_Created_Cert_TPM(TPM, Host, kID, Qk_PD) @ t27
+ & TPM2_Created_Cert_TPM(TPM, Host, kID, pkCCsess_PD) @ t27
- & Host_Receive_Certified_Q_K(TPM, Host, pke, kID, Qk_PD) @ t28
+ & Host_Receive_Certified_Q_K(TPM, Host, pke, kID, pkCCsess_PD) @ t28
& Host_Auth(TPM, Host, sid) @ t30
& TPM_HMAC(TPM, Host, pke, sk_emaid) @ t31
& Host_Auth2(TPM, Host, sid) @ t32
- & TPM2_Sign_S(TPM, Host, Qk_PD) @ t33
- & RunningEV_Auth2(TPM, Host, pke, I, M_auth, Qk_PD ) @ t34
- & CommitEMSP2(I, pke, M_auth, Qk_PD) @t36
-
- & EV_DataSign(TPM, Host, kID, Qk_PD, sid, dataID) @t38
- & TPM2_Sign_S(TPM, Host, Qk_PD) @t39
- & EV_DataSign_Send(TPM, Host, kID, Qk_PD, sid, dataID) @t40
- & CommitEMSP_Data2(I, pke, <M_auth, 'charge_data', dataID>, Qk_PD) @t42
+ & TPM2_Sign_S(TPM, Host, pkCCsess_PD) @ t33
+ & RunningEV_Auth2(TPM, Host, pke, I, M_auth, pkCCsess_PD ) @ t34
+ & CommitEMSP2(I, pke, M_auth, pkCCsess_PD) @t36
+
+ & EV_DataSign(TPM, Host, kID, pkCCsess_PD, sid, dataID) @t38
+ & TPM2_Sign_S(TPM, Host, pkCCsess_PD) @t39
+ & EV_DataSign_Send(TPM, Host, kID, pkCCsess_PD, sid, dataID) @t40
+ & CommitEMSP_Data2(I, pke, <M_auth, 'charge_data', dataID>, pkCCsess_PD) @t42
& t01<t02 //Issuer gets created before CPS
& t02<t04 //Host gets created before Bind
--
GitLab