Skip to content

Instantly share code, notes, and snippets.

@keks

keks/halfway.log

Created January 19, 2017 20:17
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save keks/2c416c126e3767dd8503841b1c7ea8f7 to your computer and use it in GitHub Desktop.
Save keks/2c416c126e3767dd8503841b1c7ea8f7 to your computer and use it in GitHub Desktop.
Download ZIP
Output of tamarin-prover on the halfway branch of tamarin-shs
Raw
halfway.log
maude tool: 'maude'
checking version: 2.7. OK.
checking installation: OK.
theory SHS begin
// Function signature and definition of the equational theory E
builtins: diffie-hellman
functions: ed2cv/1, fst/1, h/1, mac/2, macv/3, pair/2, pk/1, sdec/2,
senc/2, sign/2, snd/1, true/0, verify/3
equations:
fst(<x.1, x.2>) = x.1,
macv(mac(m, k), m, k) = true,
sdec(senc(x.1, x.2), x.2) = x.1,
snd(<x.1, x.2>) = x.2,
verify(sign(x.1, x.2), x.1, pk(x.2)) = true
rule (modulo E) Register_pk:
[ Fr( ~ltk ) ] --> [ !Ltk( $A, ~ltk ), !Pk( $A, <'g'^~ltk, pk(~ltk)> ) ]
/* has exactly the trivial AC variant */
rule (modulo E) Get_pk:
[ !Pk( A, pk ) ] --> [ Out( pk ) ]
/* has exactly the trivial AC variant */
rule (modulo E) Reveal_ltk:
[ !Ltk( A, ltk ) ] --[ LtkReveal( A ) ]-> [ Out( ltk ) ]
/* has exactly the trivial AC variant */
rule (modulo E) Client_sendChal:
[ Fr( ~eph ), !Ltk( $A, ltkA ), !Pk( $S, pkS ) ]
-->
[
Client_chalSent( $A, $S, ltkA, ~eph, pkS, $appKey ),
Out( <'g'^~eph, mac('g'^~eph, h($appKey))> )
]
/* has exactly the trivial AC variant */
rule (modulo E) Server_recvChal:
[ Fr( ~eph ), In( <dhA, dhmac> ) ]
--[ True( macv(dhmac, dhA, h($appKey)) ) ]->
[
Server_chalSent( $S, ~eph, dhA, $appKey ),
Out( <'g'^~eph, mac('g'^~eph, h(<dhA^~eph, $appKey>))> )
]
/*
rule (modulo AC) Server_recvChal:
[ Fr( ~eph ), In( <dhA, dhmac> ) ]
--[ True( z.1 ) ]->
[
Server_chalSent( $S, ~eph, dhA, $appKey ),
Out( <'g'^~eph, mac('g'^~eph, h(<z, $appKey>))> )
]
variants (modulo AC)
1. $appKey
= $appKey.15
~eph = ~eph.16
dhA = dhA.17
dhmac = mac(dhA.17, h($appKey.15))
z = dhA.17^~eph.16
z.1 = true
2. $appKey
= $appKey.16
~eph = ~eph.17
dhA = dhA.18
dhmac = dhmac.19
z = dhA.18^~eph.17
z.1 = macv(dhmac.19, dhA.18, h($appKey.16))
3. $appKey
= $appKey.18
~eph = ~eph.19
dhA = z.23^inv(~eph.19)
dhmac = dhmac.21
z = z.23
z.1 = macv(dhmac.21, z.23^inv(~eph.19), h($appKey.18))
4. $appKey
= $appKey.18
~eph = ~eph.19
dhA = z.23^inv(~eph.19)
dhmac = mac(z.23^inv(~eph.19), h($appKey.18))
z = z.23
z.1 = true
5. $appKey
= $appKey.42
~eph = ~eph.43
dhA = x.80^x.81
dhmac = dhmac.45
z = x.80^(~eph.43*x.81)
z.1 = macv(dhmac.45, x.80^x.81, h($appKey.42))
6. $appKey
= $appKey.43
~eph = ~eph.44
dhA = x.82^x.83
dhmac = mac(x.82^x.83, h($appKey.43))
z = x.82^(~eph.44*x.83)
z.1 = true
7. $appKey
= $appKey.43
~eph = ~eph.44
dhA = x.82^inv((~eph.44*x.83))
dhmac = dhmac.46
z = x.82^inv(x.83)
z.1 = macv(dhmac.46, x.82^inv((~eph.44*x.83)), h($appKey.43))
8. $appKey
= $appKey.43
~eph = ~eph.44
dhA = x.82^(x.83*inv(~eph.44))
dhmac = dhmac.46
z = x.82^x.83
z.1 = macv(dhmac.46, x.82^(x.83*inv(~eph.44)), h($appKey.43))
9. $appKey
= $appKey.44
~eph = ~eph.45
dhA = x.83^inv((~eph.45*x.85))
dhmac = mac(x.83^inv((~eph.45*x.85)), h($appKey.44))
z = x.83^inv(x.85)
z.1 = true
10. $appKey
= $appKey.44
~eph = ~eph.45
dhA = x.83^(x.85*inv(~eph.45))
dhmac = mac(x.83^(x.85*inv(~eph.45)), h($appKey.44))
z = x.83^x.85
z.1 = true
11. $appKey
= $appKey.44
~eph = ~eph.45
dhA = x.83^(x.85*inv((~eph.45*x.84)))
dhmac = dhmac.47
z = x.83^(x.85*inv(x.84))
z.1 = macv(dhmac.47, x.83^(x.85*inv((~eph.45*x.84))), h($appKey.44))
12. $appKey
= $appKey.45
~eph = ~eph.46
dhA = x.84^(x.87*inv((~eph.46*x.86)))
dhmac = mac(x.84^(x.87*inv((~eph.46*x.86))), h($appKey.45))
z = x.84^(x.87*inv(x.86))
z.1 = true
*/
rule (modulo E) Client_recvChal:
[ Client_chalSent( A, S, ltkA, eph, pkS, $appKey ), In( <dhS, dhmac> ) ]
--[ True( macv(dhmac, dhS, h(<dhS^eph, $appKey>)) ) ]->
[ Client_authSent( A, S, dhS, eph, pkS, $appKey ) ]
/*
rule (modulo AC) Client_recvChal:
[ Client_chalSent( A, S, ltkA, eph, pkS, $appKey ), In( <dhS, dhmac> ) ]
--[ True( z ) ]->
[ Client_authSent( A, S, dhS, eph, pkS, $appKey ) ]
variants (modulo AC)
1. $appKey
= $appKey.10
dhS = dhS.10
dhmac = dhmac.10
eph = eph.10
z = macv(dhmac.10, dhS.10, h(<dhS.10^eph.10, $appKey.10>))
2. $appKey
= $appKey.10
dhS = dhS.10
dhmac = dhmac.10
eph = one
z = macv(dhmac.10, dhS.10, h(<dhS.10, $appKey.10>))
3. $appKey
= $x.10
dhS = x.11
dhmac = mac(x.11, h(<x.11, $x.10>))
eph = one
z = true
4. $appKey
= $x.10
dhS = x.11
dhmac = mac(x.11, h(<x.11^x.12, $x.10>))
eph = x.12
z = true
5. $appKey
= $x.10
dhS = x.11^x.12
dhmac = mac(x.11^x.12, h(<x.11, $x.10>))
eph = inv(x.12)
z = true
6. $appKey
= $x.10
dhS = x.11^x.12
dhmac = mac(x.11^x.12, h(<x.11^x.13, $x.10>))
eph = (x.13*inv(x.12))
z = true
7. $appKey
= $x.10
dhS = x.11^x.12
dhmac = mac(x.11^x.12, h(<x.11^(x.12*x.13), $x.10>))
eph = x.13
z = true
8. $appKey
= $x.10
dhS = x.11^x.13
dhmac = mac(x.11^x.13, h(<x.11^inv(x.12), $x.10>))
eph = inv((x.12*x.13))
z = true
9. $appKey
= $x.10
dhS = x.11^x.13
dhmac = mac(x.11^x.13, h(<x.11^(x.14*inv(x.12)), $x.10>))
eph = (x.14*inv((x.12*x.13)))
z = true
10. $appKey
= $x.10
dhS = x.11^inv(x.12)
dhmac = mac(x.11^inv(x.12), h(<x.11, $x.10>))
eph = x.12
z = true
11. $appKey
= $x.10
dhS = x.11^inv(x.12)
dhmac = mac(x.11^inv(x.12), h(<x.11^x.13, $x.10>))
eph = (x.12*x.13)
z = true
12. $appKey
= $x.10
dhS = x.11^inv(x.12)
dhmac = mac(x.11^inv(x.12), h(<x.11^inv((x.12*x.13)), $x.10>))
eph = inv(x.13)
z = true
13. $appKey
= $x.10
dhS = x.11^inv(x.12)
dhmac = mac(x.11^inv(x.12), h(<x.11^(x.14*inv((x.12*x.13))), $x.10>))
eph = (x.14*inv(x.13))
z = true
14. $appKey
= $x.10
dhS = x.11^inv((x.12*x.13))
dhmac = mac(x.11^inv((x.12*x.13)), h(<x.11^inv(x.12), $x.10>))
eph = x.13
z = true
15. $appKey
= $x.10
dhS = x.11^inv((x.12*x.13))
dhmac = mac(x.11^inv((x.12*x.13)), h(<x.11^(x.14*inv(x.12)), $x.10>))
eph = (x.13*x.14)
z = true
16. $appKey
= $x.10
dhS = x.11^inv((x.13*x.14))
dhmac = mac(x.11^inv((x.13*x.14)), h(<x.11^inv((x.12*x.13)), $x.10>))
eph = (x.14*inv(x.12))
z = true
17. $appKey
= $x.10
dhS = x.11^inv((x.13*x.14))
dhmac = mac(x.11^inv((x.13*x.14)),
h(<x.11^(x.15*inv((x.12*x.13))), $x.10>))
eph = (x.14*x.15*inv(x.12))
z = true
18. $appKey
= $x.10
dhS = x.11^(x.12*x.13)
dhmac = mac(x.11^(x.12*x.13), h(<x.11^x.13, $x.10>))
eph = inv(x.12)
z = true
19. $appKey
= $x.10
dhS = x.11^(x.12*x.13)
dhmac = mac(x.11^(x.12*x.13), h(<x.11^(x.13*x.14), $x.10>))
eph = (x.14*inv(x.12))
z = true
20. $appKey
= $x.10
dhS = x.11^(x.13*x.14)
dhmac = mac(x.11^(x.13*x.14), h(<x.11^(x.14*x.15*inv(x.12)), $x.10>))
eph = (x.15*inv((x.12*x.13)))
z = true
21. $appKey
= $x.10
dhS = x.11^(x.13*x.14)
dhmac = mac(x.11^(x.13*x.14), h(<x.11^(x.14*inv(x.12)), $x.10>))
eph = inv((x.12*x.13))
z = true
22. $appKey
= $x.10
dhS = x.11^(x.13*x.14*inv(x.12))
dhmac = mac(x.11^(x.13*x.14*inv(x.12)), h(<x.11^x.14, $x.10>))
eph = (x.12*inv(x.13))
z = true
23. $appKey
= $x.10
dhS = x.11^(x.13*x.14*inv(x.12))
dhmac = mac(x.11^(x.13*x.14*inv(x.12)), h(<x.11^(x.14*x.15), $x.10>))
eph = (x.12*x.15*inv(x.13))
z = true
24. $appKey
= $x.10
dhS = x.11^(x.13*x.15*inv((x.12*x.14)))
dhmac = mac(x.11^(x.13*x.15*inv((x.12*x.14))),
h(<x.11^(x.15*x.16*inv(x.12)), $x.10>))
eph = (x.14*x.16*inv(x.13))
z = true
25. $appKey
= $x.10
dhS = x.11^(x.13*x.15*inv((x.12*x.14)))
dhmac = mac(x.11^(x.13*x.15*inv((x.12*x.14))),
h(<x.11^(x.15*inv(x.12)), $x.10>))
eph = (x.14*inv(x.13))
z = true
26. $appKey
= $x.10
dhS = x.11^(x.13*inv(x.12))
dhmac = mac(x.11^(x.13*inv(x.12)), h(<x.11, $x.10>))
eph = (x.12*inv(x.13))
z = true
27. $appKey
= $x.10
dhS = x.11^(x.13*inv(x.12))
dhmac = mac(x.11^(x.13*inv(x.12)), h(<x.11^x.13, $x.10>))
eph = x.12
z = true
28. $appKey
= $x.10
dhS = x.11^(x.13*inv(x.12))
dhmac = mac(x.11^(x.13*inv(x.12)), h(<x.11^x.14, $x.10>))
eph = (x.12*x.14*inv(x.13))
z = true
29. $appKey
= $x.10
dhS = x.11^(x.13*inv(x.12))
dhmac = mac(x.11^(x.13*inv(x.12)), h(<x.11^(x.13*x.14), $x.10>))
eph = (x.12*x.14)
z = true
30. $appKey
= $x.10
dhS = x.11^(x.13*inv((x.12*x.14)))
dhmac = mac(x.11^(x.13*inv((x.12*x.14))), h(<x.11^inv(x.12), $x.10>))
eph = (x.14*inv(x.13))
z = true
31. $appKey
= $x.10
dhS = x.11^(x.13*inv((x.12*x.14)))
dhmac = mac(x.11^(x.13*inv((x.12*x.14))),
h(<x.11^(x.15*inv(x.12)), $x.10>))
eph = (x.14*x.15*inv(x.13))
z = true
32. $appKey
= $x.10
dhS = x.11^(x.14*x.15*inv(x.12))
dhmac = mac(x.11^(x.14*x.15*inv(x.12)),
h(<x.11^(x.15*x.16*inv(x.13)), $x.10>))
eph = (x.12*x.16*inv((x.13*x.14)))
z = true
33. $appKey
= $x.10
dhS = x.11^(x.14*x.15*inv(x.12))
dhmac = mac(x.11^(x.14*x.15*inv(x.12)),
h(<x.11^(x.15*x.16*inv((x.12*x.13))), $x.10>))
eph = (x.16*inv((x.13*x.14)))
z = true
34. $appKey
= $x.10
dhS = x.11^(x.14*x.15*inv(x.12))
dhmac = mac(x.11^(x.14*x.15*inv(x.12)),
h(<x.11^(x.15*inv(x.13)), $x.10>))
eph = (x.12*inv((x.13*x.14)))
z = true
35. $appKey
= $x.10
dhS = x.11^(x.14*x.15*inv(x.12))
dhmac = mac(x.11^(x.14*x.15*inv(x.12)),
h(<x.11^(x.15*inv((x.12*x.13))), $x.10>))
eph = inv((x.13*x.14))
z = true
36. $appKey
= $x.10
dhS = x.11^(x.14*inv(x.12))
dhmac = mac(x.11^(x.14*inv(x.12)), h(<x.11^inv((x.12*x.13)), $x.10>))
eph = inv((x.13*x.14))
z = true
37. $appKey
= $x.10
dhS = x.11^(x.14*inv(x.12))
dhmac = mac(x.11^(x.14*inv(x.12)),
h(<x.11^(x.14*x.15*inv((x.12*x.13))), $x.10>))
eph = (x.15*inv(x.13))
z = true
38. $appKey
= $x.10
dhS = x.11^(x.14*inv(x.12))
dhmac = mac(x.11^(x.14*inv(x.12)), h(<x.11^(x.15*inv(x.13)), $x.10>))
eph = (x.12*x.15*inv((x.13*x.14)))
z = true
39. $appKey
= $x.10
dhS = x.11^(x.14*inv(x.12))
dhmac = mac(x.11^(x.14*inv(x.12)),
h(<x.11^(x.15*inv((x.12*x.13))), $x.10>))
eph = (x.15*inv((x.13*x.14)))
z = true
40. $appKey
= $x.10
dhS = x.11^(x.14*inv(x.13))
dhmac = mac(x.11^(x.14*inv(x.13)), h(<x.11^inv(x.12), $x.10>))
eph = (x.13*inv((x.12*x.14)))
z = true
41. $appKey
= $x.10
dhS = x.11^(x.14*inv(x.13))
dhmac = mac(x.11^(x.14*inv(x.13)),
h(<x.11^(x.14*inv((x.12*x.13))), $x.10>))
eph = inv(x.12)
z = true
42. $appKey
= $x.10
dhS = x.11^(x.14*inv((x.12*x.13)))
dhmac = mac(x.11^(x.14*inv((x.12*x.13))),
h(<x.11^(x.14*x.15*inv(x.12)), $x.10>))
eph = (x.13*x.15)
z = true
43. $appKey
= $x.10
dhS = x.11^(x.14*inv((x.12*x.13)))
dhmac = mac(x.11^(x.14*inv((x.12*x.13))),
h(<x.11^(x.14*inv(x.12)), $x.10>))
eph = x.13
z = true
44. $appKey
= $x.10
dhS = x.11^(x.15*x.16*inv((x.12*x.13)))
dhmac = mac(x.11^(x.15*x.16*inv((x.12*x.13))),
h(<x.11^(x.16*x.17*inv((x.12*x.14))), $x.10>))
eph = (x.13*x.17*inv((x.14*x.15)))
z = true
45. $appKey
= $x.10
dhS = x.11^(x.15*x.16*inv((x.12*x.13)))
dhmac = mac(x.11^(x.15*x.16*inv((x.12*x.13))),
h(<x.11^(x.16*inv((x.12*x.14))), $x.10>))
eph = (x.13*inv((x.14*x.15)))
z = true
46. $appKey
= $x.10
dhS = x.11^(x.15*inv((x.12*x.13)))
dhmac = mac(x.11^(x.15*inv((x.12*x.13))),
h(<x.11^(x.16*inv((x.12*x.14))), $x.10>))
eph = (x.13*x.16*inv((x.14*x.15)))
z = true
47. $appKey
= $x.10
dhS = x.11^(x.15*inv((x.12*x.14)))
dhmac = mac(x.11^(x.15*inv((x.12*x.14))),
h(<x.11^inv((x.12*x.13)), $x.10>))
eph = (x.14*inv((x.13*x.15)))
z = true
48. $appKey
= $x.10
dhS = x.11^(x.15*inv((x.13*x.14)))
dhmac = mac(x.11^(x.15*inv((x.13*x.14))),
h(<x.11^(x.15*x.16*inv((x.12*x.13))), $x.10>))
eph = (x.14*x.16*inv(x.12))
z = true
49. $appKey
= $x.10
dhS = x.11^(x.15*inv((x.13*x.14)))
dhmac = mac(x.11^(x.15*inv((x.13*x.14))),
h(<x.11^(x.15*inv((x.12*x.13))), $x.10>))
eph = (x.14*inv(x.12))
z = true
50. $appKey
= $appKey.12
dhS = x.10^x.11
dhmac = dhmac.12
eph = eph.12
z = macv(dhmac.12, x.10^x.11, h(<x.10^(x.11*eph.12), $appKey.12>))
51. $appKey
= $appKey.12
dhS = x.10^x.11
dhmac = dhmac.12
eph = inv(x.11)
z = macv(dhmac.12, x.10^x.11, h(<x.10, $appKey.12>))
52. $appKey
= $appKey.12
dhS = x.10^inv(x.11)
dhmac = dhmac.12
eph = x.11
z = macv(dhmac.12, x.10^inv(x.11), h(<x.10, $appKey.12>))
53. $appKey
= $appKey.13
dhS = x.10^x.11
dhmac = dhmac.13
eph = inv((x.11*x.12))
z = macv(dhmac.13, x.10^x.11, h(<x.10^inv(x.12), $appKey.13>))
54. $appKey
= $appKey.13
dhS = x.10^x.11
dhmac = dhmac.13
eph = (x.12*inv(x.11))
z = macv(dhmac.13, x.10^x.11, h(<x.10^x.12, $appKey.13>))
55. $appKey
= $appKey.13
dhS = x.10^inv(x.11)
dhmac = dhmac.13
eph = (x.11*x.12)
z = macv(dhmac.13, x.10^inv(x.11), h(<x.10^x.12, $appKey.13>))
56. $appKey
= $appKey.13
dhS = x.10^inv(x.12)
dhmac = dhmac.13
eph = inv(x.11)
z = macv(dhmac.13, x.10^inv(x.12),
h(<x.10^inv((x.11*x.12)), $appKey.13>))
57. $appKey
= $appKey.13
dhS = x.10^inv((x.11*x.12))
dhmac = dhmac.13
eph = x.11
z = macv(dhmac.13, x.10^inv((x.11*x.12)),
h(<x.10^inv(x.12), $appKey.13>))
58. $appKey
= $appKey.13
dhS = x.10^(x.11*x.12)
dhmac = dhmac.13
eph = inv(x.11)
z = macv(dhmac.13, x.10^(x.11*x.12), h(<x.10^x.12, $appKey.13>))
59. $appKey
= $appKey.13
dhS = x.10^(x.11*inv(x.12))
dhmac = dhmac.13
eph = (x.12*inv(x.11))
z = macv(dhmac.13, x.10^(x.11*inv(x.12)), h(<x.10, $appKey.13>))
60. $appKey
= $appKey.13
dhS = x.10^(x.12*inv(x.11))
dhmac = dhmac.13
eph = x.11
z = macv(dhmac.13, x.10^(x.12*inv(x.11)), h(<x.10^x.12, $appKey.13>))
61. $appKey
= $appKey.14
dhS = x.10^x.11
dhmac = dhmac.14
eph = (x.13*inv((x.11*x.12)))
z = macv(dhmac.14, x.10^x.11, h(<x.10^(x.13*inv(x.12)), $appKey.14>))
62. $appKey
= $appKey.14
dhS = x.10^inv(x.11)
dhmac = dhmac.14
eph = (x.13*inv(x.12))
z = macv(dhmac.14, x.10^inv(x.11),
h(<x.10^(x.13*inv((x.11*x.12))), $appKey.14>))
63. $appKey
= $appKey.14
dhS = x.10^inv((x.11*x.12))
dhmac = dhmac.14
eph = (x.12*x.13)
z = macv(dhmac.14, x.10^inv((x.11*x.12)),
h(<x.10^(x.13*inv(x.11)), $appKey.14>))
64. $appKey
= $appKey.14
dhS = x.10^inv((x.12*x.13))
dhmac = dhmac.14
eph = (x.13*inv(x.11))
z = macv(dhmac.14, x.10^inv((x.12*x.13)),
h(<x.10^inv((x.11*x.12)), $appKey.14>))
65. $appKey
= $appKey.14
dhS = x.10^(x.11*x.13)
dhmac = dhmac.14
eph = (x.12*inv(x.11))
z = macv(dhmac.14, x.10^(x.11*x.13),
h(<x.10^(x.12*x.13), $appKey.14>))
66. $appKey
= $appKey.14
dhS = x.10^(x.11*x.13*inv(x.12))
dhmac = dhmac.14
eph = (x.12*inv(x.11))
z = macv(dhmac.14, x.10^(x.11*x.13*inv(x.12)),
h(<x.10^x.13, $appKey.14>))
67. $appKey
= $appKey.14
dhS = x.10^(x.11*inv(x.12))
dhmac = dhmac.14
eph = (x.12*x.13*inv(x.11))
z = macv(dhmac.14, x.10^(x.11*inv(x.12)), h(<x.10^x.13, $appKey.14>))
68. $appKey
= $appKey.14
dhS = x.10^(x.11*inv((x.12*x.13)))
dhmac = dhmac.14
eph = (x.13*inv(x.11))
z = macv(dhmac.14, x.10^(x.11*inv((x.12*x.13))),
h(<x.10^inv(x.12), $appKey.14>))
69. $appKey
= $appKey.14
dhS = x.10^(x.12*x.13)
dhmac = dhmac.14
eph = inv((x.11*x.12))
z = macv(dhmac.14, x.10^(x.12*x.13),
h(<x.10^(x.13*inv(x.11)), $appKey.14>))
70. $appKey
= $appKey.14
dhS = x.10^(x.13*inv(x.11))
dhmac = dhmac.14
eph = inv((x.12*x.13))
z = macv(dhmac.14, x.10^(x.13*inv(x.11)),
h(<x.10^inv((x.11*x.12)), $appKey.14>))
71. $appKey
= $appKey.14
dhS = x.10^(x.13*inv(x.11))
dhmac = dhmac.14
eph = (x.11*x.12)
z = macv(dhmac.14, x.10^(x.13*inv(x.11)),
h(<x.10^(x.12*x.13), $appKey.14>))
72. $appKey
= $appKey.14
dhS = x.10^(x.13*inv(x.11))
dhmac = dhmac.14
eph = (x.11*inv((x.12*x.13)))
z = macv(dhmac.14, x.10^(x.13*inv(x.11)),
h(<x.10^inv(x.12), $appKey.14>))
73. $appKey
= $appKey.14
dhS = x.10^(x.13*inv(x.12))
dhmac = dhmac.14
eph = inv(x.11)
z = macv(dhmac.14, x.10^(x.13*inv(x.12)),
h(<x.10^(x.13*inv((x.11*x.12))), $appKey.14>))
74. $appKey
= $appKey.14
dhS = x.10^(x.13*inv((x.11*x.12)))
dhmac = dhmac.14
eph = x.11
z = macv(dhmac.14, x.10^(x.13*inv((x.11*x.12))),
h(<x.10^(x.13*inv(x.12)), $appKey.14>))
75. $appKey
= $appKey.15
dhS = x.10^inv((x.12*x.13))
dhmac = dhmac.15
eph = (x.13*x.14*inv(x.11))
z = macv(dhmac.15, x.10^inv((x.12*x.13)),
h(<x.10^(x.14*inv((x.11*x.12))), $appKey.15>))
76. $appKey
= $appKey.15
dhS = x.10^(x.11*x.14*inv(x.12))
dhmac = dhmac.15
eph = (x.12*x.13*inv(x.11))
z = macv(dhmac.15, x.10^(x.11*x.14*inv(x.12)),
h(<x.10^(x.13*x.14), $appKey.15>))
77. $appKey
= $appKey.15
dhS = x.10^(x.11*x.14*inv((x.12*x.13)))
dhmac = dhmac.15
eph = (x.13*inv(x.11))
z = macv(dhmac.15, x.10^(x.11*x.14*inv((x.12*x.13))),
h(<x.10^(x.14*inv(x.12)), $appKey.15>))
78. $appKey
= $appKey.15
dhS = x.10^(x.11*inv((x.12*x.13)))
dhmac = dhmac.15
eph = (x.13*x.14*inv(x.11))
z = macv(dhmac.15, x.10^(x.11*inv((x.12*x.13))),
h(<x.10^(x.14*inv(x.12)), $appKey.15>))
79. $appKey
= $appKey.15
dhS = x.10^(x.12*x.14)
dhmac = dhmac.15
eph = (x.13*inv((x.11*x.12)))
z = macv(dhmac.15, x.10^(x.12*x.14),
h(<x.10^(x.13*x.14*inv(x.11)), $appKey.15>))
80. $appKey
= $appKey.15
dhS = x.10^(x.12*inv((x.13*x.14)))
dhmac = dhmac.15
eph = (x.14*inv((x.11*x.12)))
z = macv(dhmac.15, x.10^(x.12*inv((x.13*x.14))),
h(<x.10^inv((x.11*x.13)), $appKey.15>))
81. $appKey
= $appKey.15
dhS = x.10^(x.13*x.14*inv(x.11))
dhmac = dhmac.15
eph = inv((x.12*x.13))
z = macv(dhmac.15, x.10^(x.13*x.14*inv(x.11)),
h(<x.10^(x.14*inv((x.11*x.12))), $appKey.15>))
82. $appKey
= $appKey.15
dhS = x.10^(x.13*x.14*inv(x.11))
dhmac = dhmac.15
eph = (x.11*inv((x.12*x.13)))
z = macv(dhmac.15, x.10^(x.13*x.14*inv(x.11)),
h(<x.10^(x.14*inv(x.12)), $appKey.15>))
83. $appKey
= $appKey.15
dhS = x.10^(x.13*inv(x.11))
dhmac = dhmac.15
eph = (x.11*x.14*inv((x.12*x.13)))
z = macv(dhmac.15, x.10^(x.13*inv(x.11)),
h(<x.10^(x.14*inv(x.12)), $appKey.15>))
84. $appKey
= $appKey.15
dhS = x.10^(x.13*inv(x.11))
dhmac = dhmac.15
eph = (x.14*inv((x.12*x.13)))
z = macv(dhmac.15, x.10^(x.13*inv(x.11)),
h(<x.10^(x.14*inv((x.11*x.12))), $appKey.15>))
85. $appKey
= $appKey.15
dhS = x.10^(x.14*inv(x.12))
dhmac = dhmac.15
eph = (x.13*inv(x.11))
z = macv(dhmac.15, x.10^(x.14*inv(x.12)),
h(<x.10^(x.13*x.14*inv((x.11*x.12))), $appKey.15>))
86. $appKey
= $appKey.15
dhS = x.10^(x.14*inv((x.11*x.12)))
dhmac = dhmac.15
eph = (x.12*x.13)
z = macv(dhmac.15, x.10^(x.14*inv((x.11*x.12))),
h(<x.10^(x.13*x.14*inv(x.11)), $appKey.15>))
87. $appKey
= $appKey.15
dhS = x.10^(x.14*inv((x.12*x.13)))
dhmac = dhmac.15
eph = (x.13*inv(x.11))
z = macv(dhmac.15, x.10^(x.14*inv((x.12*x.13))),
h(<x.10^(x.14*inv((x.11*x.12))), $appKey.15>))
88. $appKey
= $appKey.16
dhS = x.10^(x.11*x.15*inv((x.12*x.13)))
dhmac = dhmac.16
eph = (x.13*x.14*inv(x.11))
z = macv(dhmac.16, x.10^(x.11*x.15*inv((x.12*x.13))),
h(<x.10^(x.14*x.15*inv(x.12)), $appKey.16>))
89. $appKey
= $appKey.16
dhS = x.10^(x.12*x.15*inv((x.13*x.14)))
dhmac = dhmac.16
eph = (x.14*inv((x.11*x.12)))
z = macv(dhmac.16, x.10^(x.12*x.15*inv((x.13*x.14))),
h(<x.10^(x.15*inv((x.11*x.13))), $appKey.16>))
90. $appKey
= $appKey.16
dhS = x.10^(x.12*inv((x.13*x.14)))
dhmac = dhmac.16
eph = (x.14*x.15*inv((x.11*x.12)))
z = macv(dhmac.16, x.10^(x.12*inv((x.13*x.14))),
h(<x.10^(x.15*inv((x.11*x.13))), $appKey.16>))
91. $appKey
= $appKey.16
dhS = x.10^(x.13*x.15*inv(x.11))
dhmac = dhmac.16
eph = (x.11*x.14*inv((x.12*x.13)))
z = macv(dhmac.16, x.10^(x.13*x.15*inv(x.11)),
h(<x.10^(x.14*x.15*inv(x.12)), $appKey.16>))
92. $appKey
= $appKey.16
dhS = x.10^(x.13*x.15*inv(x.11))
dhmac = dhmac.16
eph = (x.14*inv((x.12*x.13)))
z = macv(dhmac.16, x.10^(x.13*x.15*inv(x.11)),
h(<x.10^(x.14*x.15*inv((x.11*x.12))), $appKey.16>))
93. $appKey
= $appKey.16
dhS = x.10^(x.15*inv((x.12*x.13)))
dhmac = dhmac.16
eph = (x.13*x.14*inv(x.11))
z = macv(dhmac.16, x.10^(x.15*inv((x.12*x.13))),
h(<x.10^(x.14*x.15*inv((x.11*x.12))), $appKey.16>))
94. $appKey
= $appKey.17
dhS = x.10^(x.12*x.16*inv((x.13*x.14)))
dhmac = dhmac.17
eph = (x.14*x.15*inv((x.11*x.12)))
z = macv(dhmac.17, x.10^(x.12*x.16*inv((x.13*x.14))),
h(<x.10^(x.15*x.16*inv((x.11*x.13))), $appKey.17>))
*/
axiom Eq:
"∀ x y #i. (Eq( x, y ) @ #i) ⇒ (x = y)"
// safety formula
axiom IsTrue:
"∀ x #i. (True( x ) @ #i) ⇒ (x = true)"
// safety formula
lemma Client_auth:
all-traces
"∀ S k #i.
(SessKeyI( S, k ) @ #i) ⇒
((∃ #a. SessKeyR( S, k ) @ #a) ∨
(∃ #r. (LtkReveal( S ) @ #r) ∧ (#r < #i)))"
/*
guarded formula characterizing all counter-examples:
"∃ S k #i.
(SessKeyI( S, k ) @ #i)
∧
(∀ #a. (SessKeyR( S, k ) @ #a) ⇒ ⊥) ∧
(∀ #r. (LtkReveal( S ) @ #r) ⇒ ¬(#r < #i))"
*/
by sorry
/*
WARNING: the following wellformedness checks failed!
lemma actions:
lemma `Client_auth' references action
(ProtoFact Linear "SessKeyI" 2,2,Linear)
but no rule has such an action.
lemma `Client_auth' references action
(ProtoFact Linear "SessKeyR" 2,2,Linear)
but no rule has such an action.
*/
end
==============================================================================
summary of summaries:
analyzed: shs.spthy
WARNING: 2 wellformedness check failed!
The analysis results might be wrong!
Client_auth (all-traces): analysis incomplete (1 steps)
==============================================================================
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment