keks · January 20, 2017 12:32
diff --git a/halfway2.log b/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)

 ==============================================================================
	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.91inv((~eph.48x.90)))
	z.1 = 'g'^(x.91*inv(x.90))
	z.2 = macv(dhmac.50, 'g'^(x.91inv((~eph.48x.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.93inv((~eph.49x.92))), h($appKey.48))
	z = 'g'^(x.93inv((~eph.49x.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.15inv((x.13x.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.15inv((x.13x.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.13x.14)), h(<'g'^(x.15inv(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.14x.15)), h(<'g'^inv((x.13x.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.16inv((x.13x.14))), $x.12>))
	eph = (x.15x.16inv(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.13x.14), h(<'g'^(x.14x.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.14x.15), h(<'g'^(x.15x.16*inv(x.13)), $x.12>))
	eph = (x.16inv((x.13x.14)))
	z = 'g'^(x.14*x.15)
	z.1 = true

	24. $appKey
	= $x.12
	dhmac = mac('g'^(x.14x.15), h(<'g'^(x.15inv(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.14x.15inv(x.13)), h(<'g'^x.15, $x.12>))
	eph = (x.13*inv(x.14))
	z = 'g'^(x.14x.15inv(x.13))
	z.1 = true

	26. $appKey
	= $x.12
	dhmac = mac('g'^(x.14x.15inv(x.13)), h(<'g'^(x.15*x.16), $x.12>))
	eph = (x.13x.16inv(x.14))
	z = 'g'^(x.14x.15inv(x.13))
	z.1 = true

	27. $appKey
	= $x.12
	dhmac = mac('g'^(x.14x.16inv((x.13*x.15))),
	h(<'g'^(x.16x.17inv(x.13)), $x.12>))
	eph = (x.15x.17inv(x.14))
	z = 'g'^(x.14x.16inv((x.13*x.15)))
	z.1 = true

	28. $appKey
	= $x.12
	dhmac = mac('g'^(x.14x.16inv((x.13*x.15))),
	h(<'g'^(x.16*inv(x.13)), $x.12>))
	eph = (x.15*inv(x.14))
	z = 'g'^(x.14x.16inv((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.13x.15inv(x.14))
	z = 'g'^(x.14*inv(x.13))
	z.1 = true

	32. $appKey
	= $x.12
	dhmac = mac('g'^(x.14inv(x.13)), h(<'g'^(x.14x.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.14inv((x.13x.15))), h(<'g'^inv(x.13), $x.12>))
	eph = (x.15*inv(x.14))
	z = 'g'^(x.14inv((x.13x.15)))
	z.1 = true

	34. $appKey
	= $x.12
	dhmac = mac('g'^(x.14inv((x.13x.15))),
	h(<'g'^(x.16*inv(x.13)), $x.12>))
	eph = (x.15x.16inv(x.14))
	z = 'g'^(x.14inv((x.13x.15)))
	z.1 = true

	35. $appKey
	= $x.12
	dhmac = mac('g'^(x.15x.16inv(x.13)),
	h(<'g'^(x.16x.17inv(x.14)), $x.12>))
	eph = (x.13x.17inv((x.14*x.15)))
	z = 'g'^(x.15x.16inv(x.13))
	z.1 = true

	36. $appKey
	= $x.12
	dhmac = mac('g'^(x.15x.16inv(x.13)),
	h(<'g'^(x.16x.17inv((x.13*x.14))), $x.12>))
	eph = (x.17inv((x.14x.15)))
	z = 'g'^(x.15x.16inv(x.13))
	z.1 = true

	37. $appKey
	= $x.12
	dhmac = mac('g'^(x.15x.16inv(x.13)), h(<'g'^(x.16*inv(x.14)), $x.12>))
	eph = (x.13inv((x.14x.15)))
	z = 'g'^(x.15x.16inv(x.13))
	z.1 = true

	38. $appKey
	= $x.12
	dhmac = mac('g'^(x.15x.16inv(x.13)),
	h(<'g'^(x.16inv((x.13x.14))), $x.12>))
	eph = inv((x.14*x.15))
	z = 'g'^(x.15x.16inv(x.13))
	z.1 = true

	39. $appKey
	= $x.12
	dhmac = mac('g'^(x.15inv(x.13)), h(<'g'^inv((x.13x.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.15x.16inv((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.15inv(x.13)), h(<'g'^(x.16inv(x.14)), $x.12>))
	eph = (x.13x.16inv((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.16inv((x.13x.14))), $x.12>))
	eph = (x.16inv((x.14x.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.14inv((x.13x.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.15inv((x.13x.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.15inv((x.13x.14))),
	h(<'g'^(x.15x.16inv(x.13)), $x.12>))
	eph = (x.14*x.16)
	z = 'g'^(x.15inv((x.13x.14)))
	z.1 = true

	46. $appKey
	= $x.12
	dhmac = mac('g'^(x.15inv((x.13x.14))),
	h(<'g'^(x.15*inv(x.13)), $x.12>))
	eph = x.14
	z = 'g'^(x.15inv((x.13x.14)))
	z.1 = true

	47. $appKey
	= $x.12
	dhmac = mac('g'^(x.16x.17inv((x.13*x.14))),
	h(<'g'^(x.17x.18inv((x.13*x.15))), $x.12>))
	eph = (x.14x.18inv((x.15*x.16)))
	z = 'g'^(x.16x.17inv((x.13*x.14)))
	z.1 = true

	48. $appKey
	= $x.12
	dhmac = mac('g'^(x.16x.17inv((x.13*x.14))),
	h(<'g'^(x.17inv((x.13x.15))), $x.12>))
	eph = (x.14inv((x.15x.16)))
	z = 'g'^(x.16x.17inv((x.13*x.14)))
	z.1 = true

	49. $appKey
	= $x.12
	dhmac = mac('g'^(x.16inv((x.13x.14))),
	h(<'g'^(x.17inv((x.13x.15))), $x.12>))
	eph = (x.14x.17inv((x.15*x.16)))
	z = 'g'^(x.16inv((x.13x.14)))
	z.1 = true

	50. $appKey
	= $x.12
	dhmac = mac('g'^(x.16inv((x.13x.15))),
	h(<'g'^inv((x.13*x.14)), $x.12>))
	eph = (x.15inv((x.14x.16)))
	z = 'g'^(x.16inv((x.13x.15)))
	z.1 = true

	51. $appKey
	= $x.12
	dhmac = mac('g'^(x.16inv((x.14x.15))),
	h(<'g'^(x.16x.17inv((x.13*x.14))), $x.12>))
	eph = (x.15x.17inv(x.13))
	z = 'g'^(x.16inv((x.14x.15)))
	z.1 = true

	52. $appKey
	= $x.12
	dhmac = mac('g'^(x.16inv((x.14x.15))),
	h(<'g'^(x.16inv((x.13x.14))), $x.12>))
	eph = (x.15*inv(x.13))
	z = 'g'^(x.16inv((x.14x.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.13inv((x.12x.14)))
	z.1 = macv(dhmac.15, 'g'^(x.13inv((x.12x.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.14inv((x.12x.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.12x.14inv(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.13x.14inv(x.12))
	z.1 = macv(dhmac.15, 'g'^(x.13x.14inv(x.12)),
	h(<'g'^x.14, $appKey.15>))

	70. $appKey
	= $appKey.15
	dhmac = dhmac.15
	eph = (x.12inv((x.13x.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.12x.13), h(<'g'^(x.13x.14), $appKey.15>))

	74. $appKey
	= $appKey.15
	dhmac = dhmac.15
	eph = (x.14*inv(x.12))
	z = 'g'^(x.12inv((x.13x.14)))
	z.1 = macv(dhmac.15, 'g'^(x.12inv((x.13x.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.14inv((x.12x.13))), $appKey.15>))

	76. $appKey
	= $appKey.15
	dhmac = dhmac.15
	eph = (x.14inv((x.12x.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.13x.14inv(x.12))
	z.1 = macv(dhmac.16, 'g'^(x.13x.14inv(x.12)),
	h(<'g'^(x.13inv((x.12x.15))), $appKey.16>))

	78. $appKey
	= $appKey.16
	dhmac = dhmac.16
	eph = (x.12x.15inv(x.13))
	z = 'g'^(x.13x.14inv(x.12))
	z.1 = macv(dhmac.16, 'g'^(x.13x.14inv(x.12)),
	h(<'g'^(x.14*x.15), $appKey.16>))

	79. $appKey
	= $appKey.16
	dhmac = dhmac.16
	eph = (x.12x.15inv((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.12inv((x.14x.15)))
	z = 'g'^(x.13x.14inv(x.12))
	z.1 = macv(dhmac.16, 'g'^(x.13x.14inv(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.12inv((x.13x.14)))
	z.1 = macv(dhmac.16, 'g'^(x.12inv((x.13x.14))),
	h(<'g'^(x.12x.15inv(x.13)), $appKey.16>))

	82. $appKey
	= $appKey.16
	dhmac = dhmac.16
	eph = (x.14x.15inv(x.12))
	z = 'g'^inv((x.13*x.14))
	z.1 = macv(dhmac.16, 'g'^inv((x.13*x.14)),
	h(<'g'^(x.15inv((x.12x.13))), $appKey.16>))

	83. $appKey
	= $appKey.16
	dhmac = dhmac.16
	eph = (x.14x.15inv(x.12))
	z = 'g'^(x.12inv((x.13x.14)))
	z.1 = macv(dhmac.16, 'g'^(x.12inv((x.13x.14))),
	h(<'g'^(x.15*inv(x.13)), $appKey.16>))

	84. $appKey
	= $appKey.16
	dhmac = dhmac.16
	eph = (x.14inv((x.12x.15)))
	z = 'g'^(x.12inv((x.13x.14)))
	z.1 = macv(dhmac.16, 'g'^(x.12inv((x.13x.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.12x.13inv((x.14*x.15)))
	z.1 = macv(dhmac.16, 'g'^(x.12x.13inv((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.13inv((x.14x.15)))
	z.1 = macv(dhmac.16, 'g'^(x.13inv((x.14x.15))),
	h(<'g'^(x.13inv((x.12x.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.14x.15inv((x.12*x.13))), $appKey.16>))

	88. $appKey
	= $appKey.16
	dhmac = dhmac.16
	eph = (x.15inv((x.13x.14)))
	z = 'g'^(x.12*x.13)
	z.1 = macv(dhmac.16, 'g'^(x.12*x.13),
	h(<'g'^(x.12x.15inv(x.14)), $appKey.16>))

	89. $appKey
	= $appKey.16
	dhmac = dhmac.16
	eph = (x.15inv((x.13x.14)))
	z = 'g'^(x.13*inv(x.12))
	z.1 = macv(dhmac.16, 'g'^(x.13*inv(x.12)),
	h(<'g'^(x.15inv((x.12x.14))), $appKey.16>))

	90. $appKey
	= $appKey.17
	dhmac = dhmac.17
	eph = (x.12x.16inv((x.14*x.15)))
	z = 'g'^(x.13x.14inv(x.12))
	z.1 = macv(dhmac.17, 'g'^(x.13x.14inv(x.12)),
	h(<'g'^(x.13x.16inv(x.15)), $appKey.17>))

	91. $appKey
	= $appKey.17
	dhmac = dhmac.17
	eph = (x.14x.16inv((x.12*x.15)))
	z = 'g'^(x.12inv((x.13x.14)))
	z.1 = macv(dhmac.17, 'g'^(x.12inv((x.13x.14))),
	h(<'g'^(x.16inv((x.13x.15))), $appKey.17>))

	92. $appKey
	= $appKey.17
	dhmac = dhmac.17
	eph = (x.15x.16inv(x.12))
	z = 'g'^(x.12x.13inv((x.14*x.15)))
	z.1 = macv(dhmac.17, 'g'^(x.12x.13inv((x.14*x.15))),
	h(<'g'^(x.13x.16inv(x.14)), $appKey.17>))

	93. $appKey
	= $appKey.17
	dhmac = dhmac.17
	eph = (x.15x.16inv(x.12))
	z = 'g'^(x.13inv((x.14x.15)))
	z.1 = macv(dhmac.17, 'g'^(x.13inv((x.14x.15))),
	h(<'g'^(x.13x.16inv((x.12*x.14))), $appKey.17>))

	94. $appKey
	= $appKey.17
	dhmac = dhmac.17
	eph = (x.15inv((x.13x.16)))
	z = 'g'^(x.12x.13inv((x.14*x.15)))
	z.1 = macv(dhmac.17, 'g'^(x.12x.13inv((x.14*x.15))),
	h(<'g'^(x.12inv((x.14x.16))), $appKey.17>))

	95. $appKey
	= $appKey.17
	dhmac = dhmac.17
	eph = (x.16inv((x.14x.15)))
	z = 'g'^(x.13x.14inv(x.12))
	z.1 = macv(dhmac.17, 'g'^(x.13x.14inv(x.12)),
	h(<'g'^(x.13x.16inv((x.12*x.15))), $appKey.17>))

	96. $appKey
	= $appKey.18
	dhmac = dhmac.18
	eph = (x.15x.17inv((x.13*x.16)))
	z = 'g'^(x.12x.13inv((x.14*x.15)))
	z.1 = macv(dhmac.18, 'g'^(x.12x.13inv((x.14*x.15))),
	h(<'g'^(x.12x.17inv((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)

	==============================================================================