Skip to content
Snippets Groups Projects
Commit a10c424d authored by Müller, Jonas's avatar Müller, Jonas
Browse files

Update SigPQEAC results

parent 2e2142c3
Branches
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
results/45991790.err.ALL_SigPQEAC_TAMARIN → results/45992234.err.ALL_SigPQEAC_TAMARIN
+ 8
− 2
View file @ a10c424d
...@@ -24,5 +24,11 @@ ...@@ -24,5 +24,11 @@
[Saturating Sources] Step 2/5 [Saturating Sources] Step 2/5
[Saturating Sources] Step 1/5 [Saturating Sources] Step 1/5
[Saturating Sources] Step 2/5 [Saturating Sources] Step 2/5
WARNING: you should run this program as super-user. [Saturating Sources] Step 1/5
WARNING: output may be incomplete or inaccurate, you should run this program as super-user. [Saturating Sources] Step 2/5
[Saturating Sources] Step 1/5
[Saturating Sources] Step 2/5
[Saturating Sources] Step 1/5
[Saturating Sources] Step 2/5
/var/spool/slurmd/job45992234/slurm_script: line 29: output/hw/45992234.cpu: No such file or directory
/var/spool/slurmd/job45992234/slurm_script: line 30: output/hw/45992234.processor: No such file or directory
results/45991790.out.ALL_SigPQEAC_TAMARIN → results/45992234.out.ALL_SigPQEAC_TAMARIN
+ 597
− 645
View file @ a10c424d
maude tool: 'maude' maude tool: 'maude'
checking version: 3.3.1. OK. checking version: 3.3.1. OK.
checking installation: OK. checking installation: OK.
theory FastSigPQEAC begin theory SigPQEAC begin
// Function signature and definition of the equational theory E // Function signature and definition of the equational theory E
...@@ -78,288 +78,253 @@ rule (modulo E) TA_INIT_T: ...@@ -78,288 +78,253 @@ rule (modulo E) TA_INIT_T:
/* has exactly the trivial AC variant */ /* has exactly the trivial AC variant */
rule (modulo E) TA_CHALLENGE_C: rule (modulo E) TA_CHALLENGE_C:
[ [ In( <certT, '1', 't'> ), Fr( ~r1 ), Fr( ~id_c ), Fr( ~iid ) ]
In( <certT, '1', 't'> ), Fr( ~r1 ), Fr( ~id_c ), Fr( ~iid ), Fr( ~r2 ),
!Cert( $C, certC, 'chip' )
]
--[ Eq( verify_cert(certT, 'terminal'), true ), Started( ) ]-> --[ Eq( verify_cert(certT, 'terminal'), true ), Started( ) ]->
[ [
Out( <~id_c, ~r1, certC, ~r2, '2', 'c'> ), Out( ~iid ), Out( <~id_c, ~r1, '2', 'c'> ),
TAChallengeC( <$C, ~iid>, certT, ~id_c, ~r1, ~r2 ) TAChallengeC( <$C, ~iid>, certT, ~id_c, ~r1 )
] ]
/* /*
rule (modulo AC) TA_CHALLENGE_C: rule (modulo AC) TA_CHALLENGE_C:
[ [ In( <certT, '1', 't'> ), Fr( ~r1 ), Fr( ~id_c ), Fr( ~iid ) ]
In( <certT, '1', 't'> ), Fr( ~r1 ), Fr( ~id_c ), Fr( ~iid ), Fr( ~r2 ),
!Cert( $C, certC, 'chip' )
]
--[ Eq( z, true ), Started( ) ]-> --[ Eq( z, true ), Started( ) ]->
[ [
Out( <~id_c, ~r1, certC, ~r2, '2', 'c'> ), Out( ~iid ), Out( <~id_c, ~r1, '2', 'c'> ),
TAChallengeC( <$C, ~iid>, certT, ~id_c, ~r1, ~r2 ) TAChallengeC( <$C, ~iid>, certT, ~id_c, ~r1 )
] ]
variants (modulo AC) variants (modulo AC)
1. certT = certT.15 1. certT = certT.12
z = verify(cert_sig(certT.15), z = verify(cert_sig(certT.12),
<cert_pk(certT.15), cert_id(certT.15), 'terminal'>, pk(ca_sk)) <cert_pk(certT.12), cert_id(certT.12), 'terminal'>, pk(ca_sk))
2. certT = cert(x.16, sign(<x.16, x.17, 'terminal'>, ca_sk), x.17) 2. certT = cert(x.13, sign(<x.13, x.14, 'terminal'>, ca_sk), x.14)
z = true z = true
3. certT = cert(x.17, x.18, x.19) 3. certT = cert(x.14, x.15, x.16)
z = verify(x.18, <x.17, x.19, 'terminal'>, pk(ca_sk)) z = verify(x.15, <x.14, x.16, 'terminal'>, pk(ca_sk))
*/ */
rule (modulo E) TA_RESPONSE_T: rule (modulo E) TA_RESPONSE_T:
[ [
In( <id_c, r1, certC, r2, '2', 'c'> ), TAInitT( <$T, iid> ), In( <id_c, r1, '2', 'c'> ), TAInitT( <$T, iid> ),
!Ltk( $T, ~skT, 'terminal' ), !Cert( $T, certT, 'terminal' ), Fr( ~k ) !Ltk( $T, ~skT, 'terminal' )
]
-->
[
Out( <sign(<'TA', id_c, r1>, ~skT), '3', 't'> ),
TAResponseT( <$T, iid>, id_c )
]
/* has exactly the trivial AC variant */
rule (modulo E) TA_COMPLETE_C:
[ In( <s, '3', 't'> ), TAChallengeC( <$C, iid>, certT, id_c, r1 ) ]
--[
Eq( verify(s, <'TA', id_c, r1>, cert_pk(certT)), true ),
CompletedTA( $C, iid, cert_id(certT) )
]->
[ TACompleteC( <$C, iid>, certT, id_c, r1 ) ]
/*
rule (modulo AC) TA_COMPLETE_C:
[ In( <s, '3', 't'> ), TAChallengeC( <$C, iid>, certT, id_c, r1 ) ]
--[ Eq( z, true ), CompletedTA( $C, iid, z.1 ) ]->
[ TACompleteC( <$C, iid>, certT, id_c, r1 ) ]
variants (modulo AC)
1. certT = certT.16
id_c = id_c.17
r1 = r1.19
s = s.20
z = verify(s.20, <'TA', id_c.17, r1.19>, cert_pk(certT.16))
z.1 = cert_id(certT.16)
2. certT = cert(x.37, x.38, z.28)
id_c = id_c.21
r1 = r1.23
s = s.24
z = verify(s.24, <'TA', id_c.21, r1.23>, x.37)
z.1 = z.28
3. certT = cert(pk(x.37), x.38, z.28)
id_c = id_c.21
r1 = r1.23
s = sign(<'TA', id_c.21, r1.23>, x.37)
z = true
z.1 = z.28
*/
rule (modulo E) CA_INIT_C:
[
Fr( ~r2 ), TACompleteC( <$C, iid>, certT, id_c, r1 ),
!Cert( $C, certC, 'chip' )
]
-->
[
Out( <certC, ~r2, '4', 'c'> ), Out( iid ),
CAInitC( <$C, iid>, certT, id_c, r1, ~r2 )
]
/* has exactly the trivial AC variant */
rule (modulo E) CA_INIT_T:
[
In( <certC, r2, '4', 'c'> ), Fr( ~k ), TAResponseT( <$T, iid>, id_c ),
!Ltk( $T, ~skT, 'terminal' ), !Cert( $T, certT, 'terminal' )
] ]
--[ Eq( verify_cert(certC, 'chip'), true ) ]-> --[ Eq( verify_cert(certC, 'chip'), true ) ]->
[ [
Out( <encaps(~k, cert_pk(certC)), sign(<'TA', id_c, r1>, ~skT), Out( <encaps(~k, cert_pk(certC)),
sign(<'CA', certT, certC, r2, encaps(~k, cert_pk(certC))>, ~skT), '3', sign(<'CA', certT, certC, r2, encaps(~k, cert_pk(certC))>, ~skT), '5',
't'> 't'>
), ),
CAInitT( <$T, iid>, id_c, certC, r2, <~k, encaps(~k, cert_pk(certC))> ) CAInitT( <$T, iid>, id_c, certC, r2, <~k, encaps(~k, cert_pk(certC))> )
] ]
/* /*
rule (modulo AC) TA_RESPONSE_T: rule (modulo AC) CA_INIT_T:
[ [
In( <id_c, r1, certC, r2, '2', 'c'> ), TAInitT( <$T, iid> ), In( <certC, r2, '4', 'c'> ), Fr( ~k ), TAResponseT( <$T, iid>, id_c ),
!Ltk( $T, ~skT, 'terminal' ), !Cert( $T, certT, 'terminal' ), Fr( ~k ) !Ltk( $T, ~skT, 'terminal' ), !Cert( $T, certT, 'terminal' )
] ]
--[ Eq( z.1, true ) ]-> --[ Eq( z.1, true ) ]->
[ [
Out( <encaps(~k, z), sign(<'TA', id_c, r1>, ~skT), Out( <encaps(~k, z),
sign(<'CA', certT, certC, r2, encaps(~k, z)>, ~skT), '3', 't'> sign(<'CA', certT, certC, r2, encaps(~k, z)>, ~skT), '5', 't'>
), ),
CAInitT( <$T, iid>, id_c, certC, r2, <~k, encaps(~k, z)> ) CAInitT( <$T, iid>, id_c, certC, r2, <~k, encaps(~k, z)> )
] ]
variants (modulo AC) variants (modulo AC)
1. certC = certC.20 1. certC = certC.18
z = cert_pk(certC.20) z = cert_pk(certC.18)
z.1 = verify(cert_sig(certC.20), z.1 = verify(cert_sig(certC.18),
<cert_pk(certC.20), cert_id(certC.20), 'chip'>, pk(ca_sk)) <cert_pk(certC.18), cert_id(certC.18), 'chip'>, pk(ca_sk))
2. certC = cert(z.57, sign(<z.57, x.100, 'chip'>, ca_sk), x.100) 2. certC = cert(z.44, sign(<z.44, x.75, 'chip'>, ca_sk), x.75)
z = z.57 z = z.44
z.1 = true z.1 = true
3. certC = cert(z.58, x.101, x.102) 3. certC = cert(z.45, x.76, x.77)
z = z.58 z = z.45
z.1 = verify(x.101, <z.58, x.102, 'chip'>, pk(ca_sk)) z.1 = verify(x.76, <z.45, x.77, 'chip'>, pk(ca_sk))
*/ */
rule (modulo E) TA_COMPLETE_C: rule (modulo E) CA_FINISH_C:
[ [
In( <cip, s1, s2, '3', 't'> ), In( <cip, s, '5', 't'> ), CAInitC( <$C, iid>, certT, id_c, r1, r2 ),
TAChallengeC( <$C, iid>, certT, id_c, r1, r2 ), !Ltk( $C, ~skC, 'chip' ), !Ltk( $C, ~skC, 'chip' ), !Cert( $C, certC, 'chip' )
!Cert( $C, certC, 'chip' )
] ]
--[ --[
Eq( verify(s1, <'TA', id_c, r1>, cert_pk(certT)), true ), Eq( verify(s, <'CA', certT, certC, r2, cip>, cert_pk(certT)), true ),
Eq( verify(s2, <'CA', certT, certC, r2, cip>, cert_pk(certT)), true ),
CompletedTA( $C, iid, cert_id(certT) ),
Completed( kdf(<'KEY', certT, certC, r2, cip>, decaps(cip, ~skC)), Completed( kdf(<'KEY', certT, certC, r2, cip>, decaps(cip, ~skC)),
<certT, certC, r2, cip>, $C, 'chip', cert_id(certT) <certT, certC, r2, cip>, $C, 'chip', cert_id(certT)
) )
]-> ]->
[ [
Out( <kdf(<'CNF', certT, certC, r2, cip>, decaps(cip, ~skC)), '4', 'c'> Out( <kdf(<'CNF', certT, certC, r2, cip>, decaps(cip, ~skC)), '6', 'c'>
), ),
TACompleteC( <$C, iid>, certT, id_c, r1, r2 ) CAFinishC( $C, cert_id(certT),
kdf(<'KEY', certT, certC, r2, cip>, decaps(cip, ~skC))
)
] ]
/* /*
rule (modulo AC) TA_COMPLETE_C: rule (modulo AC) CA_FINISH_C:
[ [
In( <cip, s1, s2, '3', 't'> ), In( <cip, s, '5', 't'> ), CAInitC( <$C, iid>, certT, id_c, r1, r2 ),
TAChallengeC( <$C, iid>, certT, id_c, r1, r2 ), !Ltk( $C, ~skC, 'chip' ), !Ltk( $C, ~skC, 'chip' ), !Cert( $C, certC, 'chip' )
!Cert( $C, certC, 'chip' )
] ]
--[ --[
Eq( z.1, true ), Eq( z.2, true ), CompletedTA( $C, iid, z.3 ), Eq( z.2, true ),
Completed( kdf(<'KEY', certT, certC, r2, cip>, z), Completed( kdf(<'KEY', certT, certC, r2, cip>, z),
<certT, certC, r2, cip>, $C, 'chip', z.3 <certT, certC, r2, cip>, $C, 'chip', z.1
) )
]-> ]->
[ [
Out( <kdf(<'CNF', certT, certC, r2, cip>, z), '4', 'c'> ), Out( <kdf(<'CNF', certT, certC, r2, cip>, z), '6', 'c'> ),
TACompleteC( <$C, iid>, certT, id_c, r1, r2 ) CAFinishC( $C, z.1, kdf(<'KEY', certT, certC, r2, cip>, z) )
] ]
variants (modulo AC) variants (modulo AC)
1. ~skC = ~skC.32 1. ~skC = ~skC.30
certC = certC.33 certC = certC.31
certT = certT.34 certT = certT.32
cip = cip.35 cip = cip.33
id_c = id_c.36 r2 = r2.37
r1 = r1.38 s = s.38
r2 = r2.39 z = decaps(cip.33, ~skC.30)
s1 = s1.40 z.1 = cert_id(certT.32)
s2 = s2.41 z.2 = verify(s.38, <'CA', certT.32, certC.31, r2.37, cip.33>,
z = decaps(cip.35, ~skC.32) cert_pk(certT.32))
z.1 = verify(s1.40, <'TA', id_c.36, r1.38>, cert_pk(certT.34))
z.2 = verify(s2.41, <'CA', certT.34, certC.33, r2.39, cip.35>, 2. ~skC = ~skC.35
cert_pk(certT.34)) certC = certC.36
z.3 = cert_id(certT.34) certT = certT.37
cip = encaps(z.48, pk(~skC.35))
2. ~skC = ~skC.37 r2 = r2.42
certC = certC.38 s = s.43
certT = certT.39 z = z.48
cip = encaps(z.51, pk(~skC.37)) z.1 = cert_id(certT.37)
id_c = id_c.41 z.2 = verify(s.43,
r1 = r1.43 <'CA', certT.37, certC.36, r2.42, encaps(z.48, pk(~skC.35))>,
r2 = r2.44 cert_pk(certT.37))
s1 = s1.45
s2 = s2.46 3. ~skC = ~skC.137
z = z.51 certC = certC.138
z.1 = verify(s1.45, <'TA', id_c.41, r1.43>, cert_pk(certT.39)) certT = cert(x.270, x.271, z.153)
z.2 = verify(s2.46, cip = cip.140
<'CA', certT.39, certC.38, r2.44, encaps(z.51, pk(~skC.37))>, r2 = r2.144
cert_pk(certT.39)) s = s.145
z.3 = cert_id(certT.39) z = decaps(cip.140, ~skC.137)
z.1 = z.153
3. ~skC = ~skC.150 z.2 = verify(s.145,
certC = certC.151 <'CA', cert(x.270, x.271, z.153), certC.138, r2.144, cip.140>, x.270)
certT = cert(x.296, x.297, z.169)
cip = cip.153 4. ~skC = ~skC.138
id_c = id_c.154 certC = certC.139
r1 = r1.156 certT = cert(pk(x.272), x.273, z.154)
r2 = r2.157 cip = cip.141
s1 = s1.158 r2 = r2.145
s2 = s2.159 s = sign(<'CA', cert(pk(x.272), x.273, z.154), certC.139, r2.145,
z = decaps(cip.153, ~skC.150) cip.141>,
z.1 = verify(s1.158, <'TA', id_c.154, r1.156>, x.296) x.272)
z.2 = verify(s2.159, z = decaps(cip.141, ~skC.138)
<'CA', cert(x.296, x.297, z.169), certC.151, r2.157, cip.153>, x.296) z.1 = z.154
z.3 = z.169
4. ~skC = ~skC.150
certC = certC.151
certT = cert(pk(x.296), x.297, z.169)
cip = cip.153
id_c = id_c.154
r1 = r1.156
r2 = r2.157
s1 = sign(<'TA', id_c.154, r1.156>, x.296)
s2 = s2.159
z = decaps(cip.153, ~skC.150)
z.1 = true
z.2 = verify(s2.159,
<'CA', cert(pk(x.296), x.297, z.169), certC.151, r2.157, cip.153>,
pk(x.296))
z.3 = z.169
5. ~skC = ~skC.151
certC = certC.152
certT = cert(pk(x.298), x.299, z.170)
cip = cip.154
id_c = id_c.155
r1 = r1.157
r2 = r2.158
s1 = s1.159
s2 = sign(<'CA', cert(pk(x.298), x.299, z.170), certC.152, r2.158,
cip.154>,
x.298)
z = decaps(cip.154, ~skC.151)
z.1 = verify(s1.159, <'TA', id_c.155, r1.157>, pk(x.298))
z.2 = true
z.3 = z.170
6. ~skC = ~skC.151
certC = certC.152
certT = cert(pk(x.298), x.299, z.170)
cip = cip.154
id_c = id_c.155
r1 = r1.157
r2 = r2.158
s1 = sign(<'TA', id_c.155, r1.157>, x.298)
s2 = sign(<'CA', cert(pk(x.298), x.299, z.170), certC.152, r2.158,
cip.154>,
x.298)
z = decaps(cip.154, ~skC.151)
z.1 = true
z.2 = true
z.3 = z.170
7. ~skC = ~skC.152
certC = certC.153
certT = cert(x.300, x.301, z.171)
cip = encaps(z.166, pk(~skC.152))
id_c = id_c.156
r1 = r1.158
r2 = r2.159
s1 = s1.160
s2 = s2.161
z = z.166
z.1 = verify(s1.160, <'TA', id_c.156, r1.158>, x.300)
z.2 = verify(s2.161,
<'CA', cert(x.300, x.301, z.171), certC.153, r2.159,
encaps(z.166, pk(~skC.152))>,
x.300)
z.3 = z.171
8. ~skC = ~skC.152
certC = certC.153
certT = cert(pk(x.300), x.301, z.171)
cip = encaps(z.166, pk(~skC.152))
id_c = id_c.156
r1 = r1.158
r2 = r2.159
s1 = s1.160
s2 = sign(<'CA', cert(pk(x.300), x.301, z.171), certC.153, r2.159,
encaps(z.166, pk(~skC.152))>,
x.300)
z = z.166
z.1 = verify(s1.160, <'TA', id_c.156, r1.158>, pk(x.300))
z.2 = true z.2 = true
z.3 = z.171
5. ~skC = ~skC.139
9. ~skC = ~skC.152 certC = certC.140
certC = certC.153 certT = cert(x.274, x.275, z.155)
certT = cert(pk(x.300), x.301, z.171) cip = encaps(z.152, pk(~skC.139))
cip = encaps(z.166, pk(~skC.152)) r2 = r2.146
id_c = id_c.156 s = s.147
r1 = r1.158 z = z.152
r2 = r2.159 z.1 = z.155
s1 = sign(<'TA', id_c.156, r1.158>, x.300) z.2 = verify(s.147,
s2 = s2.161 <'CA', cert(x.274, x.275, z.155), certC.140, r2.146,
z = z.166 encaps(z.152, pk(~skC.139))>,
z.1 = true x.274)
z.2 = verify(s2.161,
<'CA', cert(pk(x.300), x.301, z.171), certC.153, r2.159, 6. ~skC = ~skC.139
encaps(z.166, pk(~skC.152))>, certC = certC.140
pk(x.300)) certT = cert(pk(x.274), x.275, z.155)
z.3 = z.171 cip = encaps(z.152, pk(~skC.139))
r2 = r2.146
10. ~skC = ~skC.152 s = sign(<'CA', cert(pk(x.274), x.275, z.155), certC.140, r2.146,
certC = certC.153 encaps(z.152, pk(~skC.139))>,
certT = cert(pk(x.300), x.301, z.171) x.274)
cip = encaps(z.166, pk(~skC.152)) z = z.152
id_c = id_c.156 z.1 = z.155
r1 = r1.158
r2 = r2.159
s1 = sign(<'TA', id_c.156, r1.158>, x.300)
s2 = sign(<'CA', cert(pk(x.300), x.301, z.171), certC.153, r2.159,
encaps(z.166, pk(~skC.152))>,
x.300)
z = z.166
z.1 = true
z.2 = true z.2 = true
z.3 = z.171
*/ */
rule (modulo E) CA_FINISH_T: rule (modulo E) CA_FINISH_T:
[ [
In( <kCNF_C, '4', 'c'> ), In( <kCNF_c, '6', 'c'> ),
CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ), CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ),
!Cert( $T, certT, 'terminal' ) !Cert( $T, certT, 'terminal' )
] ]
--[ --[
Eq( kdf(<'CNF', certT, certC, r2, cip>, k), kCNF_C ), Eq( kdf(<'CNF', certT, certC, r2, cip>, k), kCNF_c ),
Completed( kdf(<'KEY', certT, certC, r2, cip>, k), Completed( kdf(<'KEY', certT, certC, r2, cip>, k),
<certT, certC, r2, cip>, $T, 'terminal', cert_id(certC) <certT, certC, r2, cip>, $T, 'terminal', cert_id(certC)
), ),
...@@ -375,12 +340,12 @@ rule (modulo E) CA_FINISH_T: ...@@ -375,12 +340,12 @@ rule (modulo E) CA_FINISH_T:
/* /*
rule (modulo AC) CA_FINISH_T: rule (modulo AC) CA_FINISH_T:
[ [
In( <kCNF_C, '4', 'c'> ), In( <kCNF_c, '6', 'c'> ),
CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ), CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ),
!Cert( $T, certT, 'terminal' ) !Cert( $T, certT, 'terminal' )
] ]
--[ --[
Eq( kdf(<'CNF', certT, certC, r2, cip>, k), kCNF_C ), Eq( kdf(<'CNF', certT, certC, r2, cip>, k), kCNF_c ),
Completed( kdf(<'KEY', certT, certC, r2, cip>, k), Completed( kdf(<'KEY', certT, certC, r2, cip>, k),
<certT, certC, r2, cip>, $T, 'terminal', z <certT, certC, r2, cip>, $T, 'terminal', z
), ),
...@@ -2240,10 +2205,9 @@ guarded formula characterizing all satisfying traces: ...@@ -2240,10 +2205,9 @@ guarded formula characterizing all satisfying traces:
*/ */
simplify simplify
solve( Completed( k, sid, C, 'chip', T ) @ #i ) solve( Completed( k, sid, C, 'chip', T ) @ #i )
case TA_COMPLETE_C case CA_FINISH_C
solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 solve( CAInitC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 ) ▶₁ #i )
) ▶₁ #i ) case CA_INIT_C
case TA_CHALLENGE_C
solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i )
case Generate_chip_key_pair case Generate_chip_key_pair
solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) solve( !Cert( $C, certC, 'chip' ) ▶₃ #i )
...@@ -2260,43 +2224,50 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -2260,43 +2224,50 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
solve( CAInitT( <$T, iid.1>, id_c.1, solve( CAInitT( <$T, iid.1>, id_c.1,
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <z, cip> cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <z, cip>
) ▶₁ #j ) ) ▶₁ #j )
case TA_RESPONSE_T case CA_INIT_T
solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T), solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T),
'terminal' 'terminal'
) ▶₂ #j ) ) ▶₂ #j )
case CA_Sign_ltk case CA_Sign_ltk
solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.3 )
case TA_RESPONSE_T
solve( !KU( sign(<'CA', solve( !KU( sign(<'CA',
cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~ltk.1) ~ltk.1)
) @ #vk.5 ) ) @ #vk.3 )
case CA_INIT_T
solve( !KU( sign(<'TA', ~id_c, ~r1>, ~skT) ) @ #vk.11 )
case TA_RESPONSE_T case TA_RESPONSE_T
solve( !KU( cert(z, sign(<z, x, 'chip'>, ca_sk), x) ) @ #vk.34 ) solve( !KU( ~r2 ) @ #vk.28 )
case CA_Sign_ltk case CA_INIT_C
solve( !KU( ~r2 ) @ #vk.30 ) solve( !KU( ~id_c ) @ #vk.34 )
case TA_CHALLENGE_C
solve( !KU( ~id_c ) @ #vk.33 )
case TA_CHALLENGE_C case TA_CHALLENGE_C
solve( !KU( ~r1 ) @ #vk.34 ) solve( !KU( ~r1 ) @ #vk.35 )
case TA_CHALLENGE_C case TA_CHALLENGE_C
solve( !KU( cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T) solve( !KU( cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T)
) @ #vk.20 ) ) @ #vk.19 )
case CA_Sign_ltk case CA_Sign_ltk
solve( !KU( kdf(<'CNF', solve( !KU( kdf(<'CNF',
cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~k) ~k)
) @ #vk.24 ) ) @ #vk.23 )
case TA_COMPLETE_C case CA_FINISH_C
solve( !KU( cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C) solve( !KU( cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C)
) @ #vk.33 ) ) @ #vk.31 )
case CA_Sign_ltk case CA_INIT_C
solve( !KU( encaps(~k, pk(~ltk)) ) @ #vk.21 ) solve( !KU( sign(<'TA', ~id_c.2, ~r1.2>, x) ) @ #vk.38 )
case TA_RESPONSE_T case TA_RESPONSE_T
solve( !KU( cert(pk(~skT.2), sign(<pk(~skT.2), z, 'terminal'>, ca_sk), z)
) @ #vk.40 )
case CA_Sign_ltk
solve( !KU( ~id_c.2 ) @ #vk.42 )
case TA_CHALLENGE_C
solve( !KU( ~r1.1 ) @ #vk.43 )
case TA_CHALLENGE_C
solve( !KU( encaps(~k, pk(~ltk)) ) @ #vk.24 )
case CA_INIT_T
SOLVED // trace found SOLVED // trace found
qed qed
qed qed
...@@ -2315,6 +2286,9 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -2315,6 +2286,9 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
qed qed
qed qed
qed qed
qed
qed
qed
lemma two_session_exist: lemma two_session_exist:
exists-trace exists-trace
...@@ -2338,10 +2312,9 @@ guarded formula characterizing all satisfying traces: ...@@ -2338,10 +2312,9 @@ guarded formula characterizing all satisfying traces:
*/ */
simplify simplify
solve( Completed( k, sid, C, 'chip', T ) @ #i ) solve( Completed( k, sid, C, 'chip', T ) @ #i )
case TA_COMPLETE_C case CA_FINISH_C
solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 solve( CAInitC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 ) ▶₁ #i )
) ▶₁ #i ) case CA_INIT_C
case TA_CHALLENGE_C
solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i )
case Generate_chip_key_pair case Generate_chip_key_pair
solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) solve( !Cert( $C, certC, 'chip' ) ▶₃ #i )
...@@ -2358,17 +2331,16 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -2358,17 +2331,16 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
solve( CAInitT( <$T, iid.1>, id_c.1, solve( CAInitT( <$T, iid.1>, id_c.1,
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <z, cip> cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <z, cip>
) ▶₁ #j ) ) ▶₁ #j )
case TA_RESPONSE_T case CA_INIT_T
solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T), solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T),
'terminal' 'terminal'
) ▶₂ #j ) ) ▶₂ #j )
case CA_Sign_ltk case CA_Sign_ltk
solve( Completed( k2, sid2, $C, 'chip', $T ) @ #i2 ) solve( Completed( k2, sid2, $C, 'chip', $T ) @ #i2 )
case TA_COMPLETE_C case CA_FINISH_C
solve( TAChallengeC( <$C, iid.1>, cert(pk(x), x.1, $T), id_c.1, r1.1, solve( CAInitC( <$C, iid.1>, cert(pk(x), x.1, $T), id_c.1, r1.1, r2.1
r2.1
) ▶₁ #i2 ) ) ▶₁ #i2 )
case TA_CHALLENGE_C case CA_INIT_C
solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i2 ) solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i2 )
case Generate_chip_key_pair case Generate_chip_key_pair
solve( !Cert( $C, certC, 'chip' ) ▶₃ #i2 ) solve( !Cert( $C, certC, 'chip' ) ▶₃ #i2 )
...@@ -2388,51 +2360,46 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -2388,51 +2360,46 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
cert(pk(~ltk.2), sign(<pk(~ltk.2), $C, 'chip'>, ca_sk), $C), ~r2.1, cert(pk(~ltk.2), sign(<pk(~ltk.2), $C, 'chip'>, ca_sk), $C), ~r2.1,
<z, cip> <z, cip>
) ▶₁ #j2 ) ) ▶₁ #j2 )
case TA_RESPONSE_T case CA_INIT_T
solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T), solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T),
'terminal' 'terminal'
) ▶₂ #j2 ) ) ▶₂ #j2 )
case CA_Sign_ltk case CA_Sign_ltk
solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.3 )
case TA_RESPONSE_T
solve( !KU( sign(<'CA', solve( !KU( sign(<'CA',
cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk),
$T), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~ltk.1) ~ltk.1)
) @ #vk.5 ) ) @ #vk.3 )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( sign(<'TA', ~id_c.1, ~r1.1>, ~ltk.1) ) @ #vk.40 ) solve( !KU( sign(<'TA', ~id_c, ~r1>, ~skT) ) @ #vk.15 )
case TA_RESPONSE_T case TA_RESPONSE_T
solve( !KU( sign(<'CA', solve( !KU( sign(<'CA',
cert(pk(~ltk.1), cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk),
sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), $T),
cert(pk(~skC), sign(<pk(~skC), $C, 'chip'>, ca_sk), $C), cert(pk(~skC), sign(<pk(~skC), $C, 'chip'>, ca_sk), $C),
~r2.1, encaps(~k.1, pk(~skC))>, ~r2.1, encaps(~k.1, pk(~skC))>,
~ltk.1) ~ltk.1)
) @ #vk.43 ) ) @ #vk.43 )
case CA_INIT_T
solve( !KU( sign(<'TA', ~id_c.1, ~r1.1>, ~ltk.1) ) @ #vk.45 )
case TA_RESPONSE_T case TA_RESPONSE_T
solve( !KU( cert(z, sign(<z, x, 'chip'>, ca_sk), x) ) @ #vk.54 ) solve( !KU( ~r2 ) @ #vk.41 )
case CA_Sign_ltk case CA_INIT_C
solve( !KU( cert(z, sign(<z, x, 'chip'>, ca_sk), x) ) @ #vk.60 ) solve( !KU( ~r2.1 ) @ #vk.51 )
case CA_Sign_ltk case CA_INIT_C
solve( !KU( ~r2 ) @ #vk.47 ) solve( !KU( ~id_c ) @ #vk.54 )
case TA_CHALLENGE_C
solve( !KU( ~r2.1 ) @ #vk.55 )
case TA_CHALLENGE_C
solve( !KU( ~id_c ) @ #vk.56 )
case TA_CHALLENGE_C case TA_CHALLENGE_C
solve( !KU( ~r1 ) @ #vk.57 ) solve( !KU( ~r1 ) @ #vk.55 )
case TA_CHALLENGE_C case TA_CHALLENGE_C
solve( !KU( ~id_c.1 ) @ #vk.59 ) solve( !KU( ~id_c.1 ) @ #vk.56 )
case TA_CHALLENGE_C case TA_CHALLENGE_C
solve( !KU( ~r1.1 ) @ #vk.60 ) solve( !KU( ~r1.1 ) @ #vk.57 )
case TA_CHALLENGE_C case TA_CHALLENGE_C
solve( !KU( cert(pk(~skT), solve( !KU( cert(pk(~skT),
sign(<pk(~skT), $T, 'terminal'>, ca_sk), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T)
$T) ) @ #vk.32 )
) @ #vk.39 )
case CA_Sign_ltk case CA_Sign_ltk
solve( !KU( kdf(<'CNF', solve( !KU( kdf(<'CNF',
cert(pk(~skT), cert(pk(~skT),
...@@ -2440,26 +2407,36 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -2440,26 +2407,36 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
ca_sk), ca_sk),
$T), $T),
cert(pk(~ltk), cert(pk(~ltk),
sign(<pk(~ltk), $C, 'chip'>, sign(<pk(~ltk), $C, 'chip'>, ca_sk),
ca_sk),
$C), $C),
~r2, encaps(~k, pk(~ltk))>, ~r2, encaps(~k, pk(~ltk))>,
~k) ~k)
) @ #vk.42 ) ) @ #vk.36 )
case TA_COMPLETE_C case CA_FINISH_C
solve( !KU( cert(pk(~ltk), solve( !KU( cert(pk(~ltk),
sign(<pk(~ltk), $C, 'chip'>, ca_sk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C)
$C) ) @ #vk.47 )
) @ #vk.52 ) case CA_INIT_C
case CA_Sign_ltk solve( !KU( sign(<'TA', ~id_c.4, ~r1.4>, x) ) @ #vk.60 )
solve( !KU( encaps(~k, pk(~ltk)) ) @ #vk.37 )
case TA_RESPONSE_T case TA_RESPONSE_T
solve( !KU( cert(pk(~skT.3),
sign(<pk(~skT.3), z, 'terminal'>,
ca_sk),
z)
) @ #vk.62 )
case CA_Sign_ltk
solve( !KU( ~id_c.4 ) @ #vk.64 )
case TA_CHALLENGE_C
solve( !KU( ~r1.3 ) @ #vk.65 )
case TA_CHALLENGE_C
solve( !KU( encaps(~k, pk(~ltk)) ) @ #vk.36 )
case CA_INIT_T
solve( !KU( cert(pk(~ltk.1), solve( !KU( cert(pk(~ltk.1),
sign(<pk(~ltk.1), $T, 'terminal' sign(<pk(~ltk.1), $T,
>, 'terminal'>,
ca_sk), ca_sk),
$T) $T)
) @ #vk.55 ) ) @ #vk.61 )
case CA_Sign_ltk case CA_Sign_ltk
solve( !KU( kdf(<'CNF', solve( !KU( kdf(<'CNF',
cert(pk(~ltk.1), cert(pk(~ltk.1),
...@@ -2468,23 +2445,41 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -2468,23 +2445,41 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
ca_sk), ca_sk),
$T), $T),
cert(pk(~skC), cert(pk(~skC),
sign(<pk(~skC), $C, 'chip' sign(<pk(~skC), $C,
>, 'chip'>,
ca_sk), ca_sk),
$C), $C),
~r2.1, encaps(~k.1, pk(~skC))>, ~r2.1,
encaps(~k.1, pk(~skC))>,
~k.1) ~k.1)
) @ #vk.56 ) ) @ #vk.62 )
case TA_COMPLETE_C case CA_FINISH_C
solve( !KU( cert(pk(~skC), solve( !KU( cert(pk(~skC),
sign(<pk(~skC), $C, 'chip'>, sign(<pk(~skC), $C,
'chip'>,
ca_sk), ca_sk),
$C) $C)
) @ #vk.59 ) ) @ #vk.63 )
case CA_Sign_ltk case CA_INIT_C
solve( !KU( encaps(~k.1, pk(~skC)) solve( !KU( sign(<'TA', ~id_c.5, ~r1.5>,
) @ #vk.57 ) x)
) @ #vk.68 )
case TA_RESPONSE_T case TA_RESPONSE_T
solve( !KU( cert(pk(~skT.4),
sign(<pk(~skT.4), z,
'terminal'>,
ca_sk),
z)
) @ #vk.70 )
case CA_Sign_ltk
solve( !KU( ~id_c.5 ) @ #vk.72 )
case TA_CHALLENGE_C
solve( !KU( ~r1.4 ) @ #vk.73 )
case TA_CHALLENGE_C
solve( !KU( encaps(~k.1,
pk(~skC))
) @ #vk.71 )
case CA_INIT_T
SOLVED // trace found SOLVED // trace found
qed qed
qed qed
...@@ -2520,6 +2515,12 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -2520,6 +2515,12 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
qed qed
qed qed
qed qed
qed
qed
qed
qed
qed
qed
lemma weak_agreement_C: lemma weak_agreement_C:
all-traces all-traces
...@@ -2539,7 +2540,7 @@ guarded formula characterizing all counter-examples: ...@@ -2539,7 +2540,7 @@ guarded formula characterizing all counter-examples:
*/ */
simplify simplify
solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t )
case TA_RESPONSE_T case CA_INIT_T
solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t ) solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t )
case CA_Sign_ltk case CA_Sign_ltk
solve( Completed( k.1, solve( Completed( k.1,
...@@ -2547,11 +2548,11 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) ...@@ -2547,11 +2548,11 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t )
cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), r2, encaps(~k, z)>, cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), r2, encaps(~k, z)>,
C, 'chip', T.1 C, 'chip', T.1
) @ #i ) ) @ #i )
case TA_COMPLETE_C case CA_FINISH_C
solve( TAChallengeC( <$C, iid>, solve( CAInitC( <$C, iid>,
cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), id_c, r1, r2 cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), id_c, r1, r2
) ▶₁ #i ) ) ▶₁ #i )
case TA_CHALLENGE_C case CA_INIT_C
solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i )
case Generate_chip_key_pair case Generate_chip_key_pair
solve( !Cert( $C, cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), 'chip' solve( !Cert( $C, cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), 'chip'
...@@ -2583,7 +2584,7 @@ guarded formula characterizing all counter-examples: ...@@ -2583,7 +2584,7 @@ guarded formula characterizing all counter-examples:
*/ */
simplify simplify
solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t )
case TA_RESPONSE_T case CA_INIT_T
solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t ) solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t )
case CA_Sign_ltk case CA_Sign_ltk
solve( Completed( k.1, solve( Completed( k.1,
...@@ -2595,48 +2596,48 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) ...@@ -2595,48 +2596,48 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t )
solve( CAInitT( <$T.1, iid>, id_c, solve( CAInitT( <$T.1, iid>, id_c,
cert(z, sign(<z, C, 'chip'>, ca_sk), C), r2, <k.1, encaps(~k, z)> cert(z, sign(<z, C, 'chip'>, ca_sk), C), r2, <k.1, encaps(~k, z)>
) ▶₁ #i ) ) ▶₁ #i )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( kdf(<'CNF', solve( !KU( kdf(<'CNF',
cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T),
cert(z, sign(<z, C, 'chip'>, ca_sk), C), r2, encaps(~k, z)>, cert(z, sign(<z, C, 'chip'>, ca_sk), C), r2, encaps(~k, z)>,
~k) ~k)
) @ #vk.1 ) ) @ #vk.1 )
case TA_COMPLETE_C case CA_FINISH_C
by contradiction /* from formulas */ by contradiction /* from formulas */
next next
case c_kdf case c_kdf
solve( !KU( ~k ) @ #vk.18 ) solve( !KU( ~k ) @ #vk.20 )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( cert(pk(sk), sign(<pk(sk), C, 'chip'>, ca_sk), C) solve( !KU( cert(pk(sk), sign(<pk(sk), C, 'chip'>, ca_sk), C)
) @ #vk.13 ) ) @ #vk.12 )
case CA_Sign_ltk case CA_INIT_C
solve( !KU( ~ltk.1 ) @ #vk.23 ) solve( !KU( ~ltk.1 ) @ #vk.25 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
next next
case TA_CHALLENGE_C case CA_Sign_ltk
solve( !KU( ~ltk.1 ) @ #vk.23 ) solve( !KU( ~ltk.1 ) @ #vk.25 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
next next
case c_cert case c_cert
solve( !KU( sign(<pk(sk), C, 'chip'>, ca_sk) ) @ #vk.25 ) solve( !KU( sign(<pk(sk), C, 'chip'>, ca_sk) ) @ #vk.27 )
case CA_Sign_ltk case CA_INIT_C
solve( !KU( ~ltk.1 ) @ #vk.24 ) solve( !KU( ~ltk.1 ) @ #vk.26 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
next next
case TA_CHALLENGE_C case CA_Sign_ltk
solve( !KU( ~ltk.1 ) @ #vk.24 ) solve( !KU( ~ltk.1 ) @ #vk.26 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
next next
case c_sign case c_sign
by solve( !KU( ca_sk ) @ #vk.29 ) by solve( !KU( ca_sk ) @ #vk.31 )
qed qed
qed qed
qed qed
...@@ -2664,7 +2665,7 @@ guarded formula characterizing all counter-examples: ...@@ -2664,7 +2665,7 @@ guarded formula characterizing all counter-examples:
*/ */
simplify simplify
solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t )
case TA_RESPONSE_T case CA_INIT_T
solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t ) solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t )
case CA_Sign_ltk case CA_Sign_ltk
solve( Completed( k.1, solve( Completed( k.1,
...@@ -2672,11 +2673,11 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) ...@@ -2672,11 +2673,11 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t )
cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), r2, encaps(~k, z)>, cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), r2, encaps(~k, z)>,
C, 'chip', T.1 C, 'chip', T.1
) @ #i ) ) @ #i )
case TA_COMPLETE_C case CA_FINISH_C
solve( TAChallengeC( <$C, iid>, solve( CAInitC( <$C, iid>,
cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), id_c, r1, r2 cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), id_c, r1, r2
) ▶₁ #i ) ) ▶₁ #i )
case TA_CHALLENGE_C case CA_INIT_C
solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i )
case Generate_chip_key_pair case Generate_chip_key_pair
solve( !Cert( $C, cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), 'chip' solve( !Cert( $C, cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), 'chip'
...@@ -2687,24 +2688,24 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) ...@@ -2687,24 +2688,24 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t )
by contradiction /* from formulas */ by contradiction /* from formulas */
next next
case split_case_2 case split_case_2
solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.18 )
case TA_RESPONSE_T
solve( !KU( sign(<'CA', solve( !KU( sign(<'CA',
cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~ltk.1) ~ltk.1)
) @ #vk.21 ) ) @ #vk.20 )
case CA_INIT_T
solve( !KU( sign(<'TA', ~id_c, ~r1>, ~skT) ) @ #vk.28 )
case TA_RESPONSE_T case TA_RESPONSE_T
solve( !KU( kdf(<'CNF', solve( !KU( kdf(<'CNF',
cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~k) ~k)
) @ #vk.4 ) ) @ #vk.5 )
case c_kdf case c_kdf
solve( !KU( ~k ) @ #vk.40 ) solve( !KU( ~k ) @ #vk.40 )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( ~ltk ) @ #vk.42 ) solve( !KU( ~ltk ) @ #vk.42 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
...@@ -2713,14 +2714,14 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) ...@@ -2713,14 +2714,14 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t )
qed qed
next next
case c_sign case c_sign
solve( !KU( ~ltk.1 ) @ #vk.40 ) solve( !KU( ~skT ) @ #vk.33 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
qed qed
next next
case c_sign case c_sign
solve( !KU( ~ltk.1 ) @ #vk.29 ) solve( !KU( ~ltk.1 ) @ #vk.36 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
...@@ -2751,7 +2752,7 @@ guarded formula characterizing all counter-examples: ...@@ -2751,7 +2752,7 @@ guarded formula characterizing all counter-examples:
*/ */
simplify simplify
solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t )
case TA_RESPONSE_T case CA_INIT_T
solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t ) solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t )
case CA_Sign_ltk case CA_Sign_ltk
solve( Completed( k.1, solve( Completed( k.1,
...@@ -2763,48 +2764,48 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) ...@@ -2763,48 +2764,48 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t )
solve( CAInitT( <$T.1, iid>, id_c, solve( CAInitT( <$T.1, iid>, id_c,
cert(z, sign(<z, C, 'chip'>, ca_sk), C), r2, <k.1, encaps(~k, z)> cert(z, sign(<z, C, 'chip'>, ca_sk), C), r2, <k.1, encaps(~k, z)>
) ▶₁ #i ) ) ▶₁ #i )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( kdf(<'CNF', solve( !KU( kdf(<'CNF',
cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T),
cert(z, sign(<z, C, 'chip'>, ca_sk), C), r2, encaps(~k, z)>, cert(z, sign(<z, C, 'chip'>, ca_sk), C), r2, encaps(~k, z)>,
~k) ~k)
) @ #vk.1 ) ) @ #vk.1 )
case TA_COMPLETE_C case CA_FINISH_C
by contradiction /* from formulas */ by contradiction /* from formulas */
next next
case c_kdf case c_kdf
solve( !KU( ~k ) @ #vk.18 ) solve( !KU( ~k ) @ #vk.20 )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( cert(pk(sk), sign(<pk(sk), C, 'chip'>, ca_sk), C) solve( !KU( cert(pk(sk), sign(<pk(sk), C, 'chip'>, ca_sk), C)
) @ #vk.13 ) ) @ #vk.12 )
case CA_Sign_ltk case CA_INIT_C
solve( !KU( ~ltk.1 ) @ #vk.23 ) solve( !KU( ~ltk.1 ) @ #vk.25 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
next next
case TA_CHALLENGE_C case CA_Sign_ltk
solve( !KU( ~ltk.1 ) @ #vk.23 ) solve( !KU( ~ltk.1 ) @ #vk.25 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
next next
case c_cert case c_cert
solve( !KU( sign(<pk(sk), C, 'chip'>, ca_sk) ) @ #vk.25 ) solve( !KU( sign(<pk(sk), C, 'chip'>, ca_sk) ) @ #vk.27 )
case CA_Sign_ltk case CA_INIT_C
solve( !KU( ~ltk.1 ) @ #vk.24 ) solve( !KU( ~ltk.1 ) @ #vk.26 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
next next
case TA_CHALLENGE_C case CA_Sign_ltk
solve( !KU( ~ltk.1 ) @ #vk.24 ) solve( !KU( ~ltk.1 ) @ #vk.26 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
next next
case c_sign case c_sign
by solve( !KU( ca_sk ) @ #vk.29 ) by solve( !KU( ca_sk ) @ #vk.31 )
qed qed
qed qed
qed qed
...@@ -2830,7 +2831,7 @@ guarded formula characterizing all counter-examples: ...@@ -2830,7 +2831,7 @@ guarded formula characterizing all counter-examples:
*/ */
simplify simplify
solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t )
case TA_RESPONSE_T case CA_INIT_T
solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t ) solve( !Cert( $T, certT, 'terminal' ) ▶₂ #t )
case CA_Sign_ltk case CA_Sign_ltk
solve( Completed( k.1, solve( Completed( k.1,
...@@ -2838,60 +2839,60 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t ) ...@@ -2838,60 +2839,60 @@ solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #t )
cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), r2, encaps(~k, z)>, cert(z, sign(<z, z.1, 'chip'>, ca_sk), z.1), r2, encaps(~k, z)>,
A, role, B A, role, B
) @ #i ) ) @ #i )
case CA_FINISH_C
by contradiction /* from formulas */
next
case CA_FINISH_T case CA_FINISH_T
solve( CAInitT( <$T.1, iid>, id_c, solve( CAInitT( <$T.1, iid>, id_c,
cert(z, sign(<z, B, 'chip'>, ca_sk), B), r2, <k.1, encaps(~k, z)> cert(z, sign(<z, B, 'chip'>, ca_sk), B), r2, <k.1, encaps(~k, z)>
) ▶₁ #i ) ) ▶₁ #i )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( kdf(<'CNF', solve( !KU( kdf(<'CNF',
cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk), sign(<pk(~ltk), $T, 'terminal'>, ca_sk), $T),
cert(z, sign(<z, B, 'chip'>, ca_sk), B), r2, encaps(~k, z)>, cert(z, sign(<z, B, 'chip'>, ca_sk), B), r2, encaps(~k, z)>,
~k) ~k)
) @ #vk.1 ) ) @ #vk.1 )
case TA_COMPLETE_C case CA_FINISH_C
by contradiction /* from formulas */ by contradiction /* from formulas */
next next
case c_kdf case c_kdf
solve( !KU( ~k ) @ #vk.18 ) solve( !KU( ~k ) @ #vk.20 )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( cert(pk(sk), sign(<pk(sk), B, 'chip'>, ca_sk), B) solve( !KU( cert(pk(sk), sign(<pk(sk), B, 'chip'>, ca_sk), B)
) @ #vk.13 ) ) @ #vk.12 )
case CA_Sign_ltk case CA_INIT_C
solve( !KU( ~ltk.1 ) @ #vk.23 ) solve( !KU( ~ltk.1 ) @ #vk.25 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
next next
case TA_CHALLENGE_C case CA_Sign_ltk
solve( !KU( ~ltk.1 ) @ #vk.23 ) solve( !KU( ~ltk.1 ) @ #vk.25 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
next next
case c_cert case c_cert
solve( !KU( sign(<pk(sk), B, 'chip'>, ca_sk) ) @ #vk.25 ) solve( !KU( sign(<pk(sk), B, 'chip'>, ca_sk) ) @ #vk.27 )
case CA_Sign_ltk case CA_INIT_C
solve( !KU( ~ltk.1 ) @ #vk.24 ) solve( !KU( ~ltk.1 ) @ #vk.26 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
next next
case TA_CHALLENGE_C case CA_Sign_ltk
solve( !KU( ~ltk.1 ) @ #vk.24 ) solve( !KU( ~ltk.1 ) @ #vk.26 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
next next
case c_sign case c_sign
by solve( !KU( ca_sk ) @ #vk.29 ) by solve( !KU( ca_sk ) @ #vk.31 )
qed qed
qed qed
qed qed
qed qed
qed qed
next
case TA_COMPLETE_C
by contradiction /* from formulas */
qed qed
qed qed
qed qed
...@@ -2916,9 +2917,34 @@ solve( (¬(#i = #j)) ∥ (¬(sid = sid2)) ) ...@@ -2916,9 +2917,34 @@ solve( (¬(#i = #j)) ∥ (¬(sid = sid2)) )
solve( (#i < #j) ∥ (#j < #i) ) solve( (#i < #j) ∥ (#j < #i) )
case case_1 case case_1
solve( Completed( k, sid, A, role, B ) @ #i ) solve( Completed( k, sid, A, role, B ) @ #i )
case CA_FINISH_C
solve( CAInitC( <$C, iid>, cert(pk(x), x.1, B), id_c, r1, r2 ) ▶₁ #i )
case CA_INIT_C
solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i )
case Generate_chip_key_pair
solve( !Cert( $C, certC, 'chip' ) ▶₃ #i )
case CA_Sign_ltk
solve( Completed( kdf(<'KEY',
cert(pk(x), sign(<pk(x), B, 'terminal'>, ca_sk), B),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cip>,
z),
sid2, $C, 'chip', B
) @ #j )
case CA_FINISH_C
solve( CAInitC( <$C, iid.1>,
cert(pk(x), sign(<pk(x), B, 'terminal'>, ca_sk), B), id_c.1, r1.1, ~r2
) ▶₁ #j )
case CA_INIT_C
by contradiction /* cyclic */
qed
qed
qed
qed
qed
next
case CA_FINISH_T case CA_FINISH_T
solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #i ) solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #i )
case TA_RESPONSE_T case CA_INIT_T
solve( !Cert( $T, certT, 'terminal' ) ▶₂ #i ) solve( !Cert( $T, certT, 'terminal' ) ▶₂ #i )
case CA_Sign_ltk case CA_Sign_ltk
solve( Completed( kdf(<'KEY', solve( Completed( kdf(<'KEY',
...@@ -2931,17 +2957,19 @@ solve( (¬(#i = #j)) ∥ (¬(sid = sid2)) ) ...@@ -2931,17 +2957,19 @@ solve( (¬(#i = #j)) ∥ (¬(sid = sid2)) )
solve( CAInitT( <$T, iid.1>, id_c.1, solve( CAInitT( <$T, iid.1>, id_c.1,
cert(z, sign(<z, B, 'chip'>, ca_sk), B), r2, <~k, encaps(~k, z)> cert(z, sign(<z, B, 'chip'>, ca_sk), B), r2, <~k, encaps(~k, z)>
) ▶₁ #j ) ) ▶₁ #j )
case TA_RESPONSE_T case CA_INIT_T
by contradiction /* cyclic */ by contradiction /* cyclic */
qed qed
qed qed
qed qed
qed qed
qed
next next
case TA_COMPLETE_C case case_2
solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, B), id_c, r1, r2 solve( Completed( k, sid, A, role, B ) @ #i )
) ▶₁ #i ) case CA_FINISH_C
case TA_CHALLENGE_C solve( CAInitC( <$C, iid>, cert(pk(x), x.1, B), id_c, r1, r2 ) ▶₁ #i )
case CA_INIT_C
solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i )
case Generate_chip_key_pair case Generate_chip_key_pair
solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) solve( !Cert( $C, certC, 'chip' ) ▶₃ #i )
...@@ -2952,24 +2980,21 @@ solve( (¬(#i = #j)) ∥ (¬(sid = sid2)) ) ...@@ -2952,24 +2980,21 @@ solve( (¬(#i = #j)) ∥ (¬(sid = sid2)) )
z), z),
sid2, $C, 'chip', B sid2, $C, 'chip', B
) @ #j ) ) @ #j )
case TA_COMPLETE_C case CA_FINISH_C
solve( TAChallengeC( <$C, iid.1>, solve( CAInitC( <$C, iid.1>,
cert(pk(x), sign(<pk(x), B, 'terminal'>, ca_sk), B), id_c.1, r1.1, ~r2 cert(pk(x), sign(<pk(x), B, 'terminal'>, ca_sk), B), id_c.1, r1.1, ~r2
) ▶₁ #j ) ) ▶₁ #j )
case TA_CHALLENGE_C case CA_INIT_C
by contradiction /* cyclic */ by contradiction /* cyclic */
qed qed
qed qed
qed qed
qed qed
qed qed
qed
next next
case case_2
solve( Completed( k, sid, A, role, B ) @ #i )
case CA_FINISH_T case CA_FINISH_T
solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #i ) solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #i )
case TA_RESPONSE_T case CA_INIT_T
solve( !Cert( $T, certT, 'terminal' ) ▶₂ #i ) solve( !Cert( $T, certT, 'terminal' ) ▶₂ #i )
case CA_Sign_ltk case CA_Sign_ltk
solve( Completed( kdf(<'KEY', solve( Completed( kdf(<'KEY',
...@@ -2982,17 +3007,20 @@ solve( (¬(#i = #j)) ∥ (¬(sid = sid2)) ) ...@@ -2982,17 +3007,20 @@ solve( (¬(#i = #j)) ∥ (¬(sid = sid2)) )
solve( CAInitT( <$T, iid.1>, id_c.1, solve( CAInitT( <$T, iid.1>, id_c.1,
cert(z, sign(<z, B, 'chip'>, ca_sk), B), r2, <~k, encaps(~k, z)> cert(z, sign(<z, B, 'chip'>, ca_sk), B), r2, <~k, encaps(~k, z)>
) ▶₁ #j ) ) ▶₁ #j )
case TA_RESPONSE_T case CA_INIT_T
by contradiction /* cyclic */ by contradiction /* cyclic */
qed qed
qed qed
qed qed
qed qed
qed
qed
next next
case TA_COMPLETE_C case case_2
solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, B), id_c, r1, r2 solve( Completed( k, sid, A, role, B ) @ #i )
) ▶₁ #i ) case CA_FINISH_C
case TA_CHALLENGE_C solve( CAInitC( <$C, iid>, cert(pk(x), x.1, B), id_c, r1, r2 ) ▶₁ #i )
case CA_INIT_C
solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i )
case Generate_chip_key_pair case Generate_chip_key_pair
solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) solve( !Cert( $C, certC, 'chip' ) ▶₃ #i )
...@@ -3003,25 +3031,16 @@ solve( (¬(#i = #j)) ∥ (¬(sid = sid2)) ) ...@@ -3003,25 +3031,16 @@ solve( (¬(#i = #j)) ∥ (¬(sid = sid2)) )
z), z),
sid2, $C, 'chip', B sid2, $C, 'chip', B
) @ #j ) ) @ #j )
case TA_COMPLETE_C case CA_FINISH_C
solve( TAChallengeC( <$C, iid.1>, by contradiction /* from formulas */
cert(pk(x), sign(<pk(x), B, 'terminal'>, ca_sk), B), id_c.1, r1.1, ~r2
) ▶₁ #j )
case TA_CHALLENGE_C
by contradiction /* cyclic */
qed
qed
qed
qed qed
qed qed
qed qed
qed qed
next next
case case_2
solve( Completed( k, sid, A, role, B ) @ #i )
case CA_FINISH_T case CA_FINISH_T
solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #i ) solve( CAInitT( <$T, iid>, id_c, certC, r2, <k, cip> ) ▶₁ #i )
case TA_RESPONSE_T case CA_INIT_T
solve( !Cert( $T, certT, 'terminal' ) ▶₂ #i ) solve( !Cert( $T, certT, 'terminal' ) ▶₂ #i )
case CA_Sign_ltk case CA_Sign_ltk
solve( Completed( kdf(<'KEY', solve( Completed( kdf(<'KEY',
...@@ -3035,27 +3054,6 @@ next ...@@ -3035,27 +3054,6 @@ next
qed qed
qed qed
qed qed
next
case TA_COMPLETE_C
solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, B), id_c, r1, r2
) ▶₁ #i )
case TA_CHALLENGE_C
solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i )
case Generate_chip_key_pair
solve( !Cert( $C, certC, 'chip' ) ▶₃ #i )
case CA_Sign_ltk
solve( Completed( kdf(<'KEY',
cert(pk(x), sign(<pk(x), B, 'terminal'>, ca_sk), B),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cip>,
z),
sid2, $C, 'chip', B
) @ #j )
case TA_COMPLETE_C
by contradiction /* from formulas */
qed
qed
qed
qed
qed qed
qed qed
...@@ -3075,10 +3073,9 @@ guarded formula characterizing all counter-examples: ...@@ -3075,10 +3073,9 @@ guarded formula characterizing all counter-examples:
*/ */
simplify simplify
solve( Completed( k, sid, C, 'chip', T ) @ #i ) solve( Completed( k, sid, C, 'chip', T ) @ #i )
case TA_COMPLETE_C case CA_FINISH_C
solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 solve( CAInitC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 ) ▶₁ #i )
) ▶₁ #i ) case CA_INIT_C
case TA_CHALLENGE_C
solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i )
case Generate_chip_key_pair case Generate_chip_key_pair
solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) solve( !Cert( $C, certC, 'chip' ) ▶₃ #i )
...@@ -3092,7 +3089,7 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -3092,7 +3089,7 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
solve( CAInitT( <$T, iid.1>, id_c.1, solve( CAInitT( <$T, iid.1>, id_c.1,
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <k, cip> cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <k, cip>
) ▶₁ #j ) ) ▶₁ #j )
case TA_RESPONSE_T case CA_INIT_T
solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T), solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T),
'terminal' 'terminal'
) ▶₂ #j ) ) ▶₂ #j )
...@@ -3102,24 +3099,24 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -3102,24 +3099,24 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
by contradiction /* from formulas */ by contradiction /* from formulas */
next next
case split_case_2 case split_case_2
solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.3 )
case TA_RESPONSE_T
solve( !KU( sign(<'CA', solve( !KU( sign(<'CA',
cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~ltk.1) ~ltk.1)
) @ #vk.5 ) ) @ #vk.3 )
case CA_INIT_T
solve( !KU( sign(<'TA', ~id_c, ~r1>, ~skT) ) @ #vk.11 )
case TA_RESPONSE_T case TA_RESPONSE_T
solve( !KU( kdf(<'CNF', solve( !KU( kdf(<'CNF',
cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~k) ~k)
) @ #vk.14 ) ) @ #vk.16 )
case c_kdf case c_kdf
solve( !KU( ~k ) @ #vk.40 ) solve( !KU( ~k ) @ #vk.40 )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( ~ltk ) @ #vk.42 ) solve( !KU( ~ltk ) @ #vk.42 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
...@@ -3128,18 +3125,18 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -3128,18 +3125,18 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
qed qed
next next
case c_sign case c_sign
solve( !KU( ~ltk.1 ) @ #vk.40 ) solve( !KU( ~skT ) @ #vk.33 )
case Corrupt_ltk case Corrupt_ltk
solve( !KU( kdf(<'CNF', solve( !KU( kdf(<'CNF',
cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~k) ~k)
) @ #vk.19 ) ) @ #vk.17 )
case c_kdf case c_kdf
solve( !KU( ~k ) @ #vk.43 ) solve( !KU( ~k ) @ #vk.42 )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( ~ltk ) @ #vk.45 ) solve( !KU( ~ltk ) @ #vk.44 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
...@@ -3149,25 +3146,20 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -3149,25 +3146,20 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
qed qed
next next
case c_sign case c_sign
solve( !KU( ~ltk.1 ) @ #vk.29 ) solve( !KU( ~ltk.1 ) @ #vk.36 )
case Corrupt_ltk case Corrupt_ltk
solve( !KU( sign(<'CA', solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.14 )
cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>,
~ltk.1)
) @ #vk.6 )
case TA_RESPONSE_T case TA_RESPONSE_T
solve( !KU( kdf(<'CNF', solve( !KU( kdf(<'CNF',
cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~k) ~k)
) @ #vk.15 ) ) @ #vk.21 )
case c_kdf case c_kdf
solve( !KU( ~k ) @ #vk.38 ) solve( !KU( ~k ) @ #vk.43 )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( ~ltk ) @ #vk.40 ) solve( !KU( ~ltk ) @ #vk.45 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
...@@ -3180,11 +3172,11 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -3180,11 +3172,11 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~k) ~k)
) @ #vk.17 ) ) @ #vk.21 )
case c_kdf case c_kdf
solve( !KU( ~k ) @ #vk.40 ) solve( !KU( ~k ) @ #vk.44 )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( ~ltk ) @ #vk.42 ) solve( !KU( ~ltk ) @ #vk.46 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
...@@ -3221,10 +3213,9 @@ guarded formula characterizing all counter-examples: ...@@ -3221,10 +3213,9 @@ guarded formula characterizing all counter-examples:
*/ */
simplify simplify
solve( Completed( k, sid, C, 'chip', T ) @ #i ) solve( Completed( k, sid, C, 'chip', T ) @ #i )
case TA_COMPLETE_C case CA_FINISH_C
solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 solve( CAInitC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 ) ▶₁ #i )
) ▶₁ #i ) case CA_INIT_C
case TA_CHALLENGE_C
solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i )
case Generate_chip_key_pair case Generate_chip_key_pair
solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) solve( !Cert( $C, certC, 'chip' ) ▶₃ #i )
...@@ -3241,32 +3232,32 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -3241,32 +3232,32 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
solve( CAInitT( <$T, iid.1>, id_c.1, solve( CAInitT( <$T, iid.1>, id_c.1,
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <z, cip> cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <z, cip>
) ▶₁ #j ) ) ▶₁ #j )
case TA_RESPONSE_T case CA_INIT_T
solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T), solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T),
'terminal' 'terminal'
) ▶₂ #j ) ) ▶₂ #j )
case CA_Sign_ltk case CA_Sign_ltk
solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.4 )
case TA_RESPONSE_T
solve( !KU( sign(<'CA', solve( !KU( sign(<'CA',
cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~ltk.1) ~ltk.1)
) @ #vk.6 ) ) @ #vk.4 )
case CA_INIT_T
solve( !KU( sign(<'TA', ~id_c, ~r1>, ~skT) ) @ #vk.12 )
case TA_RESPONSE_T case TA_RESPONSE_T
solve( !KU( kdf(<'KEY', solve( !KU( kdf(<'KEY',
cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~k) ~k)
) @ #vk.3 ) ) @ #vk.4 )
case Reveal_session case Reveal_session
by contradiction /* from formulas */ by contradiction /* from formulas */
next next
case c_kdf case c_kdf
solve( !KU( ~k ) @ #vk.41 ) solve( !KU( ~k ) @ #vk.41 )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( ~ltk ) @ #vk.43 ) solve( !KU( ~ltk ) @ #vk.43 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
...@@ -3275,10 +3266,10 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -3275,10 +3266,10 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
qed qed
next next
case c_sign case c_sign
solve( !KU( ~ltk.1 ) @ #vk.41 ) solve( !KU( ~skT ) @ #vk.34 )
case Corrupt_ltk case Corrupt_ltk
solve( !KU( kdf(<'KEY', solve( !KU( kdf(<'KEY',
cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~k) ~k)
...@@ -3287,9 +3278,9 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -3287,9 +3278,9 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
by contradiction /* from formulas */ by contradiction /* from formulas */
next next
case c_kdf case c_kdf
solve( !KU( ~k ) @ #vk.44 ) solve( !KU( ~k ) @ #vk.43 )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( ~ltk ) @ #vk.46 ) solve( !KU( ~ltk ) @ #vk.45 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
...@@ -3299,17 +3290,12 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -3299,17 +3290,12 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
qed qed
next next
case c_sign case c_sign
solve( !KU( ~ltk.1 ) @ #vk.30 ) solve( !KU( ~ltk.1 ) @ #vk.37 )
case Corrupt_ltk case Corrupt_ltk
solve( !KU( sign(<'CA', solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.15 )
cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>,
~ltk.1)
) @ #vk.7 )
case TA_RESPONSE_T case TA_RESPONSE_T
solve( !KU( kdf(<'KEY', solve( !KU( kdf(<'KEY',
cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~k) ~k)
...@@ -3318,9 +3304,9 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -3318,9 +3304,9 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
by contradiction /* from formulas */ by contradiction /* from formulas */
next next
case c_kdf case c_kdf
solve( !KU( ~k ) @ #vk.39 ) solve( !KU( ~k ) @ #vk.44 )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( ~ltk ) @ #vk.41 ) solve( !KU( ~ltk ) @ #vk.46 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
...@@ -3338,9 +3324,9 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -3338,9 +3324,9 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
by contradiction /* from formulas */ by contradiction /* from formulas */
next next
case c_kdf case c_kdf
solve( !KU( ~k ) @ #vk.41 ) solve( !KU( ~k ) @ #vk.45 )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( ~ltk ) @ #vk.43 ) solve( !KU( ~ltk ) @ #vk.47 )
case Corrupt_ltk case Corrupt_ltk
by contradiction /* from formulas */ by contradiction /* from formulas */
qed qed
...@@ -3370,54 +3356,11 @@ guarded formula characterizing all counter-examples: ...@@ -3370,54 +3356,11 @@ guarded formula characterizing all counter-examples:
(∃ #m. (K( iid ) @ #m)) ∧ (∀ #m. (K( iid ) @ #m) ⇒ ¬(#i < #m))" (∃ #m. (K( iid ) @ #m)) ∧ (∀ #m. (K( iid ) @ #m) ⇒ ¬(#i < #m))"
*/ */
simplify simplify
solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1 ) ▶₁ #i )
) ▶₁ #i )
case TA_CHALLENGE_C
solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i )
case Generate_chip_key_pair
solve( !Cert( $C, certC, 'chip' ) ▶₃ #i )
case CA_Sign_ltk
solve( splitEqs(0) )
case split_case_1
solve( !KU( sign(<'TA', ~id_c, ~r1>, x) ) @ #vk.3 )
case TA_RESPONSE_T
solve( !KU( sign(<'CA',
cert(pk(~skT), sign(<pk(~skT), T, 'terminal'>, ca_sk), T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cip>,
~skT)
) @ #vk.5 )
case TA_RESPONSE_T
solve( !KU( cert(z, sign(<z, x, 'chip'>, ca_sk), x) ) @ #vk.19 )
case CA_Sign_ltk
solve( !KU( ~iid ) @ #vk.12 )
case TA_CHALLENGE_C
solve( !KU( ~id_c ) @ #vk.17 )
case TA_CHALLENGE_C
solve( !KU( ~r1 ) @ #vk.19 )
case TA_CHALLENGE_C case TA_CHALLENGE_C
solve( !KU( ~r2 ) @ #vk.32 ) solve( !KU( ~iid ) @ #vk.6 )
case TA_CHALLENGE_C case CA_INIT_C
solve( !KU( cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T) by contradiction /* cyclic */
) @ #vk.19 )
case CA_Sign_ltk
solve( !KU( cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C)
) @ #vk.32 )
case CA_Sign_ltk
solve( !KU( encaps(~k, pk(~ltk)) ) @ #vk.18 )
case TA_RESPONSE_T
SOLVED // trace found
qed
qed
qed
qed
qed
qed
qed
qed
qed
qed
qed
qed
qed qed
qed qed
...@@ -3536,10 +3479,9 @@ guarded formula characterizing all counter-examples: ...@@ -3536,10 +3479,9 @@ guarded formula characterizing all counter-examples:
*/ */
simplify simplify
solve( Completed( k, sid, C, 'chip', T ) @ #i ) solve( Completed( k, sid, C, 'chip', T ) @ #i )
case TA_COMPLETE_C case CA_FINISH_C
solve( TAChallengeC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 solve( CAInitC( <$C, iid>, cert(pk(x), x.1, T), id_c, r1, r2 ) ▶₁ #i )
) ▶₁ #i ) case CA_INIT_C
case TA_CHALLENGE_C
solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i ) solve( !Ltk( $C, ~skC, 'chip' ) ▶₂ #i )
case Generate_chip_key_pair case Generate_chip_key_pair
solve( !Cert( $C, certC, 'chip' ) ▶₃ #i ) solve( !Cert( $C, certC, 'chip' ) ▶₃ #i )
...@@ -3556,55 +3498,62 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -3556,55 +3498,62 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
solve( CAInitT( <$T, iid.1>, id_c.1, solve( CAInitT( <$T, iid.1>, id_c.1,
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <z, cip> cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, <z, cip>
) ▶₁ #j ) ) ▶₁ #j )
case TA_RESPONSE_T case CA_INIT_T
solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T), solve( !Cert( $T, cert(pk(x), sign(<pk(x), $T, 'terminal'>, ca_sk), $T),
'terminal' 'terminal'
) ▶₂ #j ) ) ▶₂ #j )
case CA_Sign_ltk case CA_Sign_ltk
solve( !KU( sign(<'TA', ~id_c, ~r1>, ~ltk.1) ) @ #vk.4 )
case TA_RESPONSE_T
solve( !KU( sign(<'CA', solve( !KU( sign(<'CA',
cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T), cert(pk(~ltk.1), sign(<pk(~ltk.1), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~ltk.1) ~ltk.1)
) @ #vk.6 ) ) @ #vk.4 )
case CA_INIT_T
solve( !KU( sign(<'TA', ~id_c, ~r1>, ~skT) ) @ #vk.12 )
case TA_RESPONSE_T case TA_RESPONSE_T
solve( !KU( kdf(<'KEY', solve( !KU( kdf(<'KEY',
cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T), cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2, cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), ~r2,
encaps(~k, pk(~ltk))>, encaps(~k, pk(~ltk))>,
~k) ~k)
) @ #vk.3 ) ) @ #vk.4 )
case c_kdf case c_kdf
solve( !KU( ~k ) @ #vk.41 ) solve( !KU( ~k ) @ #vk.41 )
case TA_RESPONSE_T case CA_INIT_T
solve( !KU( ~ltk ) @ #vk.43 ) solve( !KU( ~ltk ) @ #vk.43 )
case Corrupt_ltk case Corrupt_ltk
solve( !KU( cert(z, sign(<z, x, 'chip'>, ca_sk), x) ) @ #vk.41 ) solve( !KU( ~r2 ) @ #vk.36 )
case CA_Sign_ltk case CA_INIT_C
solve( !KU( ~r2 ) @ #vk.38 ) solve( !KU( ~id_c ) @ #vk.41 )
case TA_CHALLENGE_C
solve( !KU( ~id_c ) @ #vk.40 )
case TA_CHALLENGE_C case TA_CHALLENGE_C
solve( !KU( ~r1 ) @ #vk.41 ) solve( !KU( ~r1 ) @ #vk.42 )
case TA_CHALLENGE_C case TA_CHALLENGE_C
solve( !KU( cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T) solve( !KU( cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T)
) @ #vk.27 ) ) @ #vk.26 )
case CA_Sign_ltk case CA_Sign_ltk
solve( !KU( kdf(<'CNF', solve( !KU( kdf(<'CNF',
cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), cert(pk(~skT), sign(<pk(~skT), $T, 'terminal'>, ca_sk), $T),
$T),
cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C), cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C),
~r2, encaps(~k, pk(~ltk))>, ~r2, encaps(~k, pk(~ltk))>,
~k) ~k)
) @ #vk.31 ) ) @ #vk.30 )
case TA_COMPLETE_C case CA_FINISH_C
solve( !KU( cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C) solve( !KU( cert(pk(~ltk), sign(<pk(~ltk), $C, 'chip'>, ca_sk), $C)
) @ #vk.40 ) ) @ #vk.38 )
case CA_Sign_ltk case CA_INIT_C
solve( !KU( encaps(~k, pk(~ltk)) ) @ #vk.28 ) solve( !KU( sign(<'TA', ~id_c.2, ~r1.2>, x) ) @ #vk.46 )
case TA_RESPONSE_T case TA_RESPONSE_T
solve( !KU( cert(pk(~skT.2), sign(<pk(~skT.2), z, 'terminal'>, ca_sk),
z)
) @ #vk.48 )
case CA_Sign_ltk
solve( !KU( ~id_c.2 ) @ #vk.50 )
case TA_CHALLENGE_C
solve( !KU( ~r1.1 ) @ #vk.51 )
case TA_CHALLENGE_C
solve( !KU( encaps(~k, pk(~ltk)) ) @ #vk.31 )
case CA_INIT_T
SOLVED // trace found SOLVED // trace found
qed qed
qed qed
...@@ -3626,6 +3575,9 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i ) ...@@ -3626,6 +3575,9 @@ solve( Completed( k, sid, C, 'chip', T ) @ #i )
qed qed
qed qed
qed qed
qed
qed
qed
...@@ -3674,10 +3626,10 @@ summary of summaries: ...@@ -3674,10 +3626,10 @@ summary of summaries:
analyzed: tmp.spthy analyzed: tmp.spthy
processing time: 754.39s processing time: 98.76s
session_exist (exists-trace): verified (19 steps) session_exist (exists-trace): verified (22 steps)
two_session_exist (exists-trace): verified (36 steps) two_session_exist (exists-trace): verified (42 steps)
weak_agreement_C (all-traces): verified (8 steps) weak_agreement_C (all-traces): verified (8 steps)
weak_agreement_T (all-traces): verified (19 steps) weak_agreement_T (all-traces): verified (19 steps)
agreement_C (all-traces): verified (19 steps) agreement_C (all-traces): verified (19 steps)
...@@ -3686,9 +3638,9 @@ analyzed: tmp.spthy ...@@ -3686,9 +3638,9 @@ analyzed: tmp.spthy
session_uniqueness (all-traces): verified (37 steps) session_uniqueness (all-traces): verified (37 steps)
consistency (all-traces): verified (31 steps) consistency (all-traces): verified (31 steps)
key_secrecy (all-traces): verified (33 steps) key_secrecy (all-traces): verified (33 steps)
chip_hiding (all-traces): falsified - found trace (16 steps) chip_hiding (all-traces): verified (4 steps)
nonRepudiation_terminal (exists-trace): verified (13 steps) nonRepudiation_terminal (exists-trace): verified (13 steps)
nonRepudiation_chip (exists-trace): falsified - no trace found (7 steps) nonRepudiation_chip (exists-trace): falsified - no trace found (7 steps)
pfs (all-traces): falsified - found trace (22 steps) pfs (all-traces): falsified - found trace (25 steps)
============================================================================== ==============================================================================
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please to comment