--- a/src/HOL/Auth/Guard/Analz.thy Fri Feb 18 15:46:13 2011 +0100
+++ b/src/HOL/Auth/Guard/Analz.thy Fri Feb 18 16:07:32 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: december 2001
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Analz.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2001 University of Cambridge
+*)
header{*Decomposition of Analz into two parts*}
--- a/src/HOL/Auth/Guard/Extensions.thy Fri Feb 18 15:46:13 2011 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy Fri Feb 18 16:07:32 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: november 2001
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Extensions.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2001 University of Cambridge
+*)
header {*Extensions to Standard Theories*}
--- a/src/HOL/Auth/Guard/Guard.thy Fri Feb 18 15:46:13 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy Fri Feb 18 16:07:32 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: january 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Guard.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*Protocol-Independent Confidentiality Theorem on Nonces*}
--- a/src/HOL/Auth/Guard/GuardK.thy Fri Feb 18 15:46:13 2011 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy Fri Feb 18 16:07:32 2011 +0100
@@ -1,18 +1,12 @@
-(******************************************************************************
-very similar to Guard except:
+(* Title: HOL/Auth/Guard/GuardK.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+
+Very similar to Guard except:
- Guard is replaced by GuardK, guard by guardK, Nonce by Key
- some scripts are slightly modified (+ keyset_in, kparts_parts)
- the hypothesis Key n ~:G (keyset G) is added
-
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+*)
header{*protocol-independent confidentiality theorem on keys*}
--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy Fri Feb 18 15:46:13 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy Fri Feb 18 16:07:32 2011 +0100
@@ -1,15 +1,9 @@
-(******************************************************************************
-incorporating Lowe's fix (inclusion of B's identity in round 2)
+(* Title: HOL/Auth/Guard/Guard_NS_Public.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+Incorporating Lowe's fix (inclusion of B's identity in round 2).
+*)
header{*Needham-Schroeder-Lowe Public-Key Protocol*}
--- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy Fri Feb 18 15:46:13 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy Fri Feb 18 16:07:32 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Guard_OtwayRees.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*Otway-Rees Protocol*}
--- a/src/HOL/Auth/Guard/Guard_Public.thy Fri Feb 18 15:46:13 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_Public.thy Fri Feb 18 16:07:32 2011 +0100
@@ -1,15 +1,9 @@
-(******************************************************************************
-lemmas on guarded messages for public protocols
+(* Title: HOL/Auth/Guard/Guard_Public.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+Lemmas on guarded messages for public protocols.
+*)
theory Guard_Public imports Guard Public Extensions begin
--- a/src/HOL/Auth/Guard/Guard_Shared.thy Fri Feb 18 15:46:13 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy Fri Feb 18 16:07:32 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Guard_Shared.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*lemmas on guarded messages for protocols with symmetric keys*}
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy Fri Feb 18 15:46:13 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy Fri Feb 18 16:07:32 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Guard_Yahalom.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*Yahalom Protocol*}
--- a/src/HOL/Auth/Guard/List_Msg.thy Fri Feb 18 15:46:13 2011 +0100
+++ b/src/HOL/Auth/Guard/List_Msg.thy Fri Feb 18 16:07:32 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: november 2001
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/List_Msg.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2001 University of Cambridge
+*)
header{*Lists of Messages and Lists of Agents*}
--- a/src/HOL/Auth/Guard/P1.thy Fri Feb 18 15:46:13 2011 +0100
+++ b/src/HOL/Auth/Guard/P1.thy Fri Feb 18 16:07:32 2011 +0100
@@ -1,17 +1,11 @@
-(******************************************************************************
-from G. Karjoth, N. Asokan and C. Gulcu
-"Protecting the computation results of free-roaming agents"
-Mobiles Agents 1998, LNCS 1477
+(* Title: HOL/Auth/Guard/P1.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
-date: february 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+From G. Karjoth, N. Asokan and C. Gulcu
+"Protecting the computation results of free-roaming agents"
+Mobiles Agents 1998, LNCS 1477.
+*)
header{*Protocol P1*}
--- a/src/HOL/Auth/Guard/P2.thy Fri Feb 18 15:46:13 2011 +0100
+++ b/src/HOL/Auth/Guard/P2.thy Fri Feb 18 16:07:32 2011 +0100
@@ -1,17 +1,11 @@
-(******************************************************************************
-from G. Karjoth, N. Asokan and C. Gulcu
-"Protecting the computation results of free-roaming agents"
-Mobiles Agents 1998, LNCS 1477
+(* Title: HOL/Auth/Guard/P2.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+From G. Karjoth, N. Asokan and C. Gulcu
+"Protecting the computation results of free-roaming agents"
+Mobiles Agents 1998, LNCS 1477.
+*)
header{*Protocol P2*}
--- a/src/HOL/Auth/Guard/Proto.thy Fri Feb 18 15:46:13 2011 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy Fri Feb 18 16:07:32 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: april 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Proto.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*Other Protocol-Independent Results*}