10 Proc. Royal Soc. 426 (1989) |
10 Proc. Royal Soc. 426 (1989) |
11 *) |
11 *) |
12 |
12 |
13 OtwayRees_Bad = Shared + |
13 OtwayRees_Bad = Shared + |
14 |
14 |
15 consts lost :: agent set (*No need for it to be a variable*) |
15 consts otway :: event list set |
16 otway :: event list set |
|
17 |
16 |
18 inductive otway |
17 inductive otway |
19 intrs |
18 intrs |
20 (*Initial trace is empty*) |
19 (*Initial trace is empty*) |
21 Nil "[]: otway" |
20 Nil "[]: otway" |
22 |
21 |
23 (*The spy MAY say anything he CAN say. We do not expect him to |
22 (*The spy MAY say anything he CAN say. We do not expect him to |
24 invent new nonces here, but he can also use NS1. Common to |
23 invent new nonces here, but he can also use NS1. Common to |
25 all similar protocols.*) |
24 all similar protocols.*) |
26 Fake "[| evs: otway; B ~= Spy; X: synth (analz (sees lost Spy evs)) |] |
25 Fake "[| evs: otway; B ~= Spy; X: synth (analz (sees Spy evs)) |] |
27 ==> Says Spy B X # evs : otway" |
26 ==> Says Spy B X # evs : otway" |
28 |
27 |
29 (*Alice initiates a protocol run*) |
28 (*Alice initiates a protocol run*) |
30 OR1 "[| evs: otway; A ~= B; B ~= Server; Nonce NA ~: used evs |] |
29 OR1 "[| evs: otway; A ~= B; B ~= Server; Nonce NA ~: used evs |] |
31 ==> Says A B {|Nonce NA, Agent A, Agent B, |
30 ==> Says A B {|Nonce NA, Agent A, Agent B, |