standardized headers;
authorwenzelm
Fri Feb 18 16:07:32 2011 +0100 (2011-02-18)
changeset 417756214816d79d3
parent 41774 13b97824aec6
child 41776 3bd83302a3c3
standardized headers;
src/HOL/Auth/Guard/Analz.thy
src/HOL/Auth/Guard/Extensions.thy
src/HOL/Auth/Guard/Guard.thy
src/HOL/Auth/Guard/GuardK.thy
src/HOL/Auth/Guard/Guard_NS_Public.thy
src/HOL/Auth/Guard/Guard_OtwayRees.thy
src/HOL/Auth/Guard/Guard_Public.thy
src/HOL/Auth/Guard/Guard_Shared.thy
src/HOL/Auth/Guard/Guard_Yahalom.thy
src/HOL/Auth/Guard/List_Msg.thy
src/HOL/Auth/Guard/P1.thy
src/HOL/Auth/Guard/P2.thy
src/HOL/Auth/Guard/Proto.thy
     1.1 --- a/src/HOL/Auth/Guard/Analz.thy	Fri Feb 18 15:46:13 2011 +0100
     1.2 +++ b/src/HOL/Auth/Guard/Analz.thy	Fri Feb 18 16:07:32 2011 +0100
     1.3 @@ -1,13 +1,7 @@
     1.4 -(******************************************************************************
     1.5 -date: december 2001
     1.6 -author: Frederic Blanqui
     1.7 -email: blanqui@lri.fr
     1.8 -webpage: http://www.lri.fr/~blanqui/
     1.9 -
    1.10 -University of Cambridge, Computer Laboratory
    1.11 -William Gates Building, JJ Thomson Avenue
    1.12 -Cambridge CB3 0FD, United Kingdom
    1.13 -******************************************************************************)
    1.14 +(*  Title:      HOL/Auth/Guard/Analz.thy
    1.15 +    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
    1.16 +    Copyright   2001  University of Cambridge
    1.17 +*)
    1.18  
    1.19  header{*Decomposition of Analz into two parts*}
    1.20  
     2.1 --- a/src/HOL/Auth/Guard/Extensions.thy	Fri Feb 18 15:46:13 2011 +0100
     2.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Fri Feb 18 16:07:32 2011 +0100
     2.3 @@ -1,13 +1,7 @@
     2.4 -(******************************************************************************
     2.5 -date: november 2001
     2.6 -author: Frederic Blanqui
     2.7 -email: blanqui@lri.fr
     2.8 -webpage: http://www.lri.fr/~blanqui/
     2.9 -
    2.10 -University of Cambridge, Computer Laboratory
    2.11 -William Gates Building, JJ Thomson Avenue
    2.12 -Cambridge CB3 0FD, United Kingdom
    2.13 -******************************************************************************)
    2.14 +(*  Title:      HOL/Auth/Guard/Extensions.thy
    2.15 +    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
    2.16 +    Copyright   2001  University of Cambridge
    2.17 +*)
    2.18  
    2.19  header {*Extensions to Standard Theories*}
    2.20  
     3.1 --- a/src/HOL/Auth/Guard/Guard.thy	Fri Feb 18 15:46:13 2011 +0100
     3.2 +++ b/src/HOL/Auth/Guard/Guard.thy	Fri Feb 18 16:07:32 2011 +0100
     3.3 @@ -1,13 +1,7 @@
     3.4 -(******************************************************************************
     3.5 -date: january 2002
     3.6 -author: Frederic Blanqui
     3.7 -email: blanqui@lri.fr
     3.8 -webpage: http://www.lri.fr/~blanqui/
     3.9 -
    3.10 -University of Cambridge, Computer Laboratory
    3.11 -William Gates Building, JJ Thomson Avenue
    3.12 -Cambridge CB3 0FD, United Kingdom
    3.13 -******************************************************************************)
    3.14 +(*  Title:      HOL/Auth/Guard/Guard.thy
    3.15 +    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
    3.16 +    Copyright   2002  University of Cambridge
    3.17 +*)
    3.18  
    3.19  header{*Protocol-Independent Confidentiality Theorem on Nonces*}
    3.20  
     4.1 --- a/src/HOL/Auth/Guard/GuardK.thy	Fri Feb 18 15:46:13 2011 +0100
     4.2 +++ b/src/HOL/Auth/Guard/GuardK.thy	Fri Feb 18 16:07:32 2011 +0100
     4.3 @@ -1,18 +1,12 @@
     4.4 -(******************************************************************************
     4.5 -very similar to Guard except:
     4.6 +(*  Title:      HOL/Auth/Guard/GuardK.thy
     4.7 +    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
     4.8 +    Copyright   2002  University of Cambridge
     4.9 +
    4.10 +Very similar to Guard except:
    4.11  - Guard is replaced by GuardK, guard by guardK, Nonce by Key
    4.12  - some scripts are slightly modified (+ keyset_in, kparts_parts)
    4.13  - the hypothesis Key n ~:G (keyset G) is added
    4.14 -
    4.15 -date: march 2002
    4.16 -author: Frederic Blanqui
    4.17 -email: blanqui@lri.fr
    4.18 -webpage: http://www.lri.fr/~blanqui/
    4.19 -
    4.20 -University of Cambridge, Computer Laboratory
    4.21 -William Gates Building, JJ Thomson Avenue
    4.22 -Cambridge CB3 0FD, United Kingdom
    4.23 -******************************************************************************)
    4.24 +*)
    4.25  
    4.26  header{*protocol-independent confidentiality theorem on keys*}
    4.27  
     5.1 --- a/src/HOL/Auth/Guard/Guard_NS_Public.thy	Fri Feb 18 15:46:13 2011 +0100
     5.2 +++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy	Fri Feb 18 16:07:32 2011 +0100
     5.3 @@ -1,15 +1,9 @@
     5.4 -(******************************************************************************
     5.5 -incorporating Lowe's fix (inclusion of B's identity in round 2)
     5.6 +(*  Title:      HOL/Auth/Guard/Guard_NS_Public.thy
     5.7 +    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
     5.8 +    Copyright   2002  University of Cambridge
     5.9  
    5.10 -date: march 2002
    5.11 -author: Frederic Blanqui
    5.12 -email: blanqui@lri.fr
    5.13 -webpage: http://www.lri.fr/~blanqui/
    5.14 -
    5.15 -University of Cambridge, Computer Laboratory
    5.16 -William Gates Building, JJ Thomson Avenue
    5.17 -Cambridge CB3 0FD, United Kingdom
    5.18 -******************************************************************************)
    5.19 +Incorporating Lowe's fix (inclusion of B's identity in round 2).
    5.20 +*)
    5.21  
    5.22  header{*Needham-Schroeder-Lowe Public-Key Protocol*}
    5.23  
     6.1 --- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Fri Feb 18 15:46:13 2011 +0100
     6.2 +++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Fri Feb 18 16:07:32 2011 +0100
     6.3 @@ -1,13 +1,7 @@
     6.4 -(******************************************************************************
     6.5 -date: march 2002
     6.6 -author: Frederic Blanqui
     6.7 -email: blanqui@lri.fr
     6.8 -webpage: http://www.lri.fr/~blanqui/
     6.9 -
    6.10 -University of Cambridge, Computer Laboratory
    6.11 -William Gates Building, JJ Thomson Avenue
    6.12 -Cambridge CB3 0FD, United Kingdom
    6.13 -******************************************************************************)
    6.14 +(*  Title:      HOL/Auth/Guard/Guard_OtwayRees.thy
    6.15 +    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
    6.16 +    Copyright   2002  University of Cambridge
    6.17 +*)
    6.18  
    6.19  header{*Otway-Rees Protocol*}
    6.20  
     7.1 --- a/src/HOL/Auth/Guard/Guard_Public.thy	Fri Feb 18 15:46:13 2011 +0100
     7.2 +++ b/src/HOL/Auth/Guard/Guard_Public.thy	Fri Feb 18 16:07:32 2011 +0100
     7.3 @@ -1,15 +1,9 @@
     7.4 -(******************************************************************************
     7.5 -lemmas on guarded messages for public protocols
     7.6 +(*  Title:      HOL/Auth/Guard/Guard_Public.thy
     7.7 +    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
     7.8 +    Copyright   2002  University of Cambridge
     7.9  
    7.10 -date: march 2002
    7.11 -author: Frederic Blanqui
    7.12 -email: blanqui@lri.fr
    7.13 -webpage: http://www.lri.fr/~blanqui/
    7.14 -
    7.15 -University of Cambridge, Computer Laboratory
    7.16 -William Gates Building, JJ Thomson Avenue
    7.17 -Cambridge CB3 0FD, United Kingdom
    7.18 -******************************************************************************)
    7.19 +Lemmas on guarded messages for public protocols.
    7.20 +*)
    7.21  
    7.22  theory Guard_Public imports Guard Public Extensions begin
    7.23  
     8.1 --- a/src/HOL/Auth/Guard/Guard_Shared.thy	Fri Feb 18 15:46:13 2011 +0100
     8.2 +++ b/src/HOL/Auth/Guard/Guard_Shared.thy	Fri Feb 18 16:07:32 2011 +0100
     8.3 @@ -1,13 +1,7 @@
     8.4 -(******************************************************************************
     8.5 -date: march 2002
     8.6 -author: Frederic Blanqui
     8.7 -email: blanqui@lri.fr
     8.8 -webpage: http://www.lri.fr/~blanqui/
     8.9 -
    8.10 -University of Cambridge, Computer Laboratory
    8.11 -William Gates Building, JJ Thomson Avenue
    8.12 -Cambridge CB3 0FD, United Kingdom
    8.13 -******************************************************************************)
    8.14 +(*  Title:      HOL/Auth/Guard/Guard_Shared.thy
    8.15 +    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
    8.16 +    Copyright   2002  University of Cambridge
    8.17 +*)
    8.18  
    8.19  header{*lemmas on guarded messages for protocols with symmetric keys*}
    8.20  
     9.1 --- a/src/HOL/Auth/Guard/Guard_Yahalom.thy	Fri Feb 18 15:46:13 2011 +0100
     9.2 +++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy	Fri Feb 18 16:07:32 2011 +0100
     9.3 @@ -1,13 +1,7 @@
     9.4 -(******************************************************************************
     9.5 -date: march 2002
     9.6 -author: Frederic Blanqui
     9.7 -email: blanqui@lri.fr
     9.8 -webpage: http://www.lri.fr/~blanqui/
     9.9 -
    9.10 -University of Cambridge, Computer Laboratory
    9.11 -William Gates Building, JJ Thomson Avenue
    9.12 -Cambridge CB3 0FD, United Kingdom
    9.13 -******************************************************************************)
    9.14 +(*  Title:      HOL/Auth/Guard/Guard_Yahalom.thy
    9.15 +    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
    9.16 +    Copyright   2002  University of Cambridge
    9.17 +*)
    9.18  
    9.19  header{*Yahalom Protocol*}
    9.20  
    10.1 --- a/src/HOL/Auth/Guard/List_Msg.thy	Fri Feb 18 15:46:13 2011 +0100
    10.2 +++ b/src/HOL/Auth/Guard/List_Msg.thy	Fri Feb 18 16:07:32 2011 +0100
    10.3 @@ -1,13 +1,7 @@
    10.4 -(******************************************************************************
    10.5 -date: november 2001
    10.6 -author: Frederic Blanqui
    10.7 -email: blanqui@lri.fr
    10.8 -webpage: http://www.lri.fr/~blanqui/
    10.9 -
   10.10 -University of Cambridge, Computer Laboratory
   10.11 -William Gates Building, JJ Thomson Avenue
   10.12 -Cambridge CB3 0FD, United Kingdom
   10.13 -******************************************************************************)
   10.14 +(*  Title:      HOL/Auth/Guard/List_Msg.thy
   10.15 +    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
   10.16 +    Copyright   2001  University of Cambridge
   10.17 +*)
   10.18  
   10.19  header{*Lists of Messages and Lists of Agents*}
   10.20  
    11.1 --- a/src/HOL/Auth/Guard/P1.thy	Fri Feb 18 15:46:13 2011 +0100
    11.2 +++ b/src/HOL/Auth/Guard/P1.thy	Fri Feb 18 16:07:32 2011 +0100
    11.3 @@ -1,17 +1,11 @@
    11.4 -(******************************************************************************
    11.5 -from G. Karjoth, N. Asokan and C. Gulcu
    11.6 -"Protecting the computation results of free-roaming agents"
    11.7 -Mobiles Agents 1998, LNCS 1477
    11.8 +(*  Title:      HOL/Auth/Guard/P1.thy
    11.9 +    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
   11.10 +    Copyright   2002  University of Cambridge
   11.11  
   11.12 -date: february 2002
   11.13 -author: Frederic Blanqui
   11.14 -email: blanqui@lri.fr
   11.15 -webpage: http://www.lri.fr/~blanqui/
   11.16 -
   11.17 -University of Cambridge, Computer Laboratory
   11.18 -William Gates Building, JJ Thomson Avenue
   11.19 -Cambridge CB3 0FD, United Kingdom
   11.20 -******************************************************************************)
   11.21 +From G. Karjoth, N. Asokan and C. Gulcu
   11.22 +"Protecting the computation results of free-roaming agents"
   11.23 +Mobiles Agents 1998, LNCS 1477.
   11.24 +*)
   11.25  
   11.26  header{*Protocol P1*}
   11.27  
    12.1 --- a/src/HOL/Auth/Guard/P2.thy	Fri Feb 18 15:46:13 2011 +0100
    12.2 +++ b/src/HOL/Auth/Guard/P2.thy	Fri Feb 18 16:07:32 2011 +0100
    12.3 @@ -1,17 +1,11 @@
    12.4 -(******************************************************************************
    12.5 -from G. Karjoth, N. Asokan and C. Gulcu
    12.6 -"Protecting the computation results of free-roaming agents"
    12.7 -Mobiles Agents 1998, LNCS 1477
    12.8 +(*  Title:      HOL/Auth/Guard/P2.thy
    12.9 +    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
   12.10 +    Copyright   2002  University of Cambridge
   12.11  
   12.12 -date: march 2002
   12.13 -author: Frederic Blanqui
   12.14 -email: blanqui@lri.fr
   12.15 -webpage: http://www.lri.fr/~blanqui/
   12.16 -
   12.17 -University of Cambridge, Computer Laboratory
   12.18 -William Gates Building, JJ Thomson Avenue
   12.19 -Cambridge CB3 0FD, United Kingdom
   12.20 -******************************************************************************)
   12.21 +From G. Karjoth, N. Asokan and C. Gulcu
   12.22 +"Protecting the computation results of free-roaming agents"
   12.23 +Mobiles Agents 1998, LNCS 1477.
   12.24 +*)
   12.25  
   12.26  header{*Protocol P2*}
   12.27  
    13.1 --- a/src/HOL/Auth/Guard/Proto.thy	Fri Feb 18 15:46:13 2011 +0100
    13.2 +++ b/src/HOL/Auth/Guard/Proto.thy	Fri Feb 18 16:07:32 2011 +0100
    13.3 @@ -1,13 +1,7 @@
    13.4 -(******************************************************************************
    13.5 -date: april 2002
    13.6 -author: Frederic Blanqui
    13.7 -email: blanqui@lri.fr
    13.8 -webpage: http://www.lri.fr/~blanqui/
    13.9 -
   13.10 -University of Cambridge, Computer Laboratory
   13.11 -William Gates Building, JJ Thomson Avenue
   13.12 -Cambridge CB3 0FD, United Kingdom
   13.13 -******************************************************************************)
   13.14 +(*  Title:      HOL/Auth/Guard/Proto.thy
   13.15 +    Author:     Frederic Blanqui, University of Cambridge Computer Laboratory
   13.16 +    Copyright   2002  University of Cambridge
   13.17 +*)
   13.18  
   13.19  header{*Other Protocol-Independent Results*}
   13.20