Skip to content

Instantly share code, notes, and snippets.

@keks

keks/halfway2.log

Created January 20, 2017 12:32
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save keks/ac627ac063a46c439da77f7e54731ff1 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save keks/ac627ac063a46c439da77f7e54731ff1 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
halfway2.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( <'g'^X, dhmac> ) ]
--[ True( macv(dhmac, 'g'^X, h($appKey)) ) ]->
[
Server_chalSent( $S, ~eph, 'g'^X, $appKey ),
Out( <'g'^~eph, mac('g'^~eph, h(<'g'^X^~eph, $appKey>))> )
]
/*
rule (modulo AC) Server_recvChal:
[ Fr( ~eph ), In( <z, dhmac> ) ]
--[ True( z.2 ) ]->
[
Server_chalSent( $S, ~eph, z, $appKey ),
Out( <'g'^~eph, mac('g'^~eph, h(<z.1, $appKey>))> )
]
variants (modulo AC)
1. $appKey
= $appKey.15
~eph = ~eph.16
dhmac = mac('g', h($appKey.15))
z = 'g'
z.1 = 'g'^~eph.16
z.2 = true
2. $appKey
= $appKey.15
~eph = ~eph.16
dhmac = mac('g'^inv(~eph.16), h($appKey.15))
z = 'g'^inv(~eph.16)
z.1 = 'g'
z.2 = true
3. $appKey
= $appKey.17
~eph = ~eph.18
dhmac = dhmac.20
z = 'g'
z.1 = 'g'^~eph.18
z.2 = macv(dhmac.20, 'g', h($appKey.17))
4. $appKey
= $appKey.17
~eph = ~eph.18
dhmac = dhmac.20
z = 'g'^inv(~eph.18)
z.1 = 'g'
z.2 = macv(dhmac.20, 'g'^inv(~eph.18), h($appKey.17))
5. $appKey
= $appKey.45
~eph = ~eph.46
dhmac = dhmac.48
z = 'g'^X.87
z.1 = 'g'^(~eph.46*X.87)
z.2 = macv(dhmac.48, 'g'^X.87, h($appKey.45))
6. $appKey
= $appKey.46
~eph = ~eph.47
dhmac = dhmac.49
z = 'g'^inv((~eph.47*x.89))
z.1 = 'g'^inv(x.89)
z.2 = macv(dhmac.49, 'g'^inv((~eph.47*x.89)), h($appKey.46))
7. $appKey
= $appKey.46
~eph = ~eph.47
dhmac = dhmac.49
z = 'g'^(x.89*inv(~eph.47))
z.1 = 'g'^x.89
z.2 = macv(dhmac.49, 'g'^(x.89*inv(~eph.47)), h($appKey.46))
8. $appKey
= $appKey.46
~eph = ~eph.47
dhmac = mac('g'^x.89, h($appKey.46))
z = 'g'^x.89
z.1 = 'g'^(~eph.47*x.89)
z.2 = true
9. $appKey
= $appKey.47
~eph = ~eph.48
dhmac = dhmac.50
z = 'g'^(x.91*inv((~eph.48*x.90)))
z.1 = 'g'^(x.91*inv(x.90))
z.2 = macv(dhmac.50, 'g'^(x.91*inv((~eph.48*x.90))), h($appKey.47))
10. $appKey
= $appKey.47
~eph = ~eph.48
dhmac = mac('g'^inv((~eph.48*x.91)), h($appKey.47))
z = 'g'^inv((~eph.48*x.91))
z.1 = 'g'^inv(x.91)
z.2 = true
11. $appKey
= $appKey.47
~eph = ~eph.48
dhmac = mac('g'^(x.91*inv(~eph.48)), h($appKey.47))
z = 'g'^(x.91*inv(~eph.48))
z.1 = 'g'^x.91
z.2 = true
12. $appKey
= $appKey.48
~eph = ~eph.49
dhmac = mac('g'^(x.93*inv((~eph.49*x.92))), h($appKey.48))
z = 'g'^(x.93*inv((~eph.49*x.92)))
z.1 = 'g'^(x.93*inv(x.92))
z.2 = true
*/
rule (modulo E) Client_recvChal:
[
Client_chalSent( A, S, ltkA, eph, <pkSdh, pkSpk>, $appKey ),
In( <'g'^X, dhmac> )
]
--[ True( macv(dhmac, 'g'^X, h(<'g'^X^eph, $appKey>)) ), Reach( ) ]->
[ Client_authSent( A, S, 'g'^X, eph, <pkSdh, pkSpk>, $appKey ) ]
/*
rule (modulo AC) Client_recvChal:
[
Client_chalSent( A, S, ltkA, eph, <pkSdh, pkSpk>, $appKey ),
In( <z, dhmac> )
]
--[ True( z.1 ), Reach( ) ]->
[ Client_authSent( A, S, z, eph, <pkSdh, pkSpk>, $appKey ) ]
variants (modulo AC)
1. $appKey
= $appKey.12
dhmac = dhmac.12
eph = eph.12
z = 'g'
z.1 = macv(dhmac.12, 'g', h(<'g'^eph.12, $appKey.12>))
2. $appKey
= $appKey.12
dhmac = dhmac.12
eph = eph.12
z = 'g'^X.12
z.1 = macv(dhmac.12, 'g'^X.12, h(<'g'^(X.12*eph.12), $appKey.12>))
3. $appKey
= $appKey.12
dhmac = dhmac.12
eph = one
z = 'g'
z.1 = macv(dhmac.12, 'g', h(<'g', $appKey.12>))
4. $appKey
= $appKey.12
dhmac = dhmac.12
eph = one
z = 'g'^X.12
z.1 = macv(dhmac.12, 'g'^X.12, h(<'g'^X.12, $appKey.12>))
5. $appKey
= $x.12
dhmac = mac('g', h(<'g', $x.12>))
eph = one
z = 'g'
z.1 = true
6. $appKey
= $x.12
dhmac = mac('g', h(<'g'^x.13, $x.12>))
eph = x.13
z = 'g'
z.1 = true
7. $appKey
= $x.12
dhmac = mac('g'^x.13, h(<'g', $x.12>))
eph = inv(x.13)
z = 'g'^x.13
z.1 = true
8. $appKey
= $x.12
dhmac = mac('g'^x.13, h(<'g'^x.13, $x.12>))
eph = one
z = 'g'^x.13
z.1 = true
9. $appKey
= $x.12
dhmac = mac('g'^x.13, h(<'g'^x.14, $x.12>))
eph = (x.14*inv(x.13))
z = 'g'^x.13
z.1 = true
10. $appKey
= $x.12
dhmac = mac('g'^x.13, h(<'g'^(x.13*x.14), $x.12>))
eph = x.14
z = 'g'^x.13
z.1 = true
11. $appKey
= $x.12
dhmac = mac('g'^x.14, h(<'g'^inv(x.13), $x.12>))
eph = inv((x.13*x.14))
z = 'g'^x.14
z.1 = true
12. $appKey
= $x.12
dhmac = mac('g'^x.14, h(<'g'^(x.15*inv(x.13)), $x.12>))
eph = (x.15*inv((x.13*x.14)))
z = 'g'^x.14
z.1 = true
13. $appKey
= $x.12
dhmac = mac('g'^inv(x.13), h(<'g', $x.12>))
eph = x.13
z = 'g'^inv(x.13)
z.1 = true
14. $appKey
= $x.12
dhmac = mac('g'^inv(x.13), h(<'g'^x.14, $x.12>))
eph = (x.13*x.14)
z = 'g'^inv(x.13)
z.1 = true
15. $appKey
= $x.12
dhmac = mac('g'^inv(x.13), h(<'g'^inv((x.13*x.14)), $x.12>))
eph = inv(x.14)
z = 'g'^inv(x.13)
z.1 = true
16. $appKey
= $x.12
dhmac = mac('g'^inv(x.13), h(<'g'^(x.15*inv((x.13*x.14))), $x.12>))
eph = (x.15*inv(x.14))
z = 'g'^inv(x.13)
z.1 = true
17. $appKey
= $x.12
dhmac = mac('g'^inv((x.13*x.14)), h(<'g'^inv(x.13), $x.12>))
eph = x.14
z = 'g'^inv((x.13*x.14))
z.1 = true
18. $appKey
= $x.12
dhmac = mac('g'^inv((x.13*x.14)), h(<'g'^(x.15*inv(x.13)), $x.12>))
eph = (x.14*x.15)
z = 'g'^inv((x.13*x.14))
z.1 = true
19. $appKey
= $x.12
dhmac = mac('g'^inv((x.14*x.15)), h(<'g'^inv((x.13*x.14)), $x.12>))
eph = (x.15*inv(x.13))
z = 'g'^inv((x.14*x.15))
z.1 = true
20. $appKey
= $x.12
dhmac = mac('g'^inv((x.14*x.15)),
h(<'g'^(x.16*inv((x.13*x.14))), $x.12>))
eph = (x.15*x.16*inv(x.13))
z = 'g'^inv((x.14*x.15))
z.1 = true
21. $appKey
= $x.12
dhmac = mac('g'^(x.13*x.14), h(<'g'^x.14, $x.12>))
eph = inv(x.13)
z = 'g'^(x.13*x.14)
z.1 = true
22. $appKey
= $x.12
dhmac = mac('g'^(x.13*x.14), h(<'g'^(x.14*x.15), $x.12>))
eph = (x.15*inv(x.13))
z = 'g'^(x.13*x.14)
z.1 = true
23. $appKey
= $x.12
dhmac = mac('g'^(x.14*x.15), h(<'g'^(x.15*x.16*inv(x.13)), $x.12>))
eph = (x.16*inv((x.13*x.14)))
z = 'g'^(x.14*x.15)
z.1 = true
24. $appKey
= $x.12
dhmac = mac('g'^(x.14*x.15), h(<'g'^(x.15*inv(x.13)), $x.12>))
eph = inv((x.13*x.14))
z = 'g'^(x.14*x.15)
z.1 = true
25. $appKey
= $x.12
dhmac = mac('g'^(x.14*x.15*inv(x.13)), h(<'g'^x.15, $x.12>))
eph = (x.13*inv(x.14))
z = 'g'^(x.14*x.15*inv(x.13))
z.1 = true
26. $appKey
= $x.12
dhmac = mac('g'^(x.14*x.15*inv(x.13)), h(<'g'^(x.15*x.16), $x.12>))
eph = (x.13*x.16*inv(x.14))
z = 'g'^(x.14*x.15*inv(x.13))
z.1 = true
27. $appKey
= $x.12
dhmac = mac('g'^(x.14*x.16*inv((x.13*x.15))),
h(<'g'^(x.16*x.17*inv(x.13)), $x.12>))
eph = (x.15*x.17*inv(x.14))
z = 'g'^(x.14*x.16*inv((x.13*x.15)))
z.1 = true
28. $appKey
= $x.12
dhmac = mac('g'^(x.14*x.16*inv((x.13*x.15))),
h(<'g'^(x.16*inv(x.13)), $x.12>))
eph = (x.15*inv(x.14))
z = 'g'^(x.14*x.16*inv((x.13*x.15)))
z.1 = true
29. $appKey
= $x.12
dhmac = mac('g'^(x.14*inv(x.13)), h(<'g', $x.12>))
eph = (x.13*inv(x.14))
z = 'g'^(x.14*inv(x.13))
z.1 = true
30. $appKey
= $x.12
dhmac = mac('g'^(x.14*inv(x.13)), h(<'g'^x.14, $x.12>))
eph = x.13
z = 'g'^(x.14*inv(x.13))
z.1 = true
31. $appKey
= $x.12
dhmac = mac('g'^(x.14*inv(x.13)), h(<'g'^x.15, $x.12>))
eph = (x.13*x.15*inv(x.14))
z = 'g'^(x.14*inv(x.13))
z.1 = true
32. $appKey
= $x.12
dhmac = mac('g'^(x.14*inv(x.13)), h(<'g'^(x.14*x.15), $x.12>))
eph = (x.13*x.15)
z = 'g'^(x.14*inv(x.13))
z.1 = true
33. $appKey
= $x.12
dhmac = mac('g'^(x.14*inv((x.13*x.15))), h(<'g'^inv(x.13), $x.12>))
eph = (x.15*inv(x.14))
z = 'g'^(x.14*inv((x.13*x.15)))
z.1 = true
34. $appKey
= $x.12
dhmac = mac('g'^(x.14*inv((x.13*x.15))),
h(<'g'^(x.16*inv(x.13)), $x.12>))
eph = (x.15*x.16*inv(x.14))
z = 'g'^(x.14*inv((x.13*x.15)))
z.1 = true
35. $appKey
= $x.12
dhmac = mac('g'^(x.15*x.16*inv(x.13)),
h(<'g'^(x.16*x.17*inv(x.14)), $x.12>))
eph = (x.13*x.17*inv((x.14*x.15)))
z = 'g'^(x.15*x.16*inv(x.13))
z.1 = true
36. $appKey
= $x.12
dhmac = mac('g'^(x.15*x.16*inv(x.13)),
h(<'g'^(x.16*x.17*inv((x.13*x.14))), $x.12>))
eph = (x.17*inv((x.14*x.15)))
z = 'g'^(x.15*x.16*inv(x.13))
z.1 = true
37. $appKey
= $x.12
dhmac = mac('g'^(x.15*x.16*inv(x.13)), h(<'g'^(x.16*inv(x.14)), $x.12>))
eph = (x.13*inv((x.14*x.15)))
z = 'g'^(x.15*x.16*inv(x.13))
z.1 = true
38. $appKey
= $x.12
dhmac = mac('g'^(x.15*x.16*inv(x.13)),
h(<'g'^(x.16*inv((x.13*x.14))), $x.12>))
eph = inv((x.14*x.15))
z = 'g'^(x.15*x.16*inv(x.13))
z.1 = true
39. $appKey
= $x.12
dhmac = mac('g'^(x.15*inv(x.13)), h(<'g'^inv((x.13*x.14)), $x.12>))
eph = inv((x.14*x.15))
z = 'g'^(x.15*inv(x.13))
z.1 = true
40. $appKey
= $x.12
dhmac = mac('g'^(x.15*inv(x.13)),
h(<'g'^(x.15*x.16*inv((x.13*x.14))), $x.12>))
eph = (x.16*inv(x.14))
z = 'g'^(x.15*inv(x.13))
z.1 = true
41. $appKey
= $x.12
dhmac = mac('g'^(x.15*inv(x.13)), h(<'g'^(x.16*inv(x.14)), $x.12>))
eph = (x.13*x.16*inv((x.14*x.15)))
z = 'g'^(x.15*inv(x.13))
z.1 = true
42. $appKey
= $x.12
dhmac = mac('g'^(x.15*inv(x.13)),
h(<'g'^(x.16*inv((x.13*x.14))), $x.12>))
eph = (x.16*inv((x.14*x.15)))
z = 'g'^(x.15*inv(x.13))
z.1 = true
43. $appKey
= $x.12
dhmac = mac('g'^(x.15*inv(x.14)), h(<'g'^inv(x.13), $x.12>))
eph = (x.14*inv((x.13*x.15)))
z = 'g'^(x.15*inv(x.14))
z.1 = true
44. $appKey
= $x.12
dhmac = mac('g'^(x.15*inv(x.14)),
h(<'g'^(x.15*inv((x.13*x.14))), $x.12>))
eph = inv(x.13)
z = 'g'^(x.15*inv(x.14))
z.1 = true
45. $appKey
= $x.12
dhmac = mac('g'^(x.15*inv((x.13*x.14))),
h(<'g'^(x.15*x.16*inv(x.13)), $x.12>))
eph = (x.14*x.16)
z = 'g'^(x.15*inv((x.13*x.14)))
z.1 = true
46. $appKey
= $x.12
dhmac = mac('g'^(x.15*inv((x.13*x.14))),
h(<'g'^(x.15*inv(x.13)), $x.12>))
eph = x.14
z = 'g'^(x.15*inv((x.13*x.14)))
z.1 = true
47. $appKey
= $x.12
dhmac = mac('g'^(x.16*x.17*inv((x.13*x.14))),
h(<'g'^(x.17*x.18*inv((x.13*x.15))), $x.12>))
eph = (x.14*x.18*inv((x.15*x.16)))
z = 'g'^(x.16*x.17*inv((x.13*x.14)))
z.1 = true
48. $appKey
= $x.12
dhmac = mac('g'^(x.16*x.17*inv((x.13*x.14))),
h(<'g'^(x.17*inv((x.13*x.15))), $x.12>))
eph = (x.14*inv((x.15*x.16)))
z = 'g'^(x.16*x.17*inv((x.13*x.14)))
z.1 = true
49. $appKey
= $x.12
dhmac = mac('g'^(x.16*inv((x.13*x.14))),
h(<'g'^(x.17*inv((x.13*x.15))), $x.12>))
eph = (x.14*x.17*inv((x.15*x.16)))
z = 'g'^(x.16*inv((x.13*x.14)))
z.1 = true
50. $appKey
= $x.12
dhmac = mac('g'^(x.16*inv((x.13*x.15))),
h(<'g'^inv((x.13*x.14)), $x.12>))
eph = (x.15*inv((x.14*x.16)))
z = 'g'^(x.16*inv((x.13*x.15)))
z.1 = true
51. $appKey
= $x.12
dhmac = mac('g'^(x.16*inv((x.14*x.15))),
h(<'g'^(x.16*x.17*inv((x.13*x.14))), $x.12>))
eph = (x.15*x.17*inv(x.13))
z = 'g'^(x.16*inv((x.14*x.15)))
z.1 = true
52. $appKey
= $x.12
dhmac = mac('g'^(x.16*inv((x.14*x.15))),
h(<'g'^(x.16*inv((x.13*x.14))), $x.12>))
eph = (x.15*inv(x.13))
z = 'g'^(x.16*inv((x.14*x.15)))
z.1 = true
53. $appKey
= $appKey.13
dhmac = dhmac.13
eph = x.12
z = 'g'^inv(x.12)
z.1 = macv(dhmac.13, 'g'^inv(x.12), h(<'g', $appKey.13>))
54. $appKey
= $appKey.13
dhmac = dhmac.13
eph = inv(x.12)
z = 'g'^x.12
z.1 = macv(dhmac.13, 'g'^x.12, h(<'g', $appKey.13>))
55. $appKey
= $appKey.14
dhmac = dhmac.14
eph = x.12
z = 'g'^inv((x.12*x.13))
z.1 = macv(dhmac.14, 'g'^inv((x.12*x.13)),
h(<'g'^inv(x.13), $appKey.14>))
56. $appKey
= $appKey.14
dhmac = dhmac.14
eph = x.12
z = 'g'^(x.13*inv(x.12))
z.1 = macv(dhmac.14, 'g'^(x.13*inv(x.12)), h(<'g'^x.13, $appKey.14>))
57. $appKey
= $appKey.14
dhmac = dhmac.14
eph = inv(x.12)
z = 'g'^(x.12*x.13)
z.1 = macv(dhmac.14, 'g'^(x.12*x.13), h(<'g'^x.13, $appKey.14>))
58. $appKey
= $appKey.14
dhmac = dhmac.14
eph = inv(x.13)
z = 'g'^inv(x.12)
z.1 = macv(dhmac.14, 'g'^inv(x.12),
h(<'g'^inv((x.12*x.13)), $appKey.14>))
59. $appKey
= $appKey.14
dhmac = dhmac.14
eph = inv((x.12*x.13))
z = 'g'^x.12
z.1 = macv(dhmac.14, 'g'^x.12, h(<'g'^inv(x.13), $appKey.14>))
60. $appKey
= $appKey.14
dhmac = dhmac.14
eph = (x.12*x.13)
z = 'g'^inv(x.12)
z.1 = macv(dhmac.14, 'g'^inv(x.12), h(<'g'^x.13, $appKey.14>))
61. $appKey
= $appKey.14
dhmac = dhmac.14
eph = (x.12*inv(x.13))
z = 'g'^(x.13*inv(x.12))
z.1 = macv(dhmac.14, 'g'^(x.13*inv(x.12)), h(<'g', $appKey.14>))
62. $appKey
= $appKey.14
dhmac = dhmac.14
eph = (x.13*inv(x.12))
z = 'g'^x.12
z.1 = macv(dhmac.14, 'g'^x.12, h(<'g'^x.13, $appKey.14>))
63. $appKey
= $appKey.15
dhmac = dhmac.15
eph = x.12
z = 'g'^(x.13*inv((x.12*x.14)))
z.1 = macv(dhmac.15, 'g'^(x.13*inv((x.12*x.14))),
h(<'g'^(x.13*inv(x.14)), $appKey.15>))
64. $appKey
= $appKey.15
dhmac = dhmac.15
eph = inv(x.12)
z = 'g'^(x.14*inv(x.13))
z.1 = macv(dhmac.15, 'g'^(x.14*inv(x.13)),
h(<'g'^(x.14*inv((x.12*x.13))), $appKey.15>))
65. $appKey
= $appKey.15
dhmac = dhmac.15
eph = inv((x.13*x.14))
z = 'g'^(x.12*x.13)
z.1 = macv(dhmac.15, 'g'^(x.12*x.13),
h(<'g'^(x.12*inv(x.14)), $appKey.15>))
66. $appKey
= $appKey.15
dhmac = dhmac.15
eph = inv((x.13*x.14))
z = 'g'^(x.13*inv(x.12))
z.1 = macv(dhmac.15, 'g'^(x.13*inv(x.12)),
h(<'g'^inv((x.12*x.14)), $appKey.15>))
67. $appKey
= $appKey.15
dhmac = dhmac.15
eph = (x.12*x.14)
z = 'g'^(x.13*inv(x.12))
z.1 = macv(dhmac.15, 'g'^(x.13*inv(x.12)),
h(<'g'^(x.13*x.14), $appKey.15>))
68. $appKey
= $appKey.15
dhmac = dhmac.15
eph = (x.12*x.14*inv(x.13))
z = 'g'^(x.13*inv(x.12))
z.1 = macv(dhmac.15, 'g'^(x.13*inv(x.12)), h(<'g'^x.14, $appKey.15>))
69. $appKey
= $appKey.15
dhmac = dhmac.15
eph = (x.12*inv(x.13))
z = 'g'^(x.13*x.14*inv(x.12))
z.1 = macv(dhmac.15, 'g'^(x.13*x.14*inv(x.12)),
h(<'g'^x.14, $appKey.15>))
70. $appKey
= $appKey.15
dhmac = dhmac.15
eph = (x.12*inv((x.13*x.14)))
z = 'g'^(x.13*inv(x.12))
z.1 = macv(dhmac.15, 'g'^(x.13*inv(x.12)),
h(<'g'^inv(x.14), $appKey.15>))
71. $appKey
= $appKey.15
dhmac = dhmac.15
eph = (x.13*x.14)
z = 'g'^inv((x.12*x.13))
z.1 = macv(dhmac.15, 'g'^inv((x.12*x.13)),
h(<'g'^(x.14*inv(x.12)), $appKey.15>))
72. $appKey
= $appKey.15
dhmac = dhmac.15
eph = (x.14*inv(x.12))
z = 'g'^inv((x.13*x.14))
z.1 = macv(dhmac.15, 'g'^inv((x.13*x.14)),
h(<'g'^inv((x.12*x.13)), $appKey.15>))
73. $appKey
= $appKey.15
dhmac = dhmac.15
eph = (x.14*inv(x.12))
z = 'g'^(x.12*x.13)
z.1 = macv(dhmac.15, 'g'^(x.12*x.13), h(<'g'^(x.13*x.14), $appKey.15>))
74. $appKey
= $appKey.15
dhmac = dhmac.15
eph = (x.14*inv(x.12))
z = 'g'^(x.12*inv((x.13*x.14)))
z.1 = macv(dhmac.15, 'g'^(x.12*inv((x.13*x.14))),
h(<'g'^inv(x.13), $appKey.15>))
75. $appKey
= $appKey.15
dhmac = dhmac.15
eph = (x.14*inv(x.13))
z = 'g'^inv(x.12)
z.1 = macv(dhmac.15, 'g'^inv(x.12),
h(<'g'^(x.14*inv((x.12*x.13))), $appKey.15>))
76. $appKey
= $appKey.15
dhmac = dhmac.15
eph = (x.14*inv((x.12*x.13)))
z = 'g'^x.12
z.1 = macv(dhmac.15, 'g'^x.12, h(<'g'^(x.14*inv(x.13)), $appKey.15>))
77. $appKey
= $appKey.16
dhmac = dhmac.16
eph = inv((x.14*x.15))
z = 'g'^(x.13*x.14*inv(x.12))
z.1 = macv(dhmac.16, 'g'^(x.13*x.14*inv(x.12)),
h(<'g'^(x.13*inv((x.12*x.15))), $appKey.16>))
78. $appKey
= $appKey.16
dhmac = dhmac.16
eph = (x.12*x.15*inv(x.13))
z = 'g'^(x.13*x.14*inv(x.12))
z.1 = macv(dhmac.16, 'g'^(x.13*x.14*inv(x.12)),
h(<'g'^(x.14*x.15), $appKey.16>))
79. $appKey
= $appKey.16
dhmac = dhmac.16
eph = (x.12*x.15*inv((x.13*x.14)))
z = 'g'^(x.13*inv(x.12))
z.1 = macv(dhmac.16, 'g'^(x.13*inv(x.12)),
h(<'g'^(x.15*inv(x.14)), $appKey.16>))
80. $appKey
= $appKey.16
dhmac = dhmac.16
eph = (x.12*inv((x.14*x.15)))
z = 'g'^(x.13*x.14*inv(x.12))
z.1 = macv(dhmac.16, 'g'^(x.13*x.14*inv(x.12)),
h(<'g'^(x.13*inv(x.15)), $appKey.16>))
81. $appKey
= $appKey.16
dhmac = dhmac.16
eph = (x.14*x.15)
z = 'g'^(x.12*inv((x.13*x.14)))
z.1 = macv(dhmac.16, 'g'^(x.12*inv((x.13*x.14))),
h(<'g'^(x.12*x.15*inv(x.13)), $appKey.16>))
82. $appKey
= $appKey.16
dhmac = dhmac.16
eph = (x.14*x.15*inv(x.12))
z = 'g'^inv((x.13*x.14))
z.1 = macv(dhmac.16, 'g'^inv((x.13*x.14)),
h(<'g'^(x.15*inv((x.12*x.13))), $appKey.16>))
83. $appKey
= $appKey.16
dhmac = dhmac.16
eph = (x.14*x.15*inv(x.12))
z = 'g'^(x.12*inv((x.13*x.14)))
z.1 = macv(dhmac.16, 'g'^(x.12*inv((x.13*x.14))),
h(<'g'^(x.15*inv(x.13)), $appKey.16>))
84. $appKey
= $appKey.16
dhmac = dhmac.16
eph = (x.14*inv((x.12*x.15)))
z = 'g'^(x.12*inv((x.13*x.14)))
z.1 = macv(dhmac.16, 'g'^(x.12*inv((x.13*x.14))),
h(<'g'^inv((x.13*x.15)), $appKey.16>))
85. $appKey
= $appKey.16
dhmac = dhmac.16
eph = (x.15*inv(x.12))
z = 'g'^(x.12*x.13*inv((x.14*x.15)))
z.1 = macv(dhmac.16, 'g'^(x.12*x.13*inv((x.14*x.15))),
h(<'g'^(x.13*inv(x.14)), $appKey.16>))
86. $appKey
= $appKey.16
dhmac = dhmac.16
eph = (x.15*inv(x.12))
z = 'g'^(x.13*inv((x.14*x.15)))
z.1 = macv(dhmac.16, 'g'^(x.13*inv((x.14*x.15))),
h(<'g'^(x.13*inv((x.12*x.14))), $appKey.16>))
87. $appKey
= $appKey.16
dhmac = dhmac.16
eph = (x.15*inv(x.13))
z = 'g'^(x.14*inv(x.12))
z.1 = macv(dhmac.16, 'g'^(x.14*inv(x.12)),
h(<'g'^(x.14*x.15*inv((x.12*x.13))), $appKey.16>))
88. $appKey
= $appKey.16
dhmac = dhmac.16
eph = (x.15*inv((x.13*x.14)))
z = 'g'^(x.12*x.13)
z.1 = macv(dhmac.16, 'g'^(x.12*x.13),
h(<'g'^(x.12*x.15*inv(x.14)), $appKey.16>))
89. $appKey
= $appKey.16
dhmac = dhmac.16
eph = (x.15*inv((x.13*x.14)))
z = 'g'^(x.13*inv(x.12))
z.1 = macv(dhmac.16, 'g'^(x.13*inv(x.12)),
h(<'g'^(x.15*inv((x.12*x.14))), $appKey.16>))
90. $appKey
= $appKey.17
dhmac = dhmac.17
eph = (x.12*x.16*inv((x.14*x.15)))
z = 'g'^(x.13*x.14*inv(x.12))
z.1 = macv(dhmac.17, 'g'^(x.13*x.14*inv(x.12)),
h(<'g'^(x.13*x.16*inv(x.15)), $appKey.17>))
91. $appKey
= $appKey.17
dhmac = dhmac.17
eph = (x.14*x.16*inv((x.12*x.15)))
z = 'g'^(x.12*inv((x.13*x.14)))
z.1 = macv(dhmac.17, 'g'^(x.12*inv((x.13*x.14))),
h(<'g'^(x.16*inv((x.13*x.15))), $appKey.17>))
92. $appKey
= $appKey.17
dhmac = dhmac.17
eph = (x.15*x.16*inv(x.12))
z = 'g'^(x.12*x.13*inv((x.14*x.15)))
z.1 = macv(dhmac.17, 'g'^(x.12*x.13*inv((x.14*x.15))),
h(<'g'^(x.13*x.16*inv(x.14)), $appKey.17>))
93. $appKey
= $appKey.17
dhmac = dhmac.17
eph = (x.15*x.16*inv(x.12))
z = 'g'^(x.13*inv((x.14*x.15)))
z.1 = macv(dhmac.17, 'g'^(x.13*inv((x.14*x.15))),
h(<'g'^(x.13*x.16*inv((x.12*x.14))), $appKey.17>))
94. $appKey
= $appKey.17
dhmac = dhmac.17
eph = (x.15*inv((x.13*x.16)))
z = 'g'^(x.12*x.13*inv((x.14*x.15)))
z.1 = macv(dhmac.17, 'g'^(x.12*x.13*inv((x.14*x.15))),
h(<'g'^(x.12*inv((x.14*x.16))), $appKey.17>))
95. $appKey
= $appKey.17
dhmac = dhmac.17
eph = (x.16*inv((x.14*x.15)))
z = 'g'^(x.13*x.14*inv(x.12))
z.1 = macv(dhmac.17, 'g'^(x.13*x.14*inv(x.12)),
h(<'g'^(x.13*x.16*inv((x.12*x.15))), $appKey.17>))
96. $appKey
= $appKey.18
dhmac = dhmac.18
eph = (x.15*x.17*inv((x.13*x.16)))
z = 'g'^(x.12*x.13*inv((x.14*x.15)))
z.1 = macv(dhmac.18, 'g'^(x.12*x.13*inv((x.14*x.15))),
h(<'g'^(x.12*x.17*inv((x.14*x.16))), $appKey.18>))
*/
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 Reachable:
exists-trace "∃ #i. (Reach( ) @ #i) ∧ (¬(∃ X #j. LtkReveal( X ) @ #j))"
/*
guarded formula characterizing all satisfying traces:
"∃ #i. (Reach( ) @ #i) ∧ ∀ X #j. (LtkReveal( X ) @ #j) ⇒ ⊥"
*/
by sorry
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!
Reachable (exists-trace): analysis incomplete (1 steps)
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