renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
authorwenzelm
Wed Sep 14 23:14:57 2005 +0200 (2005-09-14)
changeset 17394a8c9ed3f9818
parent 17393 23b7e14ce640
child 17395 a05e20f6a31a
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
src/HOL/Auth/Guard/Guard_NS_Public.thy
src/HOL/Auth/Guard/Guard_OtwayRees.thy
src/HOL/Auth/Guard/Guard_Yahalom.thy
src/HOL/Auth/Guard/NS_Public.thy
src/HOL/Auth/Guard/OtwayRees.thy
src/HOL/Auth/Guard/Yahalom.thy
src/HOL/Auth/ROOT.ML
src/HOL/IsaMakefile
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy	Wed Sep 14 23:14:57 2005 +0200
     1.3 @@ -0,0 +1,204 @@
     1.4 +(******************************************************************************
     1.5 +incorporating Lowe's fix (inclusion of B's identity in round 2)
     1.6 +
     1.7 +date: march 2002
     1.8 +author: Frederic Blanqui
     1.9 +email: blanqui@lri.fr
    1.10 +webpage: http://www.lri.fr/~blanqui/
    1.11 +
    1.12 +University of Cambridge, Computer Laboratory
    1.13 +William Gates Building, JJ Thomson Avenue
    1.14 +Cambridge CB3 0FD, United Kingdom
    1.15 +******************************************************************************)
    1.16 +
    1.17 +header{*Needham-Schroeder-Lowe Public-Key Protocol*}
    1.18 +
    1.19 +theory Guard_NS_Public imports Guard_Public begin
    1.20 +
    1.21 +subsection{*messages used in the protocol*}
    1.22 +
    1.23 +syntax ns1 :: "agent => agent => nat => event"
    1.24 +
    1.25 +translations "ns1 A B NA" => "Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
    1.26 +
    1.27 +syntax ns1' :: "agent => agent => agent => nat => event"
    1.28 +
    1.29 +translations "ns1' A' A B NA"
    1.30 +=> "Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
    1.31 +
    1.32 +syntax ns2 :: "agent => agent => nat => nat => event"
    1.33 +
    1.34 +translations "ns2 B A NA NB"
    1.35 +=> "Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
    1.36 +
    1.37 +syntax ns2' :: "agent => agent => agent => nat => nat => event"
    1.38 +
    1.39 +translations "ns2' B' B A NA NB"
    1.40 +=> "Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
    1.41 +
    1.42 +syntax ns3 :: "agent => agent => nat => event"
    1.43 +
    1.44 +translations "ns3 A B NB" => "Says A B (Crypt (pubK B) (Nonce NB))"
    1.45 +
    1.46 +subsection{*definition of the protocol*}
    1.47 +
    1.48 +consts nsp :: "event list set"
    1.49 +
    1.50 +inductive nsp
    1.51 +intros
    1.52 +
    1.53 +Nil: "[]:nsp"
    1.54 +
    1.55 +Fake: "[| evs:nsp; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs : nsp"
    1.56 +
    1.57 +NS1: "[| evs1:nsp; Nonce NA ~:used evs1 |] ==> ns1 A B NA # evs1 : nsp"
    1.58 +
    1.59 +NS2: "[| evs2:nsp; Nonce NB ~:used evs2; ns1' A' A B NA:set evs2 |] ==>
    1.60 +ns2 B A NA NB # evs2:nsp"
    1.61 +
    1.62 +NS3: "[| evs3:nsp; ns1 A B NA:set evs3; ns2' B' B A NA NB:set evs3 |] ==>
    1.63 +ns3 A B NB # evs3:nsp"
    1.64 +
    1.65 +subsection{*declarations for tactics*}
    1.66 +
    1.67 +declare knows_Spy_partsEs [elim]
    1.68 +declare Fake_parts_insert [THEN subsetD, dest]
    1.69 +declare initState.simps [simp del]
    1.70 +
    1.71 +subsection{*general properties of nsp*}
    1.72 +
    1.73 +lemma nsp_has_no_Gets: "evs:nsp ==> ALL A X. Gets A X ~:set evs"
    1.74 +by (erule nsp.induct, auto)
    1.75 +
    1.76 +lemma nsp_is_Gets_correct [iff]: "Gets_correct nsp"
    1.77 +by (auto simp: Gets_correct_def dest: nsp_has_no_Gets)
    1.78 +
    1.79 +lemma nsp_is_one_step [iff]: "one_step nsp"
    1.80 +by (unfold one_step_def, clarify, ind_cases "ev#evs:nsp", auto)
    1.81 +
    1.82 +lemma nsp_has_only_Says' [rule_format]: "evs:nsp ==>
    1.83 +ev:set evs --> (EX A B X. ev=Says A B X)"
    1.84 +by (erule nsp.induct, auto)
    1.85 +
    1.86 +lemma nsp_has_only_Says [iff]: "has_only_Says nsp"
    1.87 +by (auto simp: has_only_Says_def dest: nsp_has_only_Says')
    1.88 +
    1.89 +lemma nsp_is_regular [iff]: "regular nsp"
    1.90 +apply (simp only: regular_def, clarify)
    1.91 +by (erule nsp.induct, auto simp: initState.simps knows.simps)
    1.92 +
    1.93 +subsection{*nonce are used only once*}
    1.94 +
    1.95 +lemma NA_is_uniq [rule_format]: "evs:nsp ==>
    1.96 +Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
    1.97 +--> Crypt (pubK B') {|Nonce NA, Agent A'|}:parts (spies evs)
    1.98 +--> Nonce NA ~:analz (spies evs) --> A=A' & B=B'"
    1.99 +apply (erule nsp.induct, simp_all)
   1.100 +by (blast intro: analz_insertI)+
   1.101 +
   1.102 +lemma no_Nonce_NS1_NS2 [rule_format]: "evs:nsp ==>
   1.103 +Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs)
   1.104 +--> Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
   1.105 +--> Nonce NA:analz (spies evs)"
   1.106 +apply (erule nsp.induct, simp_all)
   1.107 +by (blast intro: analz_insertI)+
   1.108 +
   1.109 +lemma no_Nonce_NS1_NS2' [rule_format]:
   1.110 +"[| Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs);
   1.111 +Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs); evs:nsp |]
   1.112 +==> Nonce NA:analz (spies evs)"
   1.113 +by (rule no_Nonce_NS1_NS2, auto)
   1.114 + 
   1.115 +lemma NB_is_uniq [rule_format]: "evs:nsp ==>
   1.116 +Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
   1.117 +--> Crypt (pubK A') {|Nonce NA', Nonce NB, Agent B'|}:parts (spies evs)
   1.118 +--> Nonce NB ~:analz (spies evs) --> A=A' & B=B' & NA=NA'"
   1.119 +apply (erule nsp.induct, simp_all)
   1.120 +by (blast intro: analz_insertI)+
   1.121 +
   1.122 +subsection{*guardedness of NA*}
   1.123 +
   1.124 +lemma ns1_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
   1.125 +ns1 A B NA:set evs --> Guard NA {priK A,priK B} (spies evs)"
   1.126 +apply (erule nsp.induct)
   1.127 +(* Nil *)
   1.128 +apply simp_all
   1.129 +(* Fake *)
   1.130 +apply safe
   1.131 +apply (erule in_synth_Guard, erule Guard_analz, simp)
   1.132 +(* NS1 *)
   1.133 +apply blast
   1.134 +apply blast
   1.135 +apply blast
   1.136 +apply (drule Nonce_neq, simp+, rule No_Nonce, simp)
   1.137 +(* NS2 *)
   1.138 +apply (frule_tac A=A in Nonce_neq, simp+)
   1.139 +apply (case_tac "NAa=NA")
   1.140 +apply (drule Guard_Nonce_analz, simp+)
   1.141 +apply (drule Says_imp_knows_Spy)+
   1.142 +apply (drule_tac B=B and A'=Aa in NA_is_uniq, auto)
   1.143 +(* NS3 *)
   1.144 +apply (case_tac "NB=NA", clarify)
   1.145 +apply (drule Guard_Nonce_analz, simp+)
   1.146 +apply (drule Says_imp_knows_Spy)+
   1.147 +by (drule no_Nonce_NS1_NS2, auto)
   1.148 +
   1.149 +subsection{*guardedness of NB*}
   1.150 +
   1.151 +lemma ns2_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
   1.152 +ns2 B A NA NB:set evs --> Guard NB {priK A,priK B} (spies evs)" 
   1.153 +apply (erule nsp.induct)
   1.154 +(* Nil *)
   1.155 +apply simp_all
   1.156 +(* Fake *)
   1.157 +apply safe
   1.158 +apply (erule in_synth_Guard, erule Guard_analz, simp)
   1.159 +(* NS1 *)
   1.160 +apply (frule Nonce_neq, simp+, blast, rule No_Nonce, simp)
   1.161 +(* NS2 *)
   1.162 +apply blast
   1.163 +apply blast
   1.164 +apply blast
   1.165 +apply (frule_tac A=B and n=NB in Nonce_neq, simp+)
   1.166 +apply (case_tac "NAa=NB")
   1.167 +apply (drule Guard_Nonce_analz, simp+)
   1.168 +apply (drule Says_imp_knows_Spy)+
   1.169 +apply (drule no_Nonce_NS1_NS2, auto)
   1.170 +(* NS3 *)
   1.171 +apply (case_tac "NBa=NB", clarify)
   1.172 +apply (drule Guard_Nonce_analz, simp+)
   1.173 +apply (drule Says_imp_knows_Spy)+
   1.174 +by (drule_tac A=Aa and A'=A in NB_is_uniq, auto)
   1.175 +
   1.176 +subsection{*Agents' Authentication*}
   1.177 +
   1.178 +lemma B_trusts_NS1: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
   1.179 +Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
   1.180 +--> Nonce NA ~:analz (spies evs) --> ns1 A B NA:set evs"
   1.181 +apply (erule nsp.induct, simp_all)
   1.182 +by (blast intro: analz_insertI)+
   1.183 +
   1.184 +lemma A_trusts_NS2: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns1 A B NA:set evs
   1.185 +--> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
   1.186 +--> ns2 B A NA NB:set evs"
   1.187 +apply (erule nsp.induct, simp_all, safe)
   1.188 +apply (frule_tac B=B in ns1_imp_Guard, simp+)
   1.189 +apply (drule Guard_Nonce_analz, simp+, blast)
   1.190 +apply (frule_tac B=B in ns1_imp_Guard, simp+)
   1.191 +apply (drule Guard_Nonce_analz, simp+, blast)
   1.192 +apply (frule_tac B=B in ns1_imp_Guard, simp+)
   1.193 +by (drule Guard_Nonce_analz, simp+, blast+)
   1.194 +
   1.195 +lemma B_trusts_NS3: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns2 B A NA NB:set evs
   1.196 +--> Crypt (pubK B) (Nonce NB):parts (spies evs) --> ns3 A B NB:set evs"
   1.197 +apply (erule nsp.induct, simp_all, safe)
   1.198 +apply (frule_tac B=B in ns2_imp_Guard, simp+)
   1.199 +apply (drule Guard_Nonce_analz, simp+, blast)
   1.200 +apply (frule_tac B=B in ns2_imp_Guard, simp+)
   1.201 +apply (drule Guard_Nonce_analz, simp+, blast)
   1.202 +apply (frule_tac B=B in ns2_imp_Guard, simp+)
   1.203 +apply (drule Guard_Nonce_analz, simp+, blast, blast)
   1.204 +apply (frule_tac B=B in ns2_imp_Guard, simp+)
   1.205 +by (drule Guard_Nonce_analz, auto dest: Says_imp_knows_Spy NB_is_uniq)
   1.206 +
   1.207 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Wed Sep 14 23:14:57 2005 +0200
     2.3 @@ -0,0 +1,195 @@
     2.4 +(******************************************************************************
     2.5 +date: march 2002
     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 +
    2.15 +header{*Otway-Rees Protocol*}
    2.16 +
    2.17 +theory Guard_OtwayRees imports Guard_Shared begin
    2.18 +
    2.19 +subsection{*messages used in the protocol*}
    2.20 +
    2.21 +syntax nil :: "msg"
    2.22 +
    2.23 +translations "nil" == "Number 0"
    2.24 +
    2.25 +syntax or1 :: "agent => agent => nat => event"
    2.26 +
    2.27 +translations "or1 A B NA"
    2.28 +=> "Says A B {|Nonce NA, Agent A, Agent B,
    2.29 +               Ciph A {|Nonce NA, Agent A, Agent B|}|}"
    2.30 +
    2.31 +syntax or1' :: "agent => agent => agent => nat => msg => event"
    2.32 +
    2.33 +translations "or1' A' A B NA X"
    2.34 +=> "Says A' B {|Nonce NA, Agent A, Agent B, X|}"
    2.35 +
    2.36 +syntax or2 :: "agent => agent => nat => nat => msg => event"
    2.37 +
    2.38 +translations "or2 A B NA NB X"
    2.39 +=> "Says B Server {|Nonce NA, Agent A, Agent B, X,
    2.40 +                    Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
    2.41 +
    2.42 +syntax or2' :: "agent => agent => agent => nat => nat => event"
    2.43 +
    2.44 +translations "or2' B' A B NA NB"
    2.45 +=> "Says B' Server {|Nonce NA, Agent A, Agent B,
    2.46 +                     Ciph A {|Nonce NA, Agent A, Agent B|},
    2.47 +                     Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
    2.48 +
    2.49 +syntax or3 :: "agent => agent => nat => nat => key => event"
    2.50 +
    2.51 +translations "or3 A B NA NB K"
    2.52 +=> "Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|},
    2.53 +                    Ciph B {|Nonce NB, Key K|}|}"
    2.54 +
    2.55 +syntax or3':: "agent => msg => agent => agent => nat => nat => key => event"
    2.56 +
    2.57 +translations "or3' S Y A B NA NB K"
    2.58 +=> "Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}"
    2.59 +
    2.60 +syntax or4 :: "agent => agent => nat => msg => event"
    2.61 +
    2.62 +translations "or4 A B NA X" => "Says B A {|Nonce NA, X, nil|}"
    2.63 +
    2.64 +syntax or4' :: "agent => agent => nat => msg => event"
    2.65 +
    2.66 +translations "or4' B' A NA K" =>
    2.67 +"Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}"
    2.68 +
    2.69 +subsection{*definition of the protocol*}
    2.70 +
    2.71 +consts or :: "event list set"
    2.72 +
    2.73 +inductive or
    2.74 +intros
    2.75 +
    2.76 +Nil: "[]:or"
    2.77 +
    2.78 +Fake: "[| evs:or; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:or"
    2.79 +
    2.80 +OR1: "[| evs1:or; Nonce NA ~:used evs1 |] ==> or1 A B NA # evs1:or"
    2.81 +
    2.82 +OR2: "[| evs2:or; or1' A' A B NA X:set evs2; Nonce NB ~:used evs2 |]
    2.83 +==> or2 A B NA NB X # evs2:or"
    2.84 +
    2.85 +OR3: "[| evs3:or; or2' B' A B NA NB:set evs3; Key K ~:used evs3 |]
    2.86 +==> or3 A B NA NB K # evs3:or"
    2.87 +
    2.88 +OR4: "[| evs4:or; or2 A B NA NB X:set evs4; or3' S Y A B NA NB K:set evs4 |]
    2.89 +==> or4 A B NA X # evs4:or"
    2.90 +
    2.91 +subsection{*declarations for tactics*}
    2.92 +
    2.93 +declare knows_Spy_partsEs [elim]
    2.94 +declare Fake_parts_insert [THEN subsetD, dest]
    2.95 +declare initState.simps [simp del]
    2.96 +
    2.97 +subsection{*general properties of or*}
    2.98 +
    2.99 +lemma or_has_no_Gets: "evs:or ==> ALL A X. Gets A X ~:set evs"
   2.100 +by (erule or.induct, auto)
   2.101 +
   2.102 +lemma or_is_Gets_correct [iff]: "Gets_correct or"
   2.103 +by (auto simp: Gets_correct_def dest: or_has_no_Gets)
   2.104 +
   2.105 +lemma or_is_one_step [iff]: "one_step or"
   2.106 +by (unfold one_step_def, clarify, ind_cases "ev#evs:or", auto)
   2.107 +
   2.108 +lemma or_has_only_Says' [rule_format]: "evs:or ==>
   2.109 +ev:set evs --> (EX A B X. ev=Says A B X)"
   2.110 +by (erule or.induct, auto)
   2.111 +
   2.112 +lemma or_has_only_Says [iff]: "has_only_Says or"
   2.113 +by (auto simp: has_only_Says_def dest: or_has_only_Says')
   2.114 +
   2.115 +subsection{*or is regular*}
   2.116 +
   2.117 +lemma or1'_parts_spies [dest]: "or1' A' A B NA X:set evs
   2.118 +==> X:parts (spies evs)"
   2.119 +by blast
   2.120 +
   2.121 +lemma or2_parts_spies [dest]: "or2 A B NA NB X:set evs
   2.122 +==> X:parts (spies evs)"
   2.123 +by blast
   2.124 +
   2.125 +lemma or3_parts_spies [dest]: "Says S B {|NA, Y, Ciph B {|NB, K|}|}:set evs
   2.126 +==> K:parts (spies evs)"
   2.127 +by blast
   2.128 +
   2.129 +lemma or_is_regular [iff]: "regular or"
   2.130 +apply (simp only: regular_def, clarify)
   2.131 +apply (erule or.induct, simp_all add: initState.simps knows.simps)
   2.132 +by (auto dest: parts_sub)
   2.133 +
   2.134 +subsection{*guardedness of KAB*}
   2.135 +
   2.136 +lemma Guard_KAB [rule_format]: "[| evs:or; A ~:bad; B ~:bad |] ==>
   2.137 +or3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" 
   2.138 +apply (erule or.induct)
   2.139 +(* Nil *)
   2.140 +apply simp_all
   2.141 +(* Fake *)
   2.142 +apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp)
   2.143 +(* OR1 *)
   2.144 +apply blast
   2.145 +(* OR2 *)
   2.146 +apply safe
   2.147 +apply (blast dest: Says_imp_spies, blast)
   2.148 +(* OR3 *)
   2.149 +apply blast
   2.150 +apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
   2.151 +apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
   2.152 +(* OR4 *)
   2.153 +by (blast dest: Says_imp_spies in_GuardK_kparts)
   2.154 +
   2.155 +subsection{*guardedness of NB*}
   2.156 +
   2.157 +lemma Guard_NB [rule_format]: "[| evs:or; B ~:bad |] ==>
   2.158 +or2 A B NA NB X:set evs --> Guard NB {shrK B} (spies evs)" 
   2.159 +apply (erule or.induct)
   2.160 +(* Nil *)
   2.161 +apply simp_all
   2.162 +(* Fake *)
   2.163 +apply safe
   2.164 +apply (erule in_synth_Guard, erule Guard_analz, simp)
   2.165 +(* OR1 *)
   2.166 +apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
   2.167 +apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
   2.168 +(* OR2 *)
   2.169 +apply blast
   2.170 +apply (drule_tac n=NA in Nonce_neq, simp+, rule No_Nonce, simp)
   2.171 +apply (blast intro!: No_Nonce dest: used_parts)
   2.172 +apply (drule_tac n=NA in Nonce_neq, simp+, rule No_Nonce, simp)
   2.173 +apply (blast intro!: No_Nonce dest: used_parts)
   2.174 +apply (blast dest: Says_imp_spies)
   2.175 +apply (blast dest: Says_imp_spies)
   2.176 +apply (case_tac "Ba=B", clarsimp)
   2.177 +apply (drule_tac n=NB and A=B in Nonce_neq, simp+)
   2.178 +apply (drule Says_imp_spies)
   2.179 +apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+, rule No_Nonce, simp)
   2.180 +(* OR3 *)
   2.181 +apply (drule Says_imp_spies)
   2.182 +apply (frule_tac n'=NAa in in_Guard_kparts_neq, simp+, rule No_Nonce, simp)
   2.183 +apply (case_tac "Aa=B", clarsimp)
   2.184 +apply (case_tac "NAa=NB", clarsimp)
   2.185 +apply (drule Says_imp_spies)
   2.186 +apply (drule_tac Y="{|Nonce NB, Agent Aa, Agent Ba|}"
   2.187 +                 and K="shrK Aa" in in_Guard_kparts_Crypt, simp+)
   2.188 +apply (simp add: No_Nonce) 
   2.189 +apply (case_tac "Ba=B", clarsimp)
   2.190 +apply (case_tac "NBa=NB", clarify)
   2.191 +apply (drule Says_imp_spies)
   2.192 +apply (drule_tac Y="{|Nonce NAa, Nonce NB, Agent Aa, Agent Ba|}"
   2.193 +                 and K="shrK Ba" in in_Guard_kparts_Crypt, simp+)
   2.194 +apply (simp add: No_Nonce) 
   2.195 +(* OR4 *)
   2.196 +by (blast dest: Says_imp_spies)+
   2.197 +
   2.198 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy	Wed Sep 14 23:14:57 2005 +0200
     3.3 @@ -0,0 +1,259 @@
     3.4 +(******************************************************************************
     3.5 +date: march 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 +
    3.15 +header{*Yahalom Protocol*}
    3.16 +
    3.17 +theory Guard_Yahalom imports Guard_Shared begin
    3.18 +
    3.19 +subsection{*messages used in the protocol*}
    3.20 +
    3.21 +syntax ya1 :: "agent => agent => nat => event"
    3.22 +
    3.23 +translations "ya1 A B NA" => "Says A B {|Agent A, Nonce NA|}"
    3.24 +
    3.25 +syntax ya1' :: "agent => agent => agent => nat => event"
    3.26 +
    3.27 +translations "ya1' A' A B NA" => "Says A' B {|Agent A, Nonce NA|}"
    3.28 +
    3.29 +syntax ya2 :: "agent => agent => nat => nat => event"
    3.30 +
    3.31 +translations "ya2 A B NA NB"
    3.32 +=> "Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
    3.33 +
    3.34 +syntax ya2' :: "agent => agent => agent => nat => nat => event"
    3.35 +
    3.36 +translations "ya2' B' A B NA NB"
    3.37 +=> "Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
    3.38 +
    3.39 +syntax ya3 :: "agent => agent => nat => nat => key => event"
    3.40 +
    3.41 +translations "ya3 A B NA NB K"
    3.42 +=> "Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
    3.43 +                    Ciph B {|Agent A, Key K|}|}"
    3.44 +
    3.45 +syntax ya3':: "agent => msg => agent => agent => nat => nat => key => event"
    3.46 +
    3.47 +translations "ya3' S Y A B NA NB K"
    3.48 +=> "Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
    3.49 +
    3.50 +syntax ya4 :: "agent => agent => nat => nat => msg => event"
    3.51 +
    3.52 +translations "ya4 A B K NB Y" => "Says A B {|Y, Crypt K (Nonce NB)|}"
    3.53 +
    3.54 +syntax ya4' :: "agent => agent => nat => nat => msg => event"
    3.55 +
    3.56 +translations "ya4' A' B K NB Y" => "Says A' B {|Y, Crypt K (Nonce NB)|}"
    3.57 +
    3.58 +subsection{*definition of the protocol*}
    3.59 +
    3.60 +consts ya :: "event list set"
    3.61 +
    3.62 +inductive ya
    3.63 +intros
    3.64 +
    3.65 +Nil: "[]:ya"
    3.66 +
    3.67 +Fake: "[| evs:ya; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:ya"
    3.68 +
    3.69 +YA1: "[| evs1:ya; Nonce NA ~:used evs1 |] ==> ya1 A B NA # evs1:ya"
    3.70 +
    3.71 +YA2: "[| evs2:ya; ya1' A' A B NA:set evs2; Nonce NB ~:used evs2 |]
    3.72 +==> ya2 A B NA NB # evs2:ya"
    3.73 +
    3.74 +YA3: "[| evs3:ya; ya2' B' A B NA NB:set evs3; Key K ~:used evs3 |]
    3.75 +==> ya3 A B NA NB K # evs3:ya"
    3.76 +
    3.77 +YA4: "[| evs4:ya; ya1 A B NA:set evs4; ya3' S Y A B NA NB K:set evs4 |]
    3.78 +==> ya4 A B K NB Y # evs4:ya"
    3.79 +
    3.80 +subsection{*declarations for tactics*}
    3.81 +
    3.82 +declare knows_Spy_partsEs [elim]
    3.83 +declare Fake_parts_insert [THEN subsetD, dest]
    3.84 +declare initState.simps [simp del]
    3.85 +
    3.86 +subsection{*general properties of ya*}
    3.87 +
    3.88 +lemma ya_has_no_Gets: "evs:ya ==> ALL A X. Gets A X ~:set evs"
    3.89 +by (erule ya.induct, auto)
    3.90 +
    3.91 +lemma ya_is_Gets_correct [iff]: "Gets_correct ya"
    3.92 +by (auto simp: Gets_correct_def dest: ya_has_no_Gets)
    3.93 +
    3.94 +lemma ya_is_one_step [iff]: "one_step ya"
    3.95 +by (unfold one_step_def, clarify, ind_cases "ev#evs:ya", auto)
    3.96 +
    3.97 +lemma ya_has_only_Says' [rule_format]: "evs:ya ==>
    3.98 +ev:set evs --> (EX A B X. ev=Says A B X)"
    3.99 +by (erule ya.induct, auto)
   3.100 +
   3.101 +lemma ya_has_only_Says [iff]: "has_only_Says ya"
   3.102 +by (auto simp: has_only_Says_def dest: ya_has_only_Says')
   3.103 +
   3.104 +lemma ya_is_regular [iff]: "regular ya"
   3.105 +apply (simp only: regular_def, clarify)
   3.106 +apply (erule ya.induct, simp_all add: initState.simps knows.simps)
   3.107 +by (auto dest: parts_sub)
   3.108 +
   3.109 +subsection{*guardedness of KAB*}
   3.110 +
   3.111 +lemma Guard_KAB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
   3.112 +ya3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" 
   3.113 +apply (erule ya.induct)
   3.114 +(* Nil *)
   3.115 +apply simp_all
   3.116 +(* Fake *)
   3.117 +apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp)
   3.118 +(* YA1 *)
   3.119 +(* YA2 *)
   3.120 +apply safe
   3.121 +apply (blast dest: Says_imp_spies)
   3.122 +(* YA3 *)
   3.123 +apply blast
   3.124 +apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
   3.125 +apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
   3.126 +(* YA4 *)
   3.127 +apply (blast dest: Says_imp_spies in_GuardK_kparts)
   3.128 +by blast
   3.129 +
   3.130 +subsection{*session keys are not symmetric keys*}
   3.131 +
   3.132 +lemma KAB_isnt_shrK [rule_format]: "evs:ya ==>
   3.133 +ya3 A B NA NB K:set evs --> K ~:range shrK"
   3.134 +by (erule ya.induct, auto)
   3.135 +
   3.136 +lemma ya3_shrK: "evs:ya ==> ya3 A B NA NB (shrK C) ~:set evs"
   3.137 +by (blast dest: KAB_isnt_shrK)
   3.138 +
   3.139 +subsection{*ya2' implies ya1'*}
   3.140 +
   3.141 +lemma ya2'_parts_imp_ya1'_parts [rule_format]:
   3.142 +     "[| evs:ya; B ~:bad |] ==>
   3.143 +      Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
   3.144 +      {|Agent A, Nonce NA|}:spies evs"
   3.145 +by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts)
   3.146 +
   3.147 +lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB:set evs; evs:ya; B ~:bad |]
   3.148 +==> {|Agent A, Nonce NA|}:spies evs"
   3.149 +by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts)
   3.150 +
   3.151 +subsection{*uniqueness of NB*}
   3.152 +
   3.153 +lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs:ya; B ~:bad; B' ~:bad |] ==>
   3.154 +Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
   3.155 +Ciph B' {|Agent A', Nonce NA', Nonce NB|}:parts (spies evs) -->
   3.156 +A=A' & B=B' & NA=NA'"
   3.157 +apply (erule ya.induct, simp_all, clarify)
   3.158 +apply (drule Crypt_synth_insert, simp+)
   3.159 +apply (drule Crypt_synth_insert, simp+, safe)
   3.160 +apply (drule not_used_parts_false, simp+)+
   3.161 +by (drule Says_not_parts, simp+)+
   3.162 +
   3.163 +lemma NB_is_uniq_in_ya2': "[| ya2' C A B NA NB:set evs;
   3.164 +ya2' C' A' B' NA' NB:set evs; evs:ya; B ~:bad; B' ~:bad |]
   3.165 +==> A=A' & B=B' & NA=NA'"
   3.166 +by (drule NB_is_uniq_in_ya2'_parts, auto dest: Says_imp_spies)
   3.167 +
   3.168 +subsection{*ya3' implies ya2'*}
   3.169 +
   3.170 +lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs:ya; A ~:bad |] ==>
   3.171 +Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
   3.172 +--> Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs)"
   3.173 +apply (erule ya.induct, simp_all)
   3.174 +apply (clarify, drule Crypt_synth_insert, simp+)
   3.175 +apply (blast intro: parts_sub, blast)
   3.176 +by (auto dest: Says_imp_spies parts_parts)
   3.177 +
   3.178 +lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs:ya; A ~:bad |] ==>
   3.179 +Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
   3.180 +--> (EX B'. ya2' B' A B NA NB:set evs)"
   3.181 +apply (erule ya.induct, simp_all, safe)
   3.182 +apply (drule Crypt_synth_insert, simp+)
   3.183 +apply (drule Crypt_synth_insert, simp+, blast)
   3.184 +apply blast
   3.185 +apply blast
   3.186 +by (auto dest: Says_imp_spies2 parts_parts)
   3.187 +
   3.188 +lemma ya3'_imp_ya2': "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
   3.189 +==> (EX B'. ya2' B' A B NA NB:set evs)"
   3.190 +by (drule ya3'_parts_imp_ya2', auto dest: Says_imp_spies)
   3.191 +
   3.192 +subsection{*ya3' implies ya3*}
   3.193 +
   3.194 +lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs:ya; A ~:bad |] ==>
   3.195 +Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts(spies evs)
   3.196 +--> ya3 A B NA NB K:set evs"
   3.197 +apply (erule ya.induct, simp_all, safe)
   3.198 +apply (drule Crypt_synth_insert, simp+)
   3.199 +by (blast dest: Says_imp_spies2 parts_parts)
   3.200 +
   3.201 +lemma ya3'_imp_ya3: "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
   3.202 +==> ya3 A B NA NB K:set evs"
   3.203 +by (blast dest: Says_imp_spies ya3'_parts_imp_ya3)
   3.204 +
   3.205 +subsection{*guardedness of NB*}
   3.206 +
   3.207 +constdefs ya_keys :: "agent => agent => nat => nat => event list => key set"
   3.208 +"ya_keys A B NA NB evs == {shrK A,shrK B} Un {K. ya3 A B NA NB K:set evs}"
   3.209 +
   3.210 +lemma Guard_NB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
   3.211 +ya2 A B NA NB:set evs --> Guard NB (ya_keys A B NA NB evs) (spies evs)"
   3.212 +apply (erule ya.induct)
   3.213 +(* Nil *)
   3.214 +apply (simp_all add: ya_keys_def)
   3.215 +(* Fake *)
   3.216 +apply safe
   3.217 +apply (erule in_synth_Guard, erule Guard_analz, simp, clarify)
   3.218 +apply (frule_tac B=B in Guard_KAB, simp+)
   3.219 +apply (drule_tac p=ya in GuardK_Key_analz, simp+)
   3.220 +apply (blast dest: KAB_isnt_shrK, simp)
   3.221 +(* YA1 *)
   3.222 +apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
   3.223 +(* YA2 *)
   3.224 +apply blast
   3.225 +apply (drule Says_imp_spies)
   3.226 +apply (drule_tac n=NB in Nonce_neq, simp+)
   3.227 +apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+)
   3.228 +apply (rule No_Nonce, simp)
   3.229 +(* YA3 *)
   3.230 +apply (rule Guard_extand, simp, blast)
   3.231 +apply (case_tac "NAa=NB", clarify)
   3.232 +apply (frule Says_imp_spies)
   3.233 +apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
   3.234 +apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
   3.235 +apply (drule ya2'_imp_ya1'_parts, simp, blast, blast)
   3.236 +apply (case_tac "NBa=NB", clarify)
   3.237 +apply (frule Says_imp_spies)
   3.238 +apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
   3.239 +apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
   3.240 +apply (drule NB_is_uniq_in_ya2', simp+, blast, simp+)
   3.241 +apply (simp add: No_Nonce, blast)
   3.242 +(* YA4 *)
   3.243 +apply (blast dest: Says_imp_spies)
   3.244 +apply (case_tac "NBa=NB", clarify)
   3.245 +apply (frule_tac A=S in Says_imp_spies)
   3.246 +apply (frule in_Guard_kparts_Crypt, simp+)
   3.247 +apply (blast dest: Says_imp_spies)
   3.248 +apply (case_tac "NBa=NB", clarify)
   3.249 +apply (frule_tac A=S in Says_imp_spies)
   3.250 +apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
   3.251 +apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Aa in ya3_shrK, simp)
   3.252 +apply (frule ya3'_imp_ya2', simp+, blast, clarify)
   3.253 +apply (frule_tac A=B' in Says_imp_spies)
   3.254 +apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+, blast, simp+)
   3.255 +apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
   3.256 +apply (drule NB_is_uniq_in_ya2', simp+, blast, clarify)
   3.257 +apply (drule ya3'_imp_ya3, simp+)
   3.258 +apply (simp add: Guard_Nonce)
   3.259 +apply (simp add: No_Nonce)
   3.260 +done
   3.261 +
   3.262 +end
     4.1 --- a/src/HOL/Auth/Guard/NS_Public.thy	Wed Sep 14 23:06:02 2005 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,204 +0,0 @@
     4.4 -(******************************************************************************
     4.5 -incorporating Lowe's fix (inclusion of B's identity in round 2)
     4.6 -
     4.7 -date: march 2002
     4.8 -author: Frederic Blanqui
     4.9 -email: blanqui@lri.fr
    4.10 -webpage: http://www.lri.fr/~blanqui/
    4.11 -
    4.12 -University of Cambridge, Computer Laboratory
    4.13 -William Gates Building, JJ Thomson Avenue
    4.14 -Cambridge CB3 0FD, United Kingdom
    4.15 -******************************************************************************)
    4.16 -
    4.17 -header{*Needham-Schroeder-Lowe Public-Key Protocol*}
    4.18 -
    4.19 -theory NS_Public imports Guard_Public begin
    4.20 -
    4.21 -subsection{*messages used in the protocol*}
    4.22 -
    4.23 -syntax ns1 :: "agent => agent => nat => event"
    4.24 -
    4.25 -translations "ns1 A B NA" => "Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
    4.26 -
    4.27 -syntax ns1' :: "agent => agent => agent => nat => event"
    4.28 -
    4.29 -translations "ns1' A' A B NA"
    4.30 -=> "Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
    4.31 -
    4.32 -syntax ns2 :: "agent => agent => nat => nat => event"
    4.33 -
    4.34 -translations "ns2 B A NA NB"
    4.35 -=> "Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
    4.36 -
    4.37 -syntax ns2' :: "agent => agent => agent => nat => nat => event"
    4.38 -
    4.39 -translations "ns2' B' B A NA NB"
    4.40 -=> "Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
    4.41 -
    4.42 -syntax ns3 :: "agent => agent => nat => event"
    4.43 -
    4.44 -translations "ns3 A B NB" => "Says A B (Crypt (pubK B) (Nonce NB))"
    4.45 -
    4.46 -subsection{*definition of the protocol*}
    4.47 -
    4.48 -consts nsp :: "event list set"
    4.49 -
    4.50 -inductive nsp
    4.51 -intros
    4.52 -
    4.53 -Nil: "[]:nsp"
    4.54 -
    4.55 -Fake: "[| evs:nsp; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs : nsp"
    4.56 -
    4.57 -NS1: "[| evs1:nsp; Nonce NA ~:used evs1 |] ==> ns1 A B NA # evs1 : nsp"
    4.58 -
    4.59 -NS2: "[| evs2:nsp; Nonce NB ~:used evs2; ns1' A' A B NA:set evs2 |] ==>
    4.60 -ns2 B A NA NB # evs2:nsp"
    4.61 -
    4.62 -NS3: "[| evs3:nsp; ns1 A B NA:set evs3; ns2' B' B A NA NB:set evs3 |] ==>
    4.63 -ns3 A B NB # evs3:nsp"
    4.64 -
    4.65 -subsection{*declarations for tactics*}
    4.66 -
    4.67 -declare knows_Spy_partsEs [elim]
    4.68 -declare Fake_parts_insert [THEN subsetD, dest]
    4.69 -declare initState.simps [simp del]
    4.70 -
    4.71 -subsection{*general properties of nsp*}
    4.72 -
    4.73 -lemma nsp_has_no_Gets: "evs:nsp ==> ALL A X. Gets A X ~:set evs"
    4.74 -by (erule nsp.induct, auto)
    4.75 -
    4.76 -lemma nsp_is_Gets_correct [iff]: "Gets_correct nsp"
    4.77 -by (auto simp: Gets_correct_def dest: nsp_has_no_Gets)
    4.78 -
    4.79 -lemma nsp_is_one_step [iff]: "one_step nsp"
    4.80 -by (unfold one_step_def, clarify, ind_cases "ev#evs:nsp", auto)
    4.81 -
    4.82 -lemma nsp_has_only_Says' [rule_format]: "evs:nsp ==>
    4.83 -ev:set evs --> (EX A B X. ev=Says A B X)"
    4.84 -by (erule nsp.induct, auto)
    4.85 -
    4.86 -lemma nsp_has_only_Says [iff]: "has_only_Says nsp"
    4.87 -by (auto simp: has_only_Says_def dest: nsp_has_only_Says')
    4.88 -
    4.89 -lemma nsp_is_regular [iff]: "regular nsp"
    4.90 -apply (simp only: regular_def, clarify)
    4.91 -by (erule nsp.induct, auto simp: initState.simps knows.simps)
    4.92 -
    4.93 -subsection{*nonce are used only once*}
    4.94 -
    4.95 -lemma NA_is_uniq [rule_format]: "evs:nsp ==>
    4.96 -Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
    4.97 ---> Crypt (pubK B') {|Nonce NA, Agent A'|}:parts (spies evs)
    4.98 ---> Nonce NA ~:analz (spies evs) --> A=A' & B=B'"
    4.99 -apply (erule nsp.induct, simp_all)
   4.100 -by (blast intro: analz_insertI)+
   4.101 -
   4.102 -lemma no_Nonce_NS1_NS2 [rule_format]: "evs:nsp ==>
   4.103 -Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs)
   4.104 ---> Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
   4.105 ---> Nonce NA:analz (spies evs)"
   4.106 -apply (erule nsp.induct, simp_all)
   4.107 -by (blast intro: analz_insertI)+
   4.108 -
   4.109 -lemma no_Nonce_NS1_NS2' [rule_format]:
   4.110 -"[| Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs);
   4.111 -Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs); evs:nsp |]
   4.112 -==> Nonce NA:analz (spies evs)"
   4.113 -by (rule no_Nonce_NS1_NS2, auto)
   4.114 - 
   4.115 -lemma NB_is_uniq [rule_format]: "evs:nsp ==>
   4.116 -Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
   4.117 ---> Crypt (pubK A') {|Nonce NA', Nonce NB, Agent B'|}:parts (spies evs)
   4.118 ---> Nonce NB ~:analz (spies evs) --> A=A' & B=B' & NA=NA'"
   4.119 -apply (erule nsp.induct, simp_all)
   4.120 -by (blast intro: analz_insertI)+
   4.121 -
   4.122 -subsection{*guardedness of NA*}
   4.123 -
   4.124 -lemma ns1_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
   4.125 -ns1 A B NA:set evs --> Guard NA {priK A,priK B} (spies evs)"
   4.126 -apply (erule nsp.induct)
   4.127 -(* Nil *)
   4.128 -apply simp_all
   4.129 -(* Fake *)
   4.130 -apply safe
   4.131 -apply (erule in_synth_Guard, erule Guard_analz, simp)
   4.132 -(* NS1 *)
   4.133 -apply blast
   4.134 -apply blast
   4.135 -apply blast
   4.136 -apply (drule Nonce_neq, simp+, rule No_Nonce, simp)
   4.137 -(* NS2 *)
   4.138 -apply (frule_tac A=A in Nonce_neq, simp+)
   4.139 -apply (case_tac "NAa=NA")
   4.140 -apply (drule Guard_Nonce_analz, simp+)
   4.141 -apply (drule Says_imp_knows_Spy)+
   4.142 -apply (drule_tac B=B and A'=Aa in NA_is_uniq, auto)
   4.143 -(* NS3 *)
   4.144 -apply (case_tac "NB=NA", clarify)
   4.145 -apply (drule Guard_Nonce_analz, simp+)
   4.146 -apply (drule Says_imp_knows_Spy)+
   4.147 -by (drule no_Nonce_NS1_NS2, auto)
   4.148 -
   4.149 -subsection{*guardedness of NB*}
   4.150 -
   4.151 -lemma ns2_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
   4.152 -ns2 B A NA NB:set evs --> Guard NB {priK A,priK B} (spies evs)" 
   4.153 -apply (erule nsp.induct)
   4.154 -(* Nil *)
   4.155 -apply simp_all
   4.156 -(* Fake *)
   4.157 -apply safe
   4.158 -apply (erule in_synth_Guard, erule Guard_analz, simp)
   4.159 -(* NS1 *)
   4.160 -apply (frule Nonce_neq, simp+, blast, rule No_Nonce, simp)
   4.161 -(* NS2 *)
   4.162 -apply blast
   4.163 -apply blast
   4.164 -apply blast
   4.165 -apply (frule_tac A=B and n=NB in Nonce_neq, simp+)
   4.166 -apply (case_tac "NAa=NB")
   4.167 -apply (drule Guard_Nonce_analz, simp+)
   4.168 -apply (drule Says_imp_knows_Spy)+
   4.169 -apply (drule no_Nonce_NS1_NS2, auto)
   4.170 -(* NS3 *)
   4.171 -apply (case_tac "NBa=NB", clarify)
   4.172 -apply (drule Guard_Nonce_analz, simp+)
   4.173 -apply (drule Says_imp_knows_Spy)+
   4.174 -by (drule_tac A=Aa and A'=A in NB_is_uniq, auto)
   4.175 -
   4.176 -subsection{*Agents' Authentication*}
   4.177 -
   4.178 -lemma B_trusts_NS1: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
   4.179 -Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
   4.180 ---> Nonce NA ~:analz (spies evs) --> ns1 A B NA:set evs"
   4.181 -apply (erule nsp.induct, simp_all)
   4.182 -by (blast intro: analz_insertI)+
   4.183 -
   4.184 -lemma A_trusts_NS2: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns1 A B NA:set evs
   4.185 ---> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
   4.186 ---> ns2 B A NA NB:set evs"
   4.187 -apply (erule nsp.induct, simp_all, safe)
   4.188 -apply (frule_tac B=B in ns1_imp_Guard, simp+)
   4.189 -apply (drule Guard_Nonce_analz, simp+, blast)
   4.190 -apply (frule_tac B=B in ns1_imp_Guard, simp+)
   4.191 -apply (drule Guard_Nonce_analz, simp+, blast)
   4.192 -apply (frule_tac B=B in ns1_imp_Guard, simp+)
   4.193 -by (drule Guard_Nonce_analz, simp+, blast+)
   4.194 -
   4.195 -lemma B_trusts_NS3: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns2 B A NA NB:set evs
   4.196 ---> Crypt (pubK B) (Nonce NB):parts (spies evs) --> ns3 A B NB:set evs"
   4.197 -apply (erule nsp.induct, simp_all, safe)
   4.198 -apply (frule_tac B=B in ns2_imp_Guard, simp+)
   4.199 -apply (drule Guard_Nonce_analz, simp+, blast)
   4.200 -apply (frule_tac B=B in ns2_imp_Guard, simp+)
   4.201 -apply (drule Guard_Nonce_analz, simp+, blast)
   4.202 -apply (frule_tac B=B in ns2_imp_Guard, simp+)
   4.203 -apply (drule Guard_Nonce_analz, simp+, blast, blast)
   4.204 -apply (frule_tac B=B in ns2_imp_Guard, simp+)
   4.205 -by (drule Guard_Nonce_analz, auto dest: Says_imp_knows_Spy NB_is_uniq)
   4.206 -
   4.207 -end
     5.1 --- a/src/HOL/Auth/Guard/OtwayRees.thy	Wed Sep 14 23:06:02 2005 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,195 +0,0 @@
     5.4 -(******************************************************************************
     5.5 -date: march 2002
     5.6 -author: Frederic Blanqui
     5.7 -email: blanqui@lri.fr
     5.8 -webpage: http://www.lri.fr/~blanqui/
     5.9 -
    5.10 -University of Cambridge, Computer Laboratory
    5.11 -William Gates Building, JJ Thomson Avenue
    5.12 -Cambridge CB3 0FD, United Kingdom
    5.13 -******************************************************************************)
    5.14 -
    5.15 -header{*Otway-Rees Protocol*}
    5.16 -
    5.17 -theory OtwayRees imports Guard_Shared begin
    5.18 -
    5.19 -subsection{*messages used in the protocol*}
    5.20 -
    5.21 -syntax nil :: "msg"
    5.22 -
    5.23 -translations "nil" == "Number 0"
    5.24 -
    5.25 -syntax or1 :: "agent => agent => nat => event"
    5.26 -
    5.27 -translations "or1 A B NA"
    5.28 -=> "Says A B {|Nonce NA, Agent A, Agent B,
    5.29 -               Ciph A {|Nonce NA, Agent A, Agent B|}|}"
    5.30 -
    5.31 -syntax or1' :: "agent => agent => agent => nat => msg => event"
    5.32 -
    5.33 -translations "or1' A' A B NA X"
    5.34 -=> "Says A' B {|Nonce NA, Agent A, Agent B, X|}"
    5.35 -
    5.36 -syntax or2 :: "agent => agent => nat => nat => msg => event"
    5.37 -
    5.38 -translations "or2 A B NA NB X"
    5.39 -=> "Says B Server {|Nonce NA, Agent A, Agent B, X,
    5.40 -                    Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
    5.41 -
    5.42 -syntax or2' :: "agent => agent => agent => nat => nat => event"
    5.43 -
    5.44 -translations "or2' B' A B NA NB"
    5.45 -=> "Says B' Server {|Nonce NA, Agent A, Agent B,
    5.46 -                     Ciph A {|Nonce NA, Agent A, Agent B|},
    5.47 -                     Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
    5.48 -
    5.49 -syntax or3 :: "agent => agent => nat => nat => key => event"
    5.50 -
    5.51 -translations "or3 A B NA NB K"
    5.52 -=> "Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|},
    5.53 -                    Ciph B {|Nonce NB, Key K|}|}"
    5.54 -
    5.55 -syntax or3':: "agent => msg => agent => agent => nat => nat => key => event"
    5.56 -
    5.57 -translations "or3' S Y A B NA NB K"
    5.58 -=> "Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}"
    5.59 -
    5.60 -syntax or4 :: "agent => agent => nat => msg => event"
    5.61 -
    5.62 -translations "or4 A B NA X" => "Says B A {|Nonce NA, X, nil|}"
    5.63 -
    5.64 -syntax or4' :: "agent => agent => nat => msg => event"
    5.65 -
    5.66 -translations "or4' B' A NA K" =>
    5.67 -"Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}"
    5.68 -
    5.69 -subsection{*definition of the protocol*}
    5.70 -
    5.71 -consts or :: "event list set"
    5.72 -
    5.73 -inductive or
    5.74 -intros
    5.75 -
    5.76 -Nil: "[]:or"
    5.77 -
    5.78 -Fake: "[| evs:or; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:or"
    5.79 -
    5.80 -OR1: "[| evs1:or; Nonce NA ~:used evs1 |] ==> or1 A B NA # evs1:or"
    5.81 -
    5.82 -OR2: "[| evs2:or; or1' A' A B NA X:set evs2; Nonce NB ~:used evs2 |]
    5.83 -==> or2 A B NA NB X # evs2:or"
    5.84 -
    5.85 -OR3: "[| evs3:or; or2' B' A B NA NB:set evs3; Key K ~:used evs3 |]
    5.86 -==> or3 A B NA NB K # evs3:or"
    5.87 -
    5.88 -OR4: "[| evs4:or; or2 A B NA NB X:set evs4; or3' S Y A B NA NB K:set evs4 |]
    5.89 -==> or4 A B NA X # evs4:or"
    5.90 -
    5.91 -subsection{*declarations for tactics*}
    5.92 -
    5.93 -declare knows_Spy_partsEs [elim]
    5.94 -declare Fake_parts_insert [THEN subsetD, dest]
    5.95 -declare initState.simps [simp del]
    5.96 -
    5.97 -subsection{*general properties of or*}
    5.98 -
    5.99 -lemma or_has_no_Gets: "evs:or ==> ALL A X. Gets A X ~:set evs"
   5.100 -by (erule or.induct, auto)
   5.101 -
   5.102 -lemma or_is_Gets_correct [iff]: "Gets_correct or"
   5.103 -by (auto simp: Gets_correct_def dest: or_has_no_Gets)
   5.104 -
   5.105 -lemma or_is_one_step [iff]: "one_step or"
   5.106 -by (unfold one_step_def, clarify, ind_cases "ev#evs:or", auto)
   5.107 -
   5.108 -lemma or_has_only_Says' [rule_format]: "evs:or ==>
   5.109 -ev:set evs --> (EX A B X. ev=Says A B X)"
   5.110 -by (erule or.induct, auto)
   5.111 -
   5.112 -lemma or_has_only_Says [iff]: "has_only_Says or"
   5.113 -by (auto simp: has_only_Says_def dest: or_has_only_Says')
   5.114 -
   5.115 -subsection{*or is regular*}
   5.116 -
   5.117 -lemma or1'_parts_spies [dest]: "or1' A' A B NA X:set evs
   5.118 -==> X:parts (spies evs)"
   5.119 -by blast
   5.120 -
   5.121 -lemma or2_parts_spies [dest]: "or2 A B NA NB X:set evs
   5.122 -==> X:parts (spies evs)"
   5.123 -by blast
   5.124 -
   5.125 -lemma or3_parts_spies [dest]: "Says S B {|NA, Y, Ciph B {|NB, K|}|}:set evs
   5.126 -==> K:parts (spies evs)"
   5.127 -by blast
   5.128 -
   5.129 -lemma or_is_regular [iff]: "regular or"
   5.130 -apply (simp only: regular_def, clarify)
   5.131 -apply (erule or.induct, simp_all add: initState.simps knows.simps)
   5.132 -by (auto dest: parts_sub)
   5.133 -
   5.134 -subsection{*guardedness of KAB*}
   5.135 -
   5.136 -lemma Guard_KAB [rule_format]: "[| evs:or; A ~:bad; B ~:bad |] ==>
   5.137 -or3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" 
   5.138 -apply (erule or.induct)
   5.139 -(* Nil *)
   5.140 -apply simp_all
   5.141 -(* Fake *)
   5.142 -apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp)
   5.143 -(* OR1 *)
   5.144 -apply blast
   5.145 -(* OR2 *)
   5.146 -apply safe
   5.147 -apply (blast dest: Says_imp_spies, blast)
   5.148 -(* OR3 *)
   5.149 -apply blast
   5.150 -apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
   5.151 -apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
   5.152 -(* OR4 *)
   5.153 -by (blast dest: Says_imp_spies in_GuardK_kparts)
   5.154 -
   5.155 -subsection{*guardedness of NB*}
   5.156 -
   5.157 -lemma Guard_NB [rule_format]: "[| evs:or; B ~:bad |] ==>
   5.158 -or2 A B NA NB X:set evs --> Guard NB {shrK B} (spies evs)" 
   5.159 -apply (erule or.induct)
   5.160 -(* Nil *)
   5.161 -apply simp_all
   5.162 -(* Fake *)
   5.163 -apply safe
   5.164 -apply (erule in_synth_Guard, erule Guard_analz, simp)
   5.165 -(* OR1 *)
   5.166 -apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
   5.167 -apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
   5.168 -(* OR2 *)
   5.169 -apply blast
   5.170 -apply (drule_tac n=NA in Nonce_neq, simp+, rule No_Nonce, simp)
   5.171 -apply (blast intro!: No_Nonce dest: used_parts)
   5.172 -apply (drule_tac n=NA in Nonce_neq, simp+, rule No_Nonce, simp)
   5.173 -apply (blast intro!: No_Nonce dest: used_parts)
   5.174 -apply (blast dest: Says_imp_spies)
   5.175 -apply (blast dest: Says_imp_spies)
   5.176 -apply (case_tac "Ba=B", clarsimp)
   5.177 -apply (drule_tac n=NB and A=B in Nonce_neq, simp+)
   5.178 -apply (drule Says_imp_spies)
   5.179 -apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+, rule No_Nonce, simp)
   5.180 -(* OR3 *)
   5.181 -apply (drule Says_imp_spies)
   5.182 -apply (frule_tac n'=NAa in in_Guard_kparts_neq, simp+, rule No_Nonce, simp)
   5.183 -apply (case_tac "Aa=B", clarsimp)
   5.184 -apply (case_tac "NAa=NB", clarsimp)
   5.185 -apply (drule Says_imp_spies)
   5.186 -apply (drule_tac Y="{|Nonce NB, Agent Aa, Agent Ba|}"
   5.187 -                 and K="shrK Aa" in in_Guard_kparts_Crypt, simp+)
   5.188 -apply (simp add: No_Nonce) 
   5.189 -apply (case_tac "Ba=B", clarsimp)
   5.190 -apply (case_tac "NBa=NB", clarify)
   5.191 -apply (drule Says_imp_spies)
   5.192 -apply (drule_tac Y="{|Nonce NAa, Nonce NB, Agent Aa, Agent Ba|}"
   5.193 -                 and K="shrK Ba" in in_Guard_kparts_Crypt, simp+)
   5.194 -apply (simp add: No_Nonce) 
   5.195 -(* OR4 *)
   5.196 -by (blast dest: Says_imp_spies)+
   5.197 -
   5.198 -end
     6.1 --- a/src/HOL/Auth/Guard/Yahalom.thy	Wed Sep 14 23:06:02 2005 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,259 +0,0 @@
     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 -
    6.15 -header{*Yahalom Protocol*}
    6.16 -
    6.17 -theory Yahalom imports Guard_Shared begin
    6.18 -
    6.19 -subsection{*messages used in the protocol*}
    6.20 -
    6.21 -syntax ya1 :: "agent => agent => nat => event"
    6.22 -
    6.23 -translations "ya1 A B NA" => "Says A B {|Agent A, Nonce NA|}"
    6.24 -
    6.25 -syntax ya1' :: "agent => agent => agent => nat => event"
    6.26 -
    6.27 -translations "ya1' A' A B NA" => "Says A' B {|Agent A, Nonce NA|}"
    6.28 -
    6.29 -syntax ya2 :: "agent => agent => nat => nat => event"
    6.30 -
    6.31 -translations "ya2 A B NA NB"
    6.32 -=> "Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
    6.33 -
    6.34 -syntax ya2' :: "agent => agent => agent => nat => nat => event"
    6.35 -
    6.36 -translations "ya2' B' A B NA NB"
    6.37 -=> "Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
    6.38 -
    6.39 -syntax ya3 :: "agent => agent => nat => nat => key => event"
    6.40 -
    6.41 -translations "ya3 A B NA NB K"
    6.42 -=> "Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
    6.43 -                    Ciph B {|Agent A, Key K|}|}"
    6.44 -
    6.45 -syntax ya3':: "agent => msg => agent => agent => nat => nat => key => event"
    6.46 -
    6.47 -translations "ya3' S Y A B NA NB K"
    6.48 -=> "Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
    6.49 -
    6.50 -syntax ya4 :: "agent => agent => nat => nat => msg => event"
    6.51 -
    6.52 -translations "ya4 A B K NB Y" => "Says A B {|Y, Crypt K (Nonce NB)|}"
    6.53 -
    6.54 -syntax ya4' :: "agent => agent => nat => nat => msg => event"
    6.55 -
    6.56 -translations "ya4' A' B K NB Y" => "Says A' B {|Y, Crypt K (Nonce NB)|}"
    6.57 -
    6.58 -subsection{*definition of the protocol*}
    6.59 -
    6.60 -consts ya :: "event list set"
    6.61 -
    6.62 -inductive ya
    6.63 -intros
    6.64 -
    6.65 -Nil: "[]:ya"
    6.66 -
    6.67 -Fake: "[| evs:ya; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:ya"
    6.68 -
    6.69 -YA1: "[| evs1:ya; Nonce NA ~:used evs1 |] ==> ya1 A B NA # evs1:ya"
    6.70 -
    6.71 -YA2: "[| evs2:ya; ya1' A' A B NA:set evs2; Nonce NB ~:used evs2 |]
    6.72 -==> ya2 A B NA NB # evs2:ya"
    6.73 -
    6.74 -YA3: "[| evs3:ya; ya2' B' A B NA NB:set evs3; Key K ~:used evs3 |]
    6.75 -==> ya3 A B NA NB K # evs3:ya"
    6.76 -
    6.77 -YA4: "[| evs4:ya; ya1 A B NA:set evs4; ya3' S Y A B NA NB K:set evs4 |]
    6.78 -==> ya4 A B K NB Y # evs4:ya"
    6.79 -
    6.80 -subsection{*declarations for tactics*}
    6.81 -
    6.82 -declare knows_Spy_partsEs [elim]
    6.83 -declare Fake_parts_insert [THEN subsetD, dest]
    6.84 -declare initState.simps [simp del]
    6.85 -
    6.86 -subsection{*general properties of ya*}
    6.87 -
    6.88 -lemma ya_has_no_Gets: "evs:ya ==> ALL A X. Gets A X ~:set evs"
    6.89 -by (erule ya.induct, auto)
    6.90 -
    6.91 -lemma ya_is_Gets_correct [iff]: "Gets_correct ya"
    6.92 -by (auto simp: Gets_correct_def dest: ya_has_no_Gets)
    6.93 -
    6.94 -lemma ya_is_one_step [iff]: "one_step ya"
    6.95 -by (unfold one_step_def, clarify, ind_cases "ev#evs:ya", auto)
    6.96 -
    6.97 -lemma ya_has_only_Says' [rule_format]: "evs:ya ==>
    6.98 -ev:set evs --> (EX A B X. ev=Says A B X)"
    6.99 -by (erule ya.induct, auto)
   6.100 -
   6.101 -lemma ya_has_only_Says [iff]: "has_only_Says ya"
   6.102 -by (auto simp: has_only_Says_def dest: ya_has_only_Says')
   6.103 -
   6.104 -lemma ya_is_regular [iff]: "regular ya"
   6.105 -apply (simp only: regular_def, clarify)
   6.106 -apply (erule ya.induct, simp_all add: initState.simps knows.simps)
   6.107 -by (auto dest: parts_sub)
   6.108 -
   6.109 -subsection{*guardedness of KAB*}
   6.110 -
   6.111 -lemma Guard_KAB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
   6.112 -ya3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" 
   6.113 -apply (erule ya.induct)
   6.114 -(* Nil *)
   6.115 -apply simp_all
   6.116 -(* Fake *)
   6.117 -apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp)
   6.118 -(* YA1 *)
   6.119 -(* YA2 *)
   6.120 -apply safe
   6.121 -apply (blast dest: Says_imp_spies)
   6.122 -(* YA3 *)
   6.123 -apply blast
   6.124 -apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
   6.125 -apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
   6.126 -(* YA4 *)
   6.127 -apply (blast dest: Says_imp_spies in_GuardK_kparts)
   6.128 -by blast
   6.129 -
   6.130 -subsection{*session keys are not symmetric keys*}
   6.131 -
   6.132 -lemma KAB_isnt_shrK [rule_format]: "evs:ya ==>
   6.133 -ya3 A B NA NB K:set evs --> K ~:range shrK"
   6.134 -by (erule ya.induct, auto)
   6.135 -
   6.136 -lemma ya3_shrK: "evs:ya ==> ya3 A B NA NB (shrK C) ~:set evs"
   6.137 -by (blast dest: KAB_isnt_shrK)
   6.138 -
   6.139 -subsection{*ya2' implies ya1'*}
   6.140 -
   6.141 -lemma ya2'_parts_imp_ya1'_parts [rule_format]:
   6.142 -     "[| evs:ya; B ~:bad |] ==>
   6.143 -      Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
   6.144 -      {|Agent A, Nonce NA|}:spies evs"
   6.145 -by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts)
   6.146 -
   6.147 -lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB:set evs; evs:ya; B ~:bad |]
   6.148 -==> {|Agent A, Nonce NA|}:spies evs"
   6.149 -by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts)
   6.150 -
   6.151 -subsection{*uniqueness of NB*}
   6.152 -
   6.153 -lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs:ya; B ~:bad; B' ~:bad |] ==>
   6.154 -Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
   6.155 -Ciph B' {|Agent A', Nonce NA', Nonce NB|}:parts (spies evs) -->
   6.156 -A=A' & B=B' & NA=NA'"
   6.157 -apply (erule ya.induct, simp_all, clarify)
   6.158 -apply (drule Crypt_synth_insert, simp+)
   6.159 -apply (drule Crypt_synth_insert, simp+, safe)
   6.160 -apply (drule not_used_parts_false, simp+)+
   6.161 -by (drule Says_not_parts, simp+)+
   6.162 -
   6.163 -lemma NB_is_uniq_in_ya2': "[| ya2' C A B NA NB:set evs;
   6.164 -ya2' C' A' B' NA' NB:set evs; evs:ya; B ~:bad; B' ~:bad |]
   6.165 -==> A=A' & B=B' & NA=NA'"
   6.166 -by (drule NB_is_uniq_in_ya2'_parts, auto dest: Says_imp_spies)
   6.167 -
   6.168 -subsection{*ya3' implies ya2'*}
   6.169 -
   6.170 -lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs:ya; A ~:bad |] ==>
   6.171 -Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
   6.172 ---> Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs)"
   6.173 -apply (erule ya.induct, simp_all)
   6.174 -apply (clarify, drule Crypt_synth_insert, simp+)
   6.175 -apply (blast intro: parts_sub, blast)
   6.176 -by (auto dest: Says_imp_spies parts_parts)
   6.177 -
   6.178 -lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs:ya; A ~:bad |] ==>
   6.179 -Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
   6.180 ---> (EX B'. ya2' B' A B NA NB:set evs)"
   6.181 -apply (erule ya.induct, simp_all, safe)
   6.182 -apply (drule Crypt_synth_insert, simp+)
   6.183 -apply (drule Crypt_synth_insert, simp+, blast)
   6.184 -apply blast
   6.185 -apply blast
   6.186 -by (auto dest: Says_imp_spies2 parts_parts)
   6.187 -
   6.188 -lemma ya3'_imp_ya2': "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
   6.189 -==> (EX B'. ya2' B' A B NA NB:set evs)"
   6.190 -by (drule ya3'_parts_imp_ya2', auto dest: Says_imp_spies)
   6.191 -
   6.192 -subsection{*ya3' implies ya3*}
   6.193 -
   6.194 -lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs:ya; A ~:bad |] ==>
   6.195 -Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts(spies evs)
   6.196 ---> ya3 A B NA NB K:set evs"
   6.197 -apply (erule ya.induct, simp_all, safe)
   6.198 -apply (drule Crypt_synth_insert, simp+)
   6.199 -by (blast dest: Says_imp_spies2 parts_parts)
   6.200 -
   6.201 -lemma ya3'_imp_ya3: "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
   6.202 -==> ya3 A B NA NB K:set evs"
   6.203 -by (blast dest: Says_imp_spies ya3'_parts_imp_ya3)
   6.204 -
   6.205 -subsection{*guardedness of NB*}
   6.206 -
   6.207 -constdefs ya_keys :: "agent => agent => nat => nat => event list => key set"
   6.208 -"ya_keys A B NA NB evs == {shrK A,shrK B} Un {K. ya3 A B NA NB K:set evs}"
   6.209 -
   6.210 -lemma Guard_NB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
   6.211 -ya2 A B NA NB:set evs --> Guard NB (ya_keys A B NA NB evs) (spies evs)"
   6.212 -apply (erule ya.induct)
   6.213 -(* Nil *)
   6.214 -apply (simp_all add: ya_keys_def)
   6.215 -(* Fake *)
   6.216 -apply safe
   6.217 -apply (erule in_synth_Guard, erule Guard_analz, simp, clarify)
   6.218 -apply (frule_tac B=B in Guard_KAB, simp+)
   6.219 -apply (drule_tac p=ya in GuardK_Key_analz, simp+)
   6.220 -apply (blast dest: KAB_isnt_shrK, simp)
   6.221 -(* YA1 *)
   6.222 -apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
   6.223 -(* YA2 *)
   6.224 -apply blast
   6.225 -apply (drule Says_imp_spies)
   6.226 -apply (drule_tac n=NB in Nonce_neq, simp+)
   6.227 -apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+)
   6.228 -apply (rule No_Nonce, simp)
   6.229 -(* YA3 *)
   6.230 -apply (rule Guard_extand, simp, blast)
   6.231 -apply (case_tac "NAa=NB", clarify)
   6.232 -apply (frule Says_imp_spies)
   6.233 -apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
   6.234 -apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
   6.235 -apply (drule ya2'_imp_ya1'_parts, simp, blast, blast)
   6.236 -apply (case_tac "NBa=NB", clarify)
   6.237 -apply (frule Says_imp_spies)
   6.238 -apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
   6.239 -apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
   6.240 -apply (drule NB_is_uniq_in_ya2', simp+, blast, simp+)
   6.241 -apply (simp add: No_Nonce, blast)
   6.242 -(* YA4 *)
   6.243 -apply (blast dest: Says_imp_spies)
   6.244 -apply (case_tac "NBa=NB", clarify)
   6.245 -apply (frule_tac A=S in Says_imp_spies)
   6.246 -apply (frule in_Guard_kparts_Crypt, simp+)
   6.247 -apply (blast dest: Says_imp_spies)
   6.248 -apply (case_tac "NBa=NB", clarify)
   6.249 -apply (frule_tac A=S in Says_imp_spies)
   6.250 -apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
   6.251 -apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Aa in ya3_shrK, simp)
   6.252 -apply (frule ya3'_imp_ya2', simp+, blast, clarify)
   6.253 -apply (frule_tac A=B' in Says_imp_spies)
   6.254 -apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+, blast, simp+)
   6.255 -apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
   6.256 -apply (drule NB_is_uniq_in_ya2', simp+, blast, clarify)
   6.257 -apply (drule ya3'_imp_ya3, simp+)
   6.258 -apply (simp add: Guard_Nonce)
   6.259 -apply (simp add: No_Nonce)
   6.260 -done
   6.261 -
   6.262 -end
     7.1 --- a/src/HOL/Auth/ROOT.ML	Wed Sep 14 23:06:02 2005 +0200
     7.2 +++ b/src/HOL/Auth/ROOT.ML	Wed Sep 14 23:14:57 2005 +0200
     7.3 @@ -8,6 +8,8 @@
     7.4  
     7.5  no_document use_thy "NatPair";
     7.6  
     7.7 +add_path "Guard";
     7.8 +
     7.9  set timing;
    7.10  
    7.11  (*Shared-key protocols*)
    7.12 @@ -31,9 +33,9 @@
    7.13  time_use_thy "CertifiedEmail";
    7.14  
    7.15  (*Blanqui's "guard" concept: protocol-independent secrecy*)
    7.16 -time_use_thy "Guard/P1";
    7.17 -time_use_thy "Guard/P2";
    7.18 -time_use_thy "Guard/NS_Public";
    7.19 -time_use_thy "Guard/OtwayRees";
    7.20 -time_use_thy "Guard/Yahalom";
    7.21 -time_use_thy "Guard/Proto";
    7.22 +time_use_thy "P1";
    7.23 +time_use_thy "P2";
    7.24 +time_use_thy "Guard_NS_Public";
    7.25 +time_use_thy "Guard_OtwayRees";
    7.26 +time_use_thy "Guard_Yahalom";
    7.27 +time_use_thy "Proto";
     8.1 --- a/src/HOL/IsaMakefile	Wed Sep 14 23:06:02 2005 +0200
     8.2 +++ b/src/HOL/IsaMakefile	Wed Sep 14 23:14:57 2005 +0200
     8.3 @@ -390,9 +390,9 @@
     8.4    Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \
     8.5    Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \
     8.6    Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \
     8.7 -  Auth/Guard/NS_Public.thy Auth/Guard/OtwayRees.thy \
     8.8 +  Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy \
     8.9    Auth/Guard/P1.thy Auth/Guard/P2.thy \
    8.10 -  Auth/Guard/Proto.thy Auth/Guard/Yahalom.thy\
    8.11 +  Auth/Guard/Proto.thy Auth/Guard/Guard_Yahalom.thy\
    8.12    Auth/document/root.tex 
    8.13  	@$(ISATOOL) usedir -g true $(OUT)/HOL Auth
    8.14