# HG changeset patch
# User haftmann
# Date 1253540020 -7200
# Node ID 8ae912371831115099f7b65082c7203adef13c3c
# Parent  2489e3c3562bc16ce5213392183929cfb10d765d
added session entry point theories

diff -r 2489e3c3562b -r 8ae912371831 src/HOL/Auth/Auth_Public.thy
--- /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
diff -r 2489e3c3562b -r 8ae912371831 src/HOL/Auth/Auth_Shared.thy
--- /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
diff -r 2489e3c3562b -r 8ae912371831 src/HOL/Auth/Guard/Auth_Guard_Public.thy
--- /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
diff -r 2489e3c3562b -r 8ae912371831 src/HOL/Auth/Guard/Auth_Guard_Shared.thy
--- /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
diff -r 2489e3c3562b -r 8ae912371831 src/HOL/Auth/ROOT.ML
--- 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"];
diff -r 2489e3c3562b -r 8ae912371831 src/HOL/Auth/Smartcard/Auth_Smartcard.thy
--- /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
diff -r 2489e3c3562b -r 8ae912371831 src/HOL/IsaMakefile
--- 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	\