equal
deleted
inserted
replaced
11 Cambridge CB3 0FD, United Kingdom |
11 Cambridge CB3 0FD, United Kingdom |
12 ******************************************************************************) |
12 ******************************************************************************) |
13 |
13 |
14 header{*Needham-Schroeder-Lowe Public-Key Protocol*} |
14 header{*Needham-Schroeder-Lowe Public-Key Protocol*} |
15 |
15 |
16 theory NS_Public = Guard_Public: |
16 theory NS_Public imports Guard_Public begin |
17 |
17 |
18 subsection{*messages used in the protocol*} |
18 subsection{*messages used in the protocol*} |
19 |
19 |
20 syntax ns1 :: "agent => agent => nat => event" |
20 syntax ns1 :: "agent => agent => nat => event" |
21 |
21 |