# HG changeset patch # User haftmann # Date 1253542296 -7200 # Node ID 827cac8abeccb65b991e7842b52f3efac1f08cbf # Parent 72b93132fc3124a1918c7727d1ada5e57a53f6f3# Parent 55a0be42327c5c281ba9acc2aa0a7bb9dbddae66 merged diff -r 72b93132fc31 -r 827cac8abecc Admin/isatest/isatest-stats --- a/Admin/isatest/isatest-stats Mon Sep 21 16:07:20 2009 +0200 +++ b/Admin/isatest/isatest-stats Mon Sep 21 16:11:36 2009 +0200 @@ -24,9 +24,9 @@ HOL-MetisExamples \ HOL-MicroJava \ HOL-NSA \ - HOL-NewNumberTheory \ HOL-Nominal-Examples \ - HOL-NumberTheory \ + HOL-Number_Theory \ + HOL-Old_Number_Theory \ HOL-SET-Protocol \ HOL-UNITY \ HOL-Word \ diff -r 72b93132fc31 -r 827cac8abecc src/HOL/Auth/All_Symmetric.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/All_Symmetric.thy Mon Sep 21 16:11:36 2009 +0200 @@ -0,0 +1,12 @@ +theory All_Symmetric +imports Message +begin + +text {* All keys are symmetric *} + +defs all_symmetric_def: "all_symmetric \ True" + +lemma isSym_keys: "K \ symKeys" + by (simp add: symKeys_def all_symmetric_def invKey_symmetric) + +end diff -r 72b93132fc31 -r 827cac8abecc 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 16:11:36 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 72b93132fc31 -r 827cac8abecc 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 16:11:36 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 72b93132fc31 -r 827cac8abecc 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 16:11:36 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 72b93132fc31 -r 827cac8abecc 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 16:11:36 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 72b93132fc31 -r 827cac8abecc src/HOL/Auth/Public.thy --- a/src/HOL/Auth/Public.thy Mon Sep 21 16:07:20 2009 +0200 +++ b/src/HOL/Auth/Public.thy Mon Sep 21 16:11:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Auth/Public - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge @@ -8,7 +7,9 @@ Private and public keys; initial states of agents *) -theory Public imports Event begin +theory Public +imports Event +begin lemma invKey_K: "K \ symKeys ==> invKey K = K" by (simp add: symKeys_def) diff -r 72b93132fc31 -r 827cac8abecc src/HOL/Auth/ROOT.ML --- a/src/HOL/Auth/ROOT.ML Mon Sep 21 16:07:20 2009 +0200 +++ b/src/HOL/Auth/ROOT.ML Mon Sep 21 16:11:36 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 72b93132fc31 -r 827cac8abecc src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Mon Sep 21 16:07:20 2009 +0200 +++ b/src/HOL/Auth/Shared.thy Mon Sep 21 16:11:36 2009 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Auth/Shared - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge @@ -8,7 +7,9 @@ Shared, long-term keys; initial states of agents *) -theory Shared imports Event begin +theory Shared +imports Event All_Symmetric +begin consts shrK :: "agent => key" (*symmetric keys*); @@ -20,13 +21,6 @@ apply (simp add: inj_on_def split: agent.split) done -text{*All keys are symmetric*} - -defs all_symmetric_def: "all_symmetric == True" - -lemma isSym_keys: "K \ symKeys" -by (simp add: symKeys_def all_symmetric_def invKey_symmetric) - text{*Server knows all long-term keys; other agents know only their own*} primrec initState_Server: "initState Server = Key ` range shrK" diff -r 72b93132fc31 -r 827cac8abecc 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 16:11:36 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 72b93132fc31 -r 827cac8abecc src/HOL/Auth/Smartcard/Smartcard.thy --- a/src/HOL/Auth/Smartcard/Smartcard.thy Mon Sep 21 16:07:20 2009 +0200 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy Mon Sep 21 16:11:36 2009 +0200 @@ -1,10 +1,11 @@ -(* ID: $Id$ - Author: Giampaolo Bella, Catania University +(* Author: Giampaolo Bella, Catania University *) header{*Theory of smartcards*} -theory Smartcard imports EventSC begin +theory Smartcard +imports EventSC All_Symmetric +begin text{* As smartcards handle long-term (symmetric) keys, this theoy extends and @@ -42,14 +43,6 @@ shrK_disj_pin [iff]: "shrK P \ pin Q" crdK_disj_pin [iff]: "crdK C \ pin P" - -text{*All keys are symmetric*} -defs all_symmetric_def: "all_symmetric == True" - -lemma isSym_keys: "K \ symKeys" -by (simp add: symKeys_def all_symmetric_def invKey_symmetric) - - constdefs legalUse :: "card => bool" ("legalUse (_)") "legalUse C == C \ stolen" diff -r 72b93132fc31 -r 827cac8abecc src/HOL/Bali/Bali.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Bali/Bali.thy Mon Sep 21 16:11:36 2009 +0200 @@ -0,0 +1,11 @@ +(* Author: David von Oheimb + Copyright 1999 Technische Universitaet Muenchen +*) + +header {* The Hoare logic for Bali. *} + +theory Bali +imports AxExample AxSound AxCompl Trans +begin + +end diff -r 72b93132fc31 -r 827cac8abecc src/HOL/Bali/ROOT.ML --- a/src/HOL/Bali/ROOT.ML Mon Sep 21 16:07:20 2009 +0200 +++ b/src/HOL/Bali/ROOT.ML Mon Sep 21 16:11:36 2009 +0200 @@ -1,9 +1,2 @@ -(* Title: HOL/Bali/ROOT.ML - ID: $Id$ - Author: David von Oheimb - Copyright 1999 Technische Universitaet Muenchen -The Hoare logic for Bali. -*) - -use_thys ["AxExample", "AxSound", "AxCompl", "Trans"]; +use_thy "Bali" diff -r 72b93132fc31 -r 827cac8abecc src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Sep 21 16:07:20 2009 +0200 +++ b/src/HOL/IsaMakefile Mon Sep 21 16:11:36 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 \ @@ -832,7 +836,7 @@ HOL-Bali: HOL $(LOG)/HOL-Bali.gz -$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/AxCompl.thy Bali/AxExample.thy \ +$(LOG)/HOL-Bali.gz: $(OUT)/HOL Bali/Bali.thy Bali/AxCompl.thy Bali/AxExample.thy \ Bali/AxSem.thy Bali/AxSound.thy Bali/Basis.thy Bali/Conform.thy \ Bali/Decl.thy Bali/DeclConcepts.thy Bali/Eval.thy Bali/Evaln.thy \ Bali/Example.thy Bali/Name.thy Bali/ROOT.ML Bali/State.thy \ @@ -1022,6 +1026,7 @@ HOL-Nominal-Examples: HOL-Nominal $(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal-Examples.gz: $(OUT)/HOL-Nominal \ + Nominal/Examples/Nominal_Examples.thy \ Nominal/Examples/CK_Machine.thy \ Nominal/Examples/CR.thy \ Nominal/Examples/CR_Takahashi.thy \ diff -r 72b93132fc31 -r 827cac8abecc src/HOL/Nominal/Examples/Nominal_Examples.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nominal/Examples/Nominal_Examples.thy Mon Sep 21 16:11:36 2009 +0200 @@ -0,0 +1,25 @@ +(* Author: Christian Urban TU Muenchen *) + +header {* Various examples involving nominal datatypes. *} + +theory Nominal_Examples +imports + CR + CR_Takahashi + Class + Compile + Fsub + Height + Lambda_mu + SN + Weakening + Crary + SOS + LocalWeakening + Support + Contexts + Standardization + W +begin + +end diff -r 72b93132fc31 -r 827cac8abecc src/HOL/Nominal/Examples/ROOT.ML --- a/src/HOL/Nominal/Examples/ROOT.ML Mon Sep 21 16:07:20 2009 +0200 +++ b/src/HOL/Nominal/Examples/ROOT.ML Mon Sep 21 16:11:36 2009 +0200 @@ -1,27 +1,4 @@ -(* Title: HOL/Nominal/Examples/ROOT.ML - ID: $Id$ - Author: Christian Urban, TU Muenchen - -Various examples involving nominal datatypes. -*) -use_thys [ - "CR", - "CR_Takahashi", - "Class", - "Compile", - "Fsub", - "Height", - "Lambda_mu", - "SN", - "Weakening", - "Crary", - "SOS", - "LocalWeakening", - "Support", - "Contexts", - "Standardization", - "W" -]; +use_thy "Nominal_Examples"; -setmp_noncritical quick_and_dirty true use_thy "VC_Condition"; +setmp_noncritical quick_and_dirty true use_thy "VC_Condition"; (*FIXME*) diff -r 72b93132fc31 -r 827cac8abecc src/HOL/UNITY/Simple/Common.thy --- a/src/HOL/UNITY/Simple/Common.thy Mon Sep 21 16:07:20 2009 +0200 +++ b/src/HOL/UNITY/Simple/Common.thy Mon Sep 21 16:11:36 2009 +0200 @@ -83,19 +83,24 @@ (*** Progress under weak fairness ***) -declare atMost_Int_atLeast [simp] - lemma leadsTo_common_lemma: - "[| \m. F \ {m} Co (maxfg m); - \m \ lessThan n. F \ {m} LeadsTo (greaterThan m); - n \ common |] - ==> F \ (atMost n) LeadsTo common" -apply (rule LeadsTo_weaken_R) -apply (rule_tac f = id and l = n in GreaterThan_bounded_induct) -apply (simp_all (no_asm_simp) del: Int_insert_right_if1) -apply (rule_tac [2] subset_refl) -apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R) -done + assumes "\m. F \ {m} Co (maxfg m)" + and "\m \ lessThan n. F \ {m} LeadsTo (greaterThan m)" + and "n \ common" + shows "F \ (atMost n) LeadsTo common" +proof (rule LeadsTo_weaken_R) + show "F \ {..n} LeadsTo {..n} \ id -` {n..} \ common" + proof (induct rule: GreaterThan_bounded_induct [of n _ _ id]) + case 1 + from assms have "\m\{.. {..n} \ {m} LeadsTo {..n} \ {m<..} \ common" + by (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R) + then show ?case by simp + qed +next + from `n \ common` + show "{..n} \ id -` {n..} \ common \ common" + by (simp add: atMost_Int_atLeast) +qed (*The "\m \ -common" form echoes CMT6.*) lemma leadsTo_common: