# HG changeset patch # User wenzelm # Date 1298041652 -3600 # Node ID 6214816d79d30d5ad3ee3c4c5c634b6240f70717 # Parent 13b97824aec6ef89b554fef254b6f586ebf35843 standardized headers; diff -r 13b97824aec6 -r 6214816d79d3 src/HOL/Auth/Guard/Analz.thy --- 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*} diff -r 13b97824aec6 -r 6214816d79d3 src/HOL/Auth/Guard/Extensions.thy --- 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*} diff -r 13b97824aec6 -r 6214816d79d3 src/HOL/Auth/Guard/Guard.thy --- 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*} diff -r 13b97824aec6 -r 6214816d79d3 src/HOL/Auth/Guard/GuardK.thy --- 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*} diff -r 13b97824aec6 -r 6214816d79d3 src/HOL/Auth/Guard/Guard_NS_Public.thy --- 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*} diff -r 13b97824aec6 -r 6214816d79d3 src/HOL/Auth/Guard/Guard_OtwayRees.thy --- 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*} diff -r 13b97824aec6 -r 6214816d79d3 src/HOL/Auth/Guard/Guard_Public.thy --- 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 diff -r 13b97824aec6 -r 6214816d79d3 src/HOL/Auth/Guard/Guard_Shared.thy --- 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*} diff -r 13b97824aec6 -r 6214816d79d3 src/HOL/Auth/Guard/Guard_Yahalom.thy --- 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*} diff -r 13b97824aec6 -r 6214816d79d3 src/HOL/Auth/Guard/List_Msg.thy --- 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*} diff -r 13b97824aec6 -r 6214816d79d3 src/HOL/Auth/Guard/P1.thy --- 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*} diff -r 13b97824aec6 -r 6214816d79d3 src/HOL/Auth/Guard/P2.thy --- 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*} diff -r 13b97824aec6 -r 6214816d79d3 src/HOL/Auth/Guard/Proto.thy --- 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*}