--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Auth_Public.thy Mon Sep 21 15:33:40 2009 +0200
@@ -0,0 +1,15 @@
+(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+*)
+
+header {* Conventional protocols: rely on conventional Message, Event and Public -- Public-key protocols *}
+
+theory Auth_Public
+imports
+ "NS_Public_Bad"
+ "NS_Public"
+ "TLS"
+ "CertifiedEmail"
+begin
+
+end
--- /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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Guard/Auth_Guard_Public.thy Mon Sep 21 15:33:40 2009 +0200
@@ -0,0 +1,15 @@
+(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+*)
+
+header {* Blanqui's "guard" concept: protocol-independent secrecy *}
+
+theory Auth_Guard_Public
+imports
+ "P1"
+ "P2"
+ "Guard_NS_Public"
+ "Proto"
+begin
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Guard/Auth_Guard_Shared.thy Mon Sep 21 15:33:40 2009 +0200
@@ -0,0 +1,13 @@
+(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+*)
+
+header {* Blanqui's "guard" concept: protocol-independent secrecy *}
+
+theory Auth_Guard_Shared
+imports
+ "Guard_OtwayRees"
+ "Guard_Yahalom"
+begin
+
+end
--- a/src/HOL/Auth/ROOT.ML Mon Sep 21 15:33:40 2009 +0200
+++ b/src/HOL/Auth/ROOT.ML Mon Sep 21 15:33:40 2009 +0200
@@ -1,51 +1,2 @@
-(* Title: HOL/Auth/ROOT.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-Root file for protocol proofs.
-*)
-
-use_thys [
-
-(* Conventional protocols: rely on
- conventional Message, Event and Public *)
-
-(*Shared-key protocols*)
- "NS_Shared",
- "Kerberos_BAN",
- "Kerberos_BAN_Gets",
- "KerberosIV",
- "KerberosIV_Gets",
- "KerberosV",
- "OtwayRees",
- "OtwayRees_AN",
- "OtwayRees_Bad",
- "OtwayReesBella",
- "WooLam",
- "Recur",
- "Yahalom",
- "Yahalom2",
- "Yahalom_Bad",
- "ZhouGollmann",
-
-(*Public-key protocols*)
- "NS_Public_Bad",
- "NS_Public",
- "TLS",
- "CertifiedEmail",
-
-(*Smartcard protocols: rely on conventional Message and on new
- EventSC and Smartcard *)
-
- "Smartcard/ShoupRubin",
- "Smartcard/ShoupRubinBella",
-
-(*Blanqui's "guard" concept: protocol-independent secrecy*)
- "Guard/P1",
- "Guard/P2",
- "Guard/Guard_NS_Public",
- "Guard/Guard_OtwayRees",
- "Guard/Guard_Yahalom",
- "Guard/Proto"
-];
+use_thys ["Auth_Shared", "Auth_Public", "Smartcard/Auth_Smartcard", "Guard/Auth_Guard_Shared", "Guard/Auth_Guard_Public"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Smartcard/Auth_Smartcard.thy Mon Sep 21 15:33:40 2009 +0200
@@ -0,0 +1,13 @@
+(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+*)
+
+header {* Smartcard protocols: rely on conventional Message and on new EventSC and Smartcard *}
+
+theory Auth_Smartcard
+imports
+ "ShoupRubin"
+ "ShoupRubinBella"
+begin
+
+end
--- a/src/HOL/IsaMakefile Mon Sep 21 15:33:40 2009 +0200
+++ b/src/HOL/IsaMakefile Mon Sep 21 15:33:40 2009 +0200
@@ -619,6 +619,10 @@
HOL-Auth: HOL $(LOG)/HOL-Auth.gz
$(LOG)/HOL-Auth.gz: $(OUT)/HOL \
+ Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy \
+ Auth/Guard/Auth_Guard_Shared.thy \
+ Auth/Guard/Auth_Guard_Public.thy \
+ Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy \
Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy \
Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy \
Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy \