equal
deleted
inserted
replaced
8 From page 260 of |
8 From page 260 of |
9 Burrows, Abadi and Needham. A Logic of Authentication. |
9 Burrows, Abadi and Needham. A Logic of Authentication. |
10 Proc. Royal Soc. 426 (1989) |
10 Proc. Royal Soc. 426 (1989) |
11 *) |
11 *) |
12 |
12 |
13 header{*Verifying the Needham-Schroeder Public-Key Protocol*} |
13 section{*Verifying the Needham-Schroeder Public-Key Protocol*} |
14 |
14 |
15 theory NS_Public_Bad imports Public begin |
15 theory NS_Public_Bad imports Public begin |
16 |
16 |
17 inductive_set ns_public :: "event list set" |
17 inductive_set ns_public :: "event list set" |
18 where |
18 where |