1(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
2    Copyright   1996  University of Cambridge
3*)
4
5section \<open>Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols\<close>
6
7theory Auth_Shared
8imports
9  NS_Shared
10  Kerberos_BAN
11  Kerberos_BAN_Gets
12  KerberosIV
13  KerberosIV_Gets
14  KerberosV
15  OtwayRees
16  OtwayRees_AN
17  OtwayRees_Bad
18  OtwayReesBella
19  WooLam
20  Recur
21  Yahalom
22  Yahalom2
23  Yahalom_Bad
24  ZhouGollmann
25begin
26
27end
28