merged
authorhaftmann
Mon Sep 21 16:11:36 2009 +0200 (2009-09-21)
changeset 32637827cac8abecc
parent 32628 72b93132fc31
parent 32636 55a0be42327c
child 32639 a6909ef949aa
child 32642 026e7c6a6d08
merged
     1.1 --- a/Admin/isatest/isatest-stats	Mon Sep 21 16:07:20 2009 +0200
     1.2 +++ b/Admin/isatest/isatest-stats	Mon Sep 21 16:11:36 2009 +0200
     1.3 @@ -24,9 +24,9 @@
     1.4    HOL-MetisExamples \
     1.5    HOL-MicroJava \
     1.6    HOL-NSA \
     1.7 -  HOL-NewNumberTheory \
     1.8    HOL-Nominal-Examples \
     1.9 -  HOL-NumberTheory \
    1.10 +  HOL-Number_Theory \
    1.11 +  HOL-Old_Number_Theory \
    1.12    HOL-SET-Protocol \
    1.13    HOL-UNITY \
    1.14    HOL-Word \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Auth/All_Symmetric.thy	Mon Sep 21 16:11:36 2009 +0200
     2.3 @@ -0,0 +1,12 @@
     2.4 +theory All_Symmetric
     2.5 +imports Message
     2.6 +begin
     2.7 +
     2.8 +text {* All keys are symmetric *}
     2.9 +
    2.10 +defs all_symmetric_def: "all_symmetric \<equiv> True"
    2.11 +
    2.12 +lemma isSym_keys: "K \<in> symKeys"
    2.13 +  by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
    2.14 +
    2.15 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Auth/Auth_Public.thy	Mon Sep 21 16:11:36 2009 +0200
     3.3 @@ -0,0 +1,15 @@
     3.4 +(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.5 +    Copyright   1996  University of Cambridge
     3.6 +*)
     3.7 +
     3.8 +header {* Conventional protocols: rely on conventional Message, Event and Public -- Public-key protocols *}
     3.9 +
    3.10 +theory Auth_Public
    3.11 +imports
    3.12 +  "NS_Public_Bad"
    3.13 +  "NS_Public"
    3.14 +  "TLS"
    3.15 +  "CertifiedEmail"
    3.16 +begin
    3.17 +
    3.18 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Auth/Auth_Shared.thy	Mon Sep 21 16:11:36 2009 +0200
     4.3 @@ -0,0 +1,27 @@
     4.4 +(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.5 +    Copyright   1996  University of Cambridge
     4.6 +*)
     4.7 +
     4.8 +header {* Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols *}
     4.9 +
    4.10 +theory Auth_Shared
    4.11 +imports
    4.12 +  "NS_Shared"
    4.13 +  "Kerberos_BAN"
    4.14 +  "Kerberos_BAN_Gets"
    4.15 +  "KerberosIV"
    4.16 +  "KerberosIV_Gets"
    4.17 +  "KerberosV"
    4.18 +  "OtwayRees"
    4.19 +  "OtwayRees_AN"
    4.20 +  "OtwayRees_Bad"
    4.21 +  "OtwayReesBella"
    4.22 +  "WooLam"
    4.23 +  "Recur"
    4.24 +  "Yahalom"
    4.25 +  "Yahalom2"
    4.26 +  "Yahalom_Bad"
    4.27 +  "ZhouGollmann"
    4.28 +begin
    4.29 +
    4.30 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Auth/Guard/Auth_Guard_Public.thy	Mon Sep 21 16:11:36 2009 +0200
     5.3 @@ -0,0 +1,15 @@
     5.4 +(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.5 +    Copyright   1996  University of Cambridge
     5.6 +*)
     5.7 +
     5.8 +header {* Blanqui's "guard" concept: protocol-independent secrecy *}
     5.9 +
    5.10 +theory Auth_Guard_Public
    5.11 +imports
    5.12 +  "P1"
    5.13 +  "P2"
    5.14 +  "Guard_NS_Public"
    5.15 +  "Proto"
    5.16 +begin
    5.17 +
    5.18 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Auth/Guard/Auth_Guard_Shared.thy	Mon Sep 21 16:11:36 2009 +0200
     6.3 @@ -0,0 +1,13 @@
     6.4 +(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.5 +    Copyright   1996  University of Cambridge
     6.6 +*)
     6.7 +
     6.8 +header {* Blanqui's "guard" concept: protocol-independent secrecy *}
     6.9 +
    6.10 +theory Auth_Guard_Shared
    6.11 +imports
    6.12 +  "Guard_OtwayRees"
    6.13 +  "Guard_Yahalom"
    6.14 +begin
    6.15 +
    6.16 +end
     7.1 --- a/src/HOL/Auth/Public.thy	Mon Sep 21 16:07:20 2009 +0200
     7.2 +++ b/src/HOL/Auth/Public.thy	Mon Sep 21 16:11:36 2009 +0200
     7.3 @@ -1,5 +1,4 @@
     7.4  (*  Title:      HOL/Auth/Public
     7.5 -    ID:         $Id$
     7.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7      Copyright   1996  University of Cambridge
     7.8  
     7.9 @@ -8,7 +7,9 @@
    7.10  Private and public keys; initial states of agents
    7.11  *)
    7.12  
    7.13 -theory Public imports Event begin
    7.14 +theory Public
    7.15 +imports Event
    7.16 +begin
    7.17  
    7.18  lemma invKey_K: "K \<in> symKeys ==> invKey K = K"
    7.19  by (simp add: symKeys_def)
     8.1 --- a/src/HOL/Auth/ROOT.ML	Mon Sep 21 16:07:20 2009 +0200
     8.2 +++ b/src/HOL/Auth/ROOT.ML	Mon Sep 21 16:11:36 2009 +0200
     8.3 @@ -1,51 +1,2 @@
     8.4 -(*  Title:      HOL/Auth/ROOT.ML
     8.5 -    ID:         $Id$
     8.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 -    Copyright   1996  University of Cambridge
     8.8  
     8.9 -Root file for protocol proofs.
    8.10 -*)
    8.11 -
    8.12 -use_thys [
    8.13 -
    8.14 -(* Conventional protocols: rely on 
    8.15 -   conventional Message, Event and Public *)
    8.16 -
    8.17 -(*Shared-key protocols*)
    8.18 -  "NS_Shared",
    8.19 -  "Kerberos_BAN",
    8.20 -  "Kerberos_BAN_Gets",
    8.21 -  "KerberosIV",
    8.22 -  "KerberosIV_Gets",
    8.23 -  "KerberosV",
    8.24 -  "OtwayRees",
    8.25 -  "OtwayRees_AN",
    8.26 -  "OtwayRees_Bad",
    8.27 -  "OtwayReesBella",
    8.28 -  "WooLam",
    8.29 -  "Recur",
    8.30 -  "Yahalom",
    8.31 -  "Yahalom2",
    8.32 -  "Yahalom_Bad",
    8.33 -  "ZhouGollmann",
    8.34 -
    8.35 -(*Public-key protocols*)
    8.36 -  "NS_Public_Bad",
    8.37 -  "NS_Public",
    8.38 -  "TLS",
    8.39 -  "CertifiedEmail",
    8.40 -
    8.41 -(*Smartcard protocols: rely on conventional Message and on new
    8.42 -  EventSC and Smartcard *)
    8.43 -
    8.44 -  "Smartcard/ShoupRubin",
    8.45 -  "Smartcard/ShoupRubinBella",
    8.46 -
    8.47 -(*Blanqui's "guard" concept: protocol-independent secrecy*)
    8.48 -  "Guard/P1",
    8.49 -  "Guard/P2",
    8.50 -  "Guard/Guard_NS_Public",
    8.51 -  "Guard/Guard_OtwayRees",
    8.52 -  "Guard/Guard_Yahalom",
    8.53 -  "Guard/Proto"
    8.54 -];
    8.55 +use_thys ["Auth_Shared", "Auth_Public", "Smartcard/Auth_Smartcard", "Guard/Auth_Guard_Shared", "Guard/Auth_Guard_Public"];
     9.1 --- a/src/HOL/Auth/Shared.thy	Mon Sep 21 16:07:20 2009 +0200
     9.2 +++ b/src/HOL/Auth/Shared.thy	Mon Sep 21 16:11:36 2009 +0200
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      HOL/Auth/Shared
     9.5 -    ID:         $Id$
     9.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7      Copyright   1996  University of Cambridge
     9.8  
     9.9 @@ -8,7 +7,9 @@
    9.10  Shared, long-term keys; initial states of agents
    9.11  *)
    9.12  
    9.13 -theory Shared imports Event begin
    9.14 +theory Shared
    9.15 +imports Event All_Symmetric
    9.16 +begin
    9.17  
    9.18  consts
    9.19    shrK    :: "agent => key"  (*symmetric keys*);
    9.20 @@ -20,13 +21,6 @@
    9.21     apply (simp add: inj_on_def split: agent.split) 
    9.22     done
    9.23  
    9.24 -text{*All keys are symmetric*}
    9.25 -
    9.26 -defs  all_symmetric_def: "all_symmetric == True"
    9.27 -
    9.28 -lemma isSym_keys: "K \<in> symKeys"	
    9.29 -by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
    9.30 -
    9.31  text{*Server knows all long-term keys; other agents know only their own*}
    9.32  primrec
    9.33    initState_Server:  "initState Server     = Key ` range shrK"
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Auth/Smartcard/Auth_Smartcard.thy	Mon Sep 21 16:11:36 2009 +0200
    10.3 @@ -0,0 +1,13 @@
    10.4 +(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.5 +    Copyright   1996  University of Cambridge
    10.6 +*)
    10.7 +
    10.8 +header {* Smartcard protocols: rely on conventional Message and on new EventSC and Smartcard *}
    10.9 +
   10.10 +theory Auth_Smartcard
   10.11 +imports
   10.12 +  "ShoupRubin"
   10.13 +  "ShoupRubinBella"
   10.14 +begin
   10.15 +
   10.16 +end
    11.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Mon Sep 21 16:07:20 2009 +0200
    11.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Mon Sep 21 16:11:36 2009 +0200
    11.3 @@ -1,10 +1,11 @@
    11.4 -(*  ID:         $Id$
    11.5 -    Author:     Giampaolo Bella, Catania University
    11.6 +(* Author:     Giampaolo Bella, Catania University
    11.7  *)
    11.8  
    11.9  header{*Theory of smartcards*}
   11.10  
   11.11 -theory Smartcard imports EventSC begin
   11.12 +theory Smartcard
   11.13 +imports EventSC All_Symmetric
   11.14 +begin
   11.15  
   11.16  text{*  
   11.17  As smartcards handle long-term (symmetric) keys, this theoy extends and 
   11.18 @@ -42,14 +43,6 @@
   11.19    shrK_disj_pin [iff]:  "shrK P \<noteq> pin Q"
   11.20    crdK_disj_pin [iff]:   "crdK C \<noteq> pin P"
   11.21  
   11.22 -
   11.23 -text{*All keys are symmetric*}
   11.24 -defs  all_symmetric_def: "all_symmetric == True"
   11.25 -
   11.26 -lemma isSym_keys: "K \<in> symKeys"	
   11.27 -by (simp add: symKeys_def all_symmetric_def invKey_symmetric) 
   11.28 -
   11.29 -
   11.30  constdefs
   11.31    legalUse :: "card => bool" ("legalUse (_)")
   11.32    "legalUse C == C \<notin> stolen"
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Bali/Bali.thy	Mon Sep 21 16:11:36 2009 +0200
    12.3 @@ -0,0 +1,11 @@
    12.4 +(*  Author:     David von Oheimb
    12.5 +    Copyright   1999 Technische Universitaet Muenchen
    12.6 +*)
    12.7 +
    12.8 +header {* The Hoare logic for Bali. *}
    12.9 +
   12.10 +theory Bali
   12.11 +imports AxExample AxSound AxCompl Trans
   12.12 +begin
   12.13 +
   12.14 +end
    13.1 --- a/src/HOL/Bali/ROOT.ML	Mon Sep 21 16:07:20 2009 +0200
    13.2 +++ b/src/HOL/Bali/ROOT.ML	Mon Sep 21 16:11:36 2009 +0200
    13.3 @@ -1,9 +1,2 @@
    13.4 -(*  Title:      HOL/Bali/ROOT.ML
    13.5 -    ID:         $Id$
    13.6 -    Author:     David von Oheimb
    13.7 -    Copyright   1999 Technische Universitaet Muenchen
    13.8  
    13.9 -The Hoare logic for Bali.
   13.10 -*)
   13.11 -
   13.12 -use_thys ["AxExample", "AxSound", "AxCompl", "Trans"];
   13.13 +use_thy "Bali"
    14.1 --- a/src/HOL/IsaMakefile	Mon Sep 21 16:07:20 2009 +0200
    14.2 +++ b/src/HOL/IsaMakefile	Mon Sep 21 16:11:36 2009 +0200
    14.3 @@ -619,6 +619,10 @@
    14.4  HOL-Auth: HOL $(LOG)/HOL-Auth.gz
    14.5  
    14.6  $(LOG)/HOL-Auth.gz: $(OUT)/HOL 						\
    14.7 +  Auth/Auth_Shared.thy Auth/Auth_Public.thy Auth/All_Symmetric.thy		\
    14.8 +  Auth/Guard/Auth_Guard_Shared.thy		\
    14.9 +  Auth/Guard/Auth_Guard_Public.thy		\
   14.10 +  Auth/Smartcard/Auth_Smartcard.thy Auth/All_Symmetric.thy		\
   14.11    Auth/CertifiedEmail.thy Auth/Event.thy Auth/Message.thy		\
   14.12    Auth/NS_Public.thy Auth/NS_Public_Bad.thy Auth/NS_Shared.thy		\
   14.13    Auth/OtwayRees.thy Auth/OtwayReesBella.thy Auth/OtwayRees_AN.thy	\
   14.14 @@ -832,7 +836,7 @@
   14.15  
   14.16  HOL-Bali: HOL $(LOG)/HOL-Bali.gz
   14.17  
   14.18 -$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/AxCompl.thy Bali/AxExample.thy	\
   14.19 +$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/Bali.thy Bali/AxCompl.thy Bali/AxExample.thy	\
   14.20    Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy	\
   14.21    Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy	\
   14.22    Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy		\
   14.23 @@ -1022,6 +1026,7 @@
   14.24  HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz
   14.25  
   14.26  $(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal 	\
   14.27 +  Nominal/Examples/Nominal_Examples.thy \
   14.28    Nominal/Examples/CK_Machine.thy \
   14.29    Nominal/Examples/CR.thy \
   14.30    Nominal/Examples/CR_Takahashi.thy \
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Nominal/Examples/Nominal_Examples.thy	Mon Sep 21 16:11:36 2009 +0200
    15.3 @@ -0,0 +1,25 @@
    15.4 +(*  Author:  Christian Urban TU Muenchen *)
    15.5 +
    15.6 +header {* Various examples involving nominal datatypes. *}
    15.7 +
    15.8 +theory Nominal_Examples
    15.9 +imports
   15.10 +  CR
   15.11 +  CR_Takahashi
   15.12 +  Class
   15.13 +  Compile
   15.14 +  Fsub
   15.15 +  Height
   15.16 +  Lambda_mu
   15.17 +  SN
   15.18 +  Weakening
   15.19 +  Crary
   15.20 +  SOS
   15.21 +  LocalWeakening
   15.22 +  Support
   15.23 +  Contexts
   15.24 +  Standardization
   15.25 +  W
   15.26 +begin
   15.27 +
   15.28 +end
    16.1 --- a/src/HOL/Nominal/Examples/ROOT.ML	Mon Sep 21 16:07:20 2009 +0200
    16.2 +++ b/src/HOL/Nominal/Examples/ROOT.ML	Mon Sep 21 16:11:36 2009 +0200
    16.3 @@ -1,27 +1,4 @@
    16.4 -(*  Title:      HOL/Nominal/Examples/ROOT.ML
    16.5 -    ID:         $Id$
    16.6 -    Author:     Christian Urban, TU Muenchen
    16.7 -
    16.8 -Various examples involving nominal datatypes.
    16.9 -*)
   16.10  
   16.11 -use_thys [
   16.12 -  "CR",
   16.13 -  "CR_Takahashi",
   16.14 -  "Class",
   16.15 -  "Compile",
   16.16 -  "Fsub",
   16.17 -  "Height",
   16.18 -  "Lambda_mu",
   16.19 -  "SN",
   16.20 -  "Weakening",
   16.21 -  "Crary",
   16.22 -  "SOS",
   16.23 -  "LocalWeakening",
   16.24 -  "Support",
   16.25 -  "Contexts",
   16.26 -  "Standardization",
   16.27 -  "W"
   16.28 -];
   16.29 +use_thy "Nominal_Examples";
   16.30  
   16.31 -setmp_noncritical quick_and_dirty true use_thy "VC_Condition";
   16.32 +setmp_noncritical quick_and_dirty true use_thy "VC_Condition"; (*FIXME*)
    17.1 --- a/src/HOL/UNITY/Simple/Common.thy	Mon Sep 21 16:07:20 2009 +0200
    17.2 +++ b/src/HOL/UNITY/Simple/Common.thy	Mon Sep 21 16:11:36 2009 +0200
    17.3 @@ -83,19 +83,24 @@
    17.4  
    17.5  (*** Progress under weak fairness ***)
    17.6  
    17.7 -declare atMost_Int_atLeast [simp]
    17.8 -
    17.9  lemma leadsTo_common_lemma:
   17.10 -     "[| \<forall>m. F \<in> {m} Co (maxfg m);  
   17.11 -         \<forall>m \<in> lessThan n. F \<in> {m} LeadsTo (greaterThan m);  
   17.12 -         n \<in> common |]   
   17.13 -      ==> F \<in> (atMost n) LeadsTo common"
   17.14 -apply (rule LeadsTo_weaken_R)
   17.15 -apply (rule_tac f = id and l = n in GreaterThan_bounded_induct)
   17.16 -apply (simp_all (no_asm_simp) del: Int_insert_right_if1)
   17.17 -apply (rule_tac [2] subset_refl)
   17.18 -apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
   17.19 -done
   17.20 +  assumes "\<forall>m. F \<in> {m} Co (maxfg m)"
   17.21 +    and "\<forall>m \<in> lessThan n. F \<in> {m} LeadsTo (greaterThan m)"
   17.22 +    and "n \<in> common"
   17.23 +  shows "F \<in> (atMost n) LeadsTo common"
   17.24 +proof (rule LeadsTo_weaken_R)
   17.25 +  show "F \<in> {..n} LeadsTo {..n} \<inter> id -` {n..} \<union> common"
   17.26 +  proof (induct rule: GreaterThan_bounded_induct [of n _ _ id])
   17.27 +    case 1
   17.28 +    from assms have "\<forall>m\<in>{..<n}. F \<in> {..n} \<inter> {m} LeadsTo {..n} \<inter> {m<..} \<union> common"
   17.29 +      by (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R)
   17.30 +    then show ?case by simp
   17.31 +  qed
   17.32 +next
   17.33 +  from `n \<in> common`
   17.34 +  show "{..n} \<inter> id -` {n..} \<union> common \<subseteq> common"
   17.35 +    by (simp add: atMost_Int_atLeast)
   17.36 +qed
   17.37  
   17.38  (*The "\<forall>m \<in> -common" form echoes CMT6.*)
   17.39  lemma leadsTo_common: