--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Auth_Shared.thy Mon Sep 21 15:33:40 2009 +0200
@@ -0,0 +1,27 @@
+(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+*)
+
+header {* Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols *}
+
+theory Auth_Shared
+imports
+ "NS_Shared"
+ "Kerberos_BAN"
+ "Kerberos_BAN_Gets"
+ "KerberosIV"
+ "KerberosIV_Gets"
+ "KerberosV"
+ "OtwayRees"
+ "OtwayRees_AN"
+ "OtwayRees_Bad"
+ "OtwayReesBella"
+ "WooLam"
+ "Recur"
+ "Yahalom"
+ "Yahalom2"
+ "Yahalom_Bad"
+ "ZhouGollmann"
+begin
+
+end