equal
deleted
inserted
replaced
7 |
7 |
8 Demonstrates of why Oops is necessary. This protocol can be attacked because |
8 Demonstrates of why Oops is necessary. This protocol can be attacked because |
9 it doesn't keep NB secret, but without Oops it can be "verified" anyway. |
9 it doesn't keep NB secret, but without Oops it can be "verified" anyway. |
10 The issues are discussed in lcp's LICS 2000 invited lecture. |
10 The issues are discussed in lcp's LICS 2000 invited lecture. |
11 *) |
11 *) |
|
12 |
|
13 header{*The Yahalom Protocol: A Flawed Version*} |
12 |
14 |
13 theory Yahalom_Bad = Shared: |
15 theory Yahalom_Bad = Shared: |
14 |
16 |
15 consts yahalom :: "event list set" |
17 consts yahalom :: "event list set" |
16 inductive "yahalom" |
18 inductive "yahalom" |