ATSE

SUMMARY
  UNSAFE

DETAILS
  ATTACK_FOUND
  TYPED_MODEL

PROTOCOL
  /home/span/span/testsuite/results/hlpslGenFile.if

GOAL
  Secrecy attack on (n1(Kab))

BACKEND
  CL-AtSe

STATISTICS

  Analysed   : 18 states
  Reachable  : 6 states
  Translation: 0.00 seconds
  Computation: 0.00 seconds


ATTACK TRACE
 i -> (alice,9):  start
 (alice,9) -> i:  alice.n13(Na)

 i -> (bob,8):  alice.Na(9)
 (bob,8) -> i:  bob.{alice.Na(9).n9(Nb)}_kbs

 i -> (server,7):  bob.{alice.Na(9).n9(Nb)}_kbs
 (server,7) -> i:  {bob.n7(Kab).Na(9).n9(Nb)}_kas.{alice.n7(Kab)}_kbs
                   & Secret(n7(Kab),set_99);

 i -> (bob,4):  i.Na(3)
 (bob,4) -> i:  bob.{i.Na(3).n3(Nb)}_kbs

 i -> (server,3):  bob.{i.Na(3).n3(Nb)}_kbs
 (server,3) -> i:  {bob.n1(Kab).Na(3).n3(Nb)}_kis.{i.n1(Kab)}_kbs
                   & Secret(n1(Kab),set_84);