equal
deleted
inserted
replaced
55 Nil "[]: recur" |
55 Nil "[]: recur" |
56 |
56 |
57 (*The spy MAY say anything he CAN say. Common to |
57 (*The spy MAY say anything he CAN say. Common to |
58 all similar protocols.*) |
58 all similar protocols.*) |
59 Fake "[| evs: recur; B ~= Spy; |
59 Fake "[| evs: recur; B ~= Spy; |
60 X: synth (analz (sees Spy evs)) |] |
60 X: synth (analz (spies evs)) |] |
61 ==> Says Spy B X # evs : recur" |
61 ==> Says Spy B X # evs : recur" |
62 |
62 |
63 (*Alice initiates a protocol run. |
63 (*Alice initiates a protocol run. |
64 "Agent Server" is just a placeholder, to terminate the nesting.*) |
64 "Agent Server" is just a placeholder, to terminate the nesting.*) |
65 RA1 "[| evs1: recur; A ~= B; A ~= Server; Nonce NA ~: used evs1 |] |
65 RA1 "[| evs1: recur; A ~= B; A ~= Server; Nonce NA ~: used evs1 |] |