isabelle: changeset 17394:a8c9ed3f9818

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy	Wed Sep 14 23:14:57 2005 +0200
@@ -0,0 +1,204 @@
+(******************************************************************************
+incorporating Lowe's fix (inclusion of B's identity in round 2)
+
+date: march 2002
+author: Frederic Blanqui
+email: blanqui@lri.fr
+webpage: http://www.lri.fr/~blanqui/
+
+University of Cambridge, Computer Laboratory
+William Gates Building, JJ Thomson Avenue
+Cambridge CB3 0FD, United Kingdom
+******************************************************************************)
+
+header{*Needham-Schroeder-Lowe Public-Key Protocol*}
+
+theory Guard_NS_Public imports Guard_Public begin
+
+subsection{*messages used in the protocol*}
+
+syntax ns1 :: "agent => agent => nat => event"
+
+translations "ns1 A B NA" => "Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
+
+syntax ns1' :: "agent => agent => agent => nat => event"
+
+translations "ns1' A' A B NA"
+=> "Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
+
+syntax ns2 :: "agent => agent => nat => nat => event"
+
+translations "ns2 B A NA NB"
+=> "Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
+
+syntax ns2' :: "agent => agent => agent => nat => nat => event"
+
+translations "ns2' B' B A NA NB"
+=> "Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
+
+syntax ns3 :: "agent => agent => nat => event"
+
+translations "ns3 A B NB" => "Says A B (Crypt (pubK B) (Nonce NB))"
+
+subsection{*definition of the protocol*}
+
+consts nsp :: "event list set"
+
+inductive nsp
+intros
+
+Nil: "[]:nsp"
+
+Fake: "[| evs:nsp; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs : nsp"
+
+NS1: "[| evs1:nsp; Nonce NA ~:used evs1 |] ==> ns1 A B NA # evs1 : nsp"
+
+NS2: "[| evs2:nsp; Nonce NB ~:used evs2; ns1' A' A B NA:set evs2 |] ==>
+ns2 B A NA NB # evs2:nsp"
+
+NS3: "[| evs3:nsp; ns1 A B NA:set evs3; ns2' B' B A NA NB:set evs3 |] ==>
+ns3 A B NB # evs3:nsp"
+
+subsection{*declarations for tactics*}
+
+declare knows_Spy_partsEs [elim]
+declare Fake_parts_insert [THEN subsetD, dest]
+declare initState.simps [simp del]
+
+subsection{*general properties of nsp*}
+
+lemma nsp_has_no_Gets: "evs:nsp ==> ALL A X. Gets A X ~:set evs"
+by (erule nsp.induct, auto)
+
+lemma nsp_is_Gets_correct [iff]: "Gets_correct nsp"
+by (auto simp: Gets_correct_def dest: nsp_has_no_Gets)
+
+lemma nsp_is_one_step [iff]: "one_step nsp"
+by (unfold one_step_def, clarify, ind_cases "ev#evs:nsp", auto)
+
+lemma nsp_has_only_Says' [rule_format]: "evs:nsp ==>
+ev:set evs --> (EX A B X. ev=Says A B X)"
+by (erule nsp.induct, auto)
+
+lemma nsp_has_only_Says [iff]: "has_only_Says nsp"
+by (auto simp: has_only_Says_def dest: nsp_has_only_Says')
+
+lemma nsp_is_regular [iff]: "regular nsp"
+apply (simp only: regular_def, clarify)
+by (erule nsp.induct, auto simp: initState.simps knows.simps)
+
+subsection{*nonce are used only once*}
+
+lemma NA_is_uniq [rule_format]: "evs:nsp ==>
+Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
+--> Crypt (pubK B') {|Nonce NA, Agent A'|}:parts (spies evs)
+--> Nonce NA ~:analz (spies evs) --> A=A' & B=B'"
+apply (erule nsp.induct, simp_all)
+by (blast intro: analz_insertI)+
+
+lemma no_Nonce_NS1_NS2 [rule_format]: "evs:nsp ==>
+Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs)
+--> Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
+--> Nonce NA:analz (spies evs)"
+apply (erule nsp.induct, simp_all)
+by (blast intro: analz_insertI)+
+
+lemma no_Nonce_NS1_NS2' [rule_format]:
+"[| Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs);
+Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs); evs:nsp |]
+==> Nonce NA:analz (spies evs)"
+by (rule no_Nonce_NS1_NS2, auto)
+ 
+lemma NB_is_uniq [rule_format]: "evs:nsp ==>
+Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
+--> Crypt (pubK A') {|Nonce NA', Nonce NB, Agent B'|}:parts (spies evs)
+--> Nonce NB ~:analz (spies evs) --> A=A' & B=B' & NA=NA'"
+apply (erule nsp.induct, simp_all)
+by (blast intro: analz_insertI)+
+
+subsection{*guardedness of NA*}
+
+lemma ns1_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
+ns1 A B NA:set evs --> Guard NA {priK A,priK B} (spies evs)"
+apply (erule nsp.induct)
+(* Nil *)
+apply simp_all
+(* Fake *)
+apply safe
+apply (erule in_synth_Guard, erule Guard_analz, simp)
+(* NS1 *)
+apply blast
+apply blast
+apply blast
+apply (drule Nonce_neq, simp+, rule No_Nonce, simp)
+(* NS2 *)
+apply (frule_tac A=A in Nonce_neq, simp+)
+apply (case_tac "NAa=NA")
+apply (drule Guard_Nonce_analz, simp+)
+apply (drule Says_imp_knows_Spy)+
+apply (drule_tac B=B and A'=Aa in NA_is_uniq, auto)
+(* NS3 *)
+apply (case_tac "NB=NA", clarify)
+apply (drule Guard_Nonce_analz, simp+)
+apply (drule Says_imp_knows_Spy)+
+by (drule no_Nonce_NS1_NS2, auto)
+
+subsection{*guardedness of NB*}
+
+lemma ns2_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
+ns2 B A NA NB:set evs --> Guard NB {priK A,priK B} (spies evs)" 
+apply (erule nsp.induct)
+(* Nil *)
+apply simp_all
+(* Fake *)
+apply safe
+apply (erule in_synth_Guard, erule Guard_analz, simp)
+(* NS1 *)
+apply (frule Nonce_neq, simp+, blast, rule No_Nonce, simp)
+(* NS2 *)
+apply blast
+apply blast
+apply blast
+apply (frule_tac A=B and n=NB in Nonce_neq, simp+)
+apply (case_tac "NAa=NB")
+apply (drule Guard_Nonce_analz, simp+)
+apply (drule Says_imp_knows_Spy)+
+apply (drule no_Nonce_NS1_NS2, auto)
+(* NS3 *)
+apply (case_tac "NBa=NB", clarify)
+apply (drule Guard_Nonce_analz, simp+)
+apply (drule Says_imp_knows_Spy)+
+by (drule_tac A=Aa and A'=A in NB_is_uniq, auto)
+
+subsection{*Agents' Authentication*}
+
+lemma B_trusts_NS1: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
+Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
+--> Nonce NA ~:analz (spies evs) --> ns1 A B NA:set evs"
+apply (erule nsp.induct, simp_all)
+by (blast intro: analz_insertI)+
+
+lemma A_trusts_NS2: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns1 A B NA:set evs
+--> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
+--> ns2 B A NA NB:set evs"
+apply (erule nsp.induct, simp_all, safe)
+apply (frule_tac B=B in ns1_imp_Guard, simp+)
+apply (drule Guard_Nonce_analz, simp+, blast)
+apply (frule_tac B=B in ns1_imp_Guard, simp+)
+apply (drule Guard_Nonce_analz, simp+, blast)
+apply (frule_tac B=B in ns1_imp_Guard, simp+)
+by (drule Guard_Nonce_analz, simp+, blast+)
+
+lemma B_trusts_NS3: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns2 B A NA NB:set evs
+--> Crypt (pubK B) (Nonce NB):parts (spies evs) --> ns3 A B NB:set evs"
+apply (erule nsp.induct, simp_all, safe)
+apply (frule_tac B=B in ns2_imp_Guard, simp+)
+apply (drule Guard_Nonce_analz, simp+, blast)
+apply (frule_tac B=B in ns2_imp_Guard, simp+)
+apply (drule Guard_Nonce_analz, simp+, blast)
+apply (frule_tac B=B in ns2_imp_Guard, simp+)
+apply (drule Guard_Nonce_analz, simp+, blast, blast)
+apply (frule_tac B=B in ns2_imp_Guard, simp+)
+by (drule Guard_Nonce_analz, auto dest: Says_imp_knows_Spy NB_is_uniq)
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Wed Sep 14 23:14:57 2005 +0200
@@ -0,0 +1,195 @@
+(******************************************************************************
+date: march 2002
+author: Frederic Blanqui
+email: blanqui@lri.fr
+webpage: http://www.lri.fr/~blanqui/
+
+University of Cambridge, Computer Laboratory
+William Gates Building, JJ Thomson Avenue
+Cambridge CB3 0FD, United Kingdom
+******************************************************************************)
+
+header{*Otway-Rees Protocol*}
+
+theory Guard_OtwayRees imports Guard_Shared begin
+
+subsection{*messages used in the protocol*}
+
+syntax nil :: "msg"
+
+translations "nil" == "Number 0"
+
+syntax or1 :: "agent => agent => nat => event"
+
+translations "or1 A B NA"
+=> "Says A B {|Nonce NA, Agent A, Agent B,
+               Ciph A {|Nonce NA, Agent A, Agent B|}|}"
+
+syntax or1' :: "agent => agent => agent => nat => msg => event"
+
+translations "or1' A' A B NA X"
+=> "Says A' B {|Nonce NA, Agent A, Agent B, X|}"
+
+syntax or2 :: "agent => agent => nat => nat => msg => event"
+
+translations "or2 A B NA NB X"
+=> "Says B Server {|Nonce NA, Agent A, Agent B, X,
+                    Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
+
+syntax or2' :: "agent => agent => agent => nat => nat => event"
+
+translations "or2' B' A B NA NB"
+=> "Says B' Server {|Nonce NA, Agent A, Agent B,
+                     Ciph A {|Nonce NA, Agent A, Agent B|},
+                     Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
+
+syntax or3 :: "agent => agent => nat => nat => key => event"
+
+translations "or3 A B NA NB K"
+=> "Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|},
+                    Ciph B {|Nonce NB, Key K|}|}"
+
+syntax or3':: "agent => msg => agent => agent => nat => nat => key => event"
+
+translations "or3' S Y A B NA NB K"
+=> "Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}"
+
+syntax or4 :: "agent => agent => nat => msg => event"
+
+translations "or4 A B NA X" => "Says B A {|Nonce NA, X, nil|}"
+
+syntax or4' :: "agent => agent => nat => msg => event"
+
+translations "or4' B' A NA K" =>
+"Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}"
+
+subsection{*definition of the protocol*}
+
+consts or :: "event list set"
+
+inductive or
+intros
+
+Nil: "[]:or"
+
+Fake: "[| evs:or; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:or"
+
+OR1: "[| evs1:or; Nonce NA ~:used evs1 |] ==> or1 A B NA # evs1:or"
+
+OR2: "[| evs2:or; or1' A' A B NA X:set evs2; Nonce NB ~:used evs2 |]
+==> or2 A B NA NB X # evs2:or"
+
+OR3: "[| evs3:or; or2' B' A B NA NB:set evs3; Key K ~:used evs3 |]
+==> or3 A B NA NB K # evs3:or"
+
+OR4: "[| evs4:or; or2 A B NA NB X:set evs4; or3' S Y A B NA NB K:set evs4 |]
+==> or4 A B NA X # evs4:or"
+
+subsection{*declarations for tactics*}
+
+declare knows_Spy_partsEs [elim]
+declare Fake_parts_insert [THEN subsetD, dest]
+declare initState.simps [simp del]
+
+subsection{*general properties of or*}
+
+lemma or_has_no_Gets: "evs:or ==> ALL A X. Gets A X ~:set evs"
+by (erule or.induct, auto)
+
+lemma or_is_Gets_correct [iff]: "Gets_correct or"
+by (auto simp: Gets_correct_def dest: or_has_no_Gets)
+
+lemma or_is_one_step [iff]: "one_step or"
+by (unfold one_step_def, clarify, ind_cases "ev#evs:or", auto)
+
+lemma or_has_only_Says' [rule_format]: "evs:or ==>
+ev:set evs --> (EX A B X. ev=Says A B X)"
+by (erule or.induct, auto)
+
+lemma or_has_only_Says [iff]: "has_only_Says or"
+by (auto simp: has_only_Says_def dest: or_has_only_Says')
+
+subsection{*or is regular*}
+
+lemma or1'_parts_spies [dest]: "or1' A' A B NA X:set evs
+==> X:parts (spies evs)"
+by blast
+
+lemma or2_parts_spies [dest]: "or2 A B NA NB X:set evs
+==> X:parts (spies evs)"
+by blast
+
+lemma or3_parts_spies [dest]: "Says S B {|NA, Y, Ciph B {|NB, K|}|}:set evs
+==> K:parts (spies evs)"
+by blast
+
+lemma or_is_regular [iff]: "regular or"
+apply (simp only: regular_def, clarify)
+apply (erule or.induct, simp_all add: initState.simps knows.simps)
+by (auto dest: parts_sub)
+
+subsection{*guardedness of KAB*}
+
+lemma Guard_KAB [rule_format]: "[| evs:or; A ~:bad; B ~:bad |] ==>
+or3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" 
+apply (erule or.induct)
+(* Nil *)
+apply simp_all
+(* Fake *)
+apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp)
+(* OR1 *)
+apply blast
+(* OR2 *)
+apply safe
+apply (blast dest: Says_imp_spies, blast)
+(* OR3 *)
+apply blast
+apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
+apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
+(* OR4 *)
+by (blast dest: Says_imp_spies in_GuardK_kparts)
+
+subsection{*guardedness of NB*}
+
+lemma Guard_NB [rule_format]: "[| evs:or; B ~:bad |] ==>
+or2 A B NA NB X:set evs --> Guard NB {shrK B} (spies evs)" 
+apply (erule or.induct)
+(* Nil *)
+apply simp_all
+(* Fake *)
+apply safe
+apply (erule in_synth_Guard, erule Guard_analz, simp)
+(* OR1 *)
+apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
+apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
+(* OR2 *)
+apply blast
+apply (drule_tac n=NA in Nonce_neq, simp+, rule No_Nonce, simp)
+apply (blast intro!: No_Nonce dest: used_parts)
+apply (drule_tac n=NA in Nonce_neq, simp+, rule No_Nonce, simp)
+apply (blast intro!: No_Nonce dest: used_parts)
+apply (blast dest: Says_imp_spies)
+apply (blast dest: Says_imp_spies)
+apply (case_tac "Ba=B", clarsimp)
+apply (drule_tac n=NB and A=B in Nonce_neq, simp+)
+apply (drule Says_imp_spies)
+apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+, rule No_Nonce, simp)
+(* OR3 *)
+apply (drule Says_imp_spies)
+apply (frule_tac n'=NAa in in_Guard_kparts_neq, simp+, rule No_Nonce, simp)
+apply (case_tac "Aa=B", clarsimp)
+apply (case_tac "NAa=NB", clarsimp)
+apply (drule Says_imp_spies)
+apply (drule_tac Y="{|Nonce NB, Agent Aa, Agent Ba|}"
+                 and K="shrK Aa" in in_Guard_kparts_Crypt, simp+)
+apply (simp add: No_Nonce) 
+apply (case_tac "Ba=B", clarsimp)
+apply (case_tac "NBa=NB", clarify)
+apply (drule Says_imp_spies)
+apply (drule_tac Y="{|Nonce NAa, Nonce NB, Agent Aa, Agent Ba|}"
+                 and K="shrK Ba" in in_Guard_kparts_Crypt, simp+)
+apply (simp add: No_Nonce) 
+(* OR4 *)
+by (blast dest: Says_imp_spies)+
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy	Wed Sep 14 23:14:57 2005 +0200
@@ -0,0 +1,259 @@
+(******************************************************************************
+date: march 2002
+author: Frederic Blanqui
+email: blanqui@lri.fr
+webpage: http://www.lri.fr/~blanqui/
+
+University of Cambridge, Computer Laboratory
+William Gates Building, JJ Thomson Avenue
+Cambridge CB3 0FD, United Kingdom
+******************************************************************************)
+
+header{*Yahalom Protocol*}
+
+theory Guard_Yahalom imports Guard_Shared begin
+
+subsection{*messages used in the protocol*}
+
+syntax ya1 :: "agent => agent => nat => event"
+
+translations "ya1 A B NA" => "Says A B {|Agent A, Nonce NA|}"
+
+syntax ya1' :: "agent => agent => agent => nat => event"
+
+translations "ya1' A' A B NA" => "Says A' B {|Agent A, Nonce NA|}"
+
+syntax ya2 :: "agent => agent => nat => nat => event"
+
+translations "ya2 A B NA NB"
+=> "Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
+
+syntax ya2' :: "agent => agent => agent => nat => nat => event"
+
+translations "ya2' B' A B NA NB"
+=> "Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
+
+syntax ya3 :: "agent => agent => nat => nat => key => event"
+
+translations "ya3 A B NA NB K"
+=> "Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
+                    Ciph B {|Agent A, Key K|}|}"
+
+syntax ya3':: "agent => msg => agent => agent => nat => nat => key => event"
+
+translations "ya3' S Y A B NA NB K"
+=> "Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
+
+syntax ya4 :: "agent => agent => nat => nat => msg => event"
+
+translations "ya4 A B K NB Y" => "Says A B {|Y, Crypt K (Nonce NB)|}"
+
+syntax ya4' :: "agent => agent => nat => nat => msg => event"
+
+translations "ya4' A' B K NB Y" => "Says A' B {|Y, Crypt K (Nonce NB)|}"
+
+subsection{*definition of the protocol*}
+
+consts ya :: "event list set"
+
+inductive ya
+intros
+
+Nil: "[]:ya"
+
+Fake: "[| evs:ya; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:ya"
+
+YA1: "[| evs1:ya; Nonce NA ~:used evs1 |] ==> ya1 A B NA # evs1:ya"
+
+YA2: "[| evs2:ya; ya1' A' A B NA:set evs2; Nonce NB ~:used evs2 |]
+==> ya2 A B NA NB # evs2:ya"
+
+YA3: "[| evs3:ya; ya2' B' A B NA NB:set evs3; Key K ~:used evs3 |]
+==> ya3 A B NA NB K # evs3:ya"
+
+YA4: "[| evs4:ya; ya1 A B NA:set evs4; ya3' S Y A B NA NB K:set evs4 |]
+==> ya4 A B K NB Y # evs4:ya"
+
+subsection{*declarations for tactics*}
+
+declare knows_Spy_partsEs [elim]
+declare Fake_parts_insert [THEN subsetD, dest]
+declare initState.simps [simp del]
+
+subsection{*general properties of ya*}
+
+lemma ya_has_no_Gets: "evs:ya ==> ALL A X. Gets A X ~:set evs"
+by (erule ya.induct, auto)
+
+lemma ya_is_Gets_correct [iff]: "Gets_correct ya"
+by (auto simp: Gets_correct_def dest: ya_has_no_Gets)
+
+lemma ya_is_one_step [iff]: "one_step ya"
+by (unfold one_step_def, clarify, ind_cases "ev#evs:ya", auto)
+
+lemma ya_has_only_Says' [rule_format]: "evs:ya ==>
+ev:set evs --> (EX A B X. ev=Says A B X)"
+by (erule ya.induct, auto)
+
+lemma ya_has_only_Says [iff]: "has_only_Says ya"
+by (auto simp: has_only_Says_def dest: ya_has_only_Says')
+
+lemma ya_is_regular [iff]: "regular ya"
+apply (simp only: regular_def, clarify)
+apply (erule ya.induct, simp_all add: initState.simps knows.simps)
+by (auto dest: parts_sub)
+
+subsection{*guardedness of KAB*}
+
+lemma Guard_KAB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
+ya3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" 
+apply (erule ya.induct)
+(* Nil *)
+apply simp_all
+(* Fake *)
+apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp)
+(* YA1 *)
+(* YA2 *)
+apply safe
+apply (blast dest: Says_imp_spies)
+(* YA3 *)
+apply blast
+apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
+apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
+(* YA4 *)
+apply (blast dest: Says_imp_spies in_GuardK_kparts)
+by blast
+
+subsection{*session keys are not symmetric keys*}
+
+lemma KAB_isnt_shrK [rule_format]: "evs:ya ==>
+ya3 A B NA NB K:set evs --> K ~:range shrK"
+by (erule ya.induct, auto)
+
+lemma ya3_shrK: "evs:ya ==> ya3 A B NA NB (shrK C) ~:set evs"
+by (blast dest: KAB_isnt_shrK)
+
+subsection{*ya2' implies ya1'*}
+
+lemma ya2'_parts_imp_ya1'_parts [rule_format]:
+     "[| evs:ya; B ~:bad |] ==>
+      Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
+      {|Agent A, Nonce NA|}:spies evs"
+by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts)
+
+lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB:set evs; evs:ya; B ~:bad |]
+==> {|Agent A, Nonce NA|}:spies evs"
+by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts)
+
+subsection{*uniqueness of NB*}
+
+lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs:ya; B ~:bad; B' ~:bad |] ==>
+Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
+Ciph B' {|Agent A', Nonce NA', Nonce NB|}:parts (spies evs) -->
+A=A' & B=B' & NA=NA'"
+apply (erule ya.induct, simp_all, clarify)
+apply (drule Crypt_synth_insert, simp+)
+apply (drule Crypt_synth_insert, simp+, safe)
+apply (drule not_used_parts_false, simp+)+
+by (drule Says_not_parts, simp+)+
+
+lemma NB_is_uniq_in_ya2': "[| ya2' C A B NA NB:set evs;
+ya2' C' A' B' NA' NB:set evs; evs:ya; B ~:bad; B' ~:bad |]
+==> A=A' & B=B' & NA=NA'"
+by (drule NB_is_uniq_in_ya2'_parts, auto dest: Says_imp_spies)
+
+subsection{*ya3' implies ya2'*}
+
+lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs:ya; A ~:bad |] ==>
+Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
+--> Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs)"
+apply (erule ya.induct, simp_all)
+apply (clarify, drule Crypt_synth_insert, simp+)
+apply (blast intro: parts_sub, blast)
+by (auto dest: Says_imp_spies parts_parts)
+
+lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs:ya; A ~:bad |] ==>
+Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
+--> (EX B'. ya2' B' A B NA NB:set evs)"
+apply (erule ya.induct, simp_all, safe)
+apply (drule Crypt_synth_insert, simp+)
+apply (drule Crypt_synth_insert, simp+, blast)
+apply blast
+apply blast
+by (auto dest: Says_imp_spies2 parts_parts)
+
+lemma ya3'_imp_ya2': "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
+==> (EX B'. ya2' B' A B NA NB:set evs)"
+by (drule ya3'_parts_imp_ya2', auto dest: Says_imp_spies)
+
+subsection{*ya3' implies ya3*}
+
+lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs:ya; A ~:bad |] ==>
+Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts(spies evs)
+--> ya3 A B NA NB K:set evs"
+apply (erule ya.induct, simp_all, safe)
+apply (drule Crypt_synth_insert, simp+)
+by (blast dest: Says_imp_spies2 parts_parts)
+
+lemma ya3'_imp_ya3: "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
+==> ya3 A B NA NB K:set evs"
+by (blast dest: Says_imp_spies ya3'_parts_imp_ya3)
+
+subsection{*guardedness of NB*}
+
+constdefs ya_keys :: "agent => agent => nat => nat => event list => key set"
+"ya_keys A B NA NB evs == {shrK A,shrK B} Un {K. ya3 A B NA NB K:set evs}"
+
+lemma Guard_NB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
+ya2 A B NA NB:set evs --> Guard NB (ya_keys A B NA NB evs) (spies evs)"
+apply (erule ya.induct)
+(* Nil *)
+apply (simp_all add: ya_keys_def)
+(* Fake *)
+apply safe
+apply (erule in_synth_Guard, erule Guard_analz, simp, clarify)
+apply (frule_tac B=B in Guard_KAB, simp+)
+apply (drule_tac p=ya in GuardK_Key_analz, simp+)
+apply (blast dest: KAB_isnt_shrK, simp)
+(* YA1 *)
+apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
+(* YA2 *)
+apply blast
+apply (drule Says_imp_spies)
+apply (drule_tac n=NB in Nonce_neq, simp+)
+apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+)
+apply (rule No_Nonce, simp)
+(* YA3 *)
+apply (rule Guard_extand, simp, blast)
+apply (case_tac "NAa=NB", clarify)
+apply (frule Says_imp_spies)
+apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
+apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
+apply (drule ya2'_imp_ya1'_parts, simp, blast, blast)
+apply (case_tac "NBa=NB", clarify)
+apply (frule Says_imp_spies)
+apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
+apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
+apply (drule NB_is_uniq_in_ya2', simp+, blast, simp+)
+apply (simp add: No_Nonce, blast)
+(* YA4 *)
+apply (blast dest: Says_imp_spies)
+apply (case_tac "NBa=NB", clarify)
+apply (frule_tac A=S in Says_imp_spies)
+apply (frule in_Guard_kparts_Crypt, simp+)
+apply (blast dest: Says_imp_spies)
+apply (case_tac "NBa=NB", clarify)
+apply (frule_tac A=S in Says_imp_spies)
+apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
+apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Aa in ya3_shrK, simp)
+apply (frule ya3'_imp_ya2', simp+, blast, clarify)
+apply (frule_tac A=B' in Says_imp_spies)
+apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+, blast, simp+)
+apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
+apply (drule NB_is_uniq_in_ya2', simp+, blast, clarify)
+apply (drule ya3'_imp_ya3, simp+)
+apply (simp add: Guard_Nonce)
+apply (simp add: No_Nonce)
+done
+
+end

--- a/src/HOL/Auth/Guard/NS_Public.thy	Wed Sep 14 23:06:02 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,204 +0,0 @@
-(******************************************************************************
-incorporating Lowe's fix (inclusion of B's identity in round 2)
-
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
-
-header{*Needham-Schroeder-Lowe Public-Key Protocol*}
-
-theory NS_Public imports Guard_Public begin
-
-subsection{*messages used in the protocol*}
-
-syntax ns1 :: "agent => agent => nat => event"
-
-translations "ns1 A B NA" => "Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
-
-syntax ns1' :: "agent => agent => agent => nat => event"
-
-translations "ns1' A' A B NA"
-=> "Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
-
-syntax ns2 :: "agent => agent => nat => nat => event"
-
-translations "ns2 B A NA NB"
-=> "Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
-
-syntax ns2' :: "agent => agent => agent => nat => nat => event"
-
-translations "ns2' B' B A NA NB"
-=> "Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
-
-syntax ns3 :: "agent => agent => nat => event"
-
-translations "ns3 A B NB" => "Says A B (Crypt (pubK B) (Nonce NB))"
-
-subsection{*definition of the protocol*}
-
-consts nsp :: "event list set"
-
-inductive nsp
-intros
-
-Nil: "[]:nsp"
-
-Fake: "[| evs:nsp; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs : nsp"
-
-NS1: "[| evs1:nsp; Nonce NA ~:used evs1 |] ==> ns1 A B NA # evs1 : nsp"
-
-NS2: "[| evs2:nsp; Nonce NB ~:used evs2; ns1' A' A B NA:set evs2 |] ==>
-ns2 B A NA NB # evs2:nsp"
-
-NS3: "[| evs3:nsp; ns1 A B NA:set evs3; ns2' B' B A NA NB:set evs3 |] ==>
-ns3 A B NB # evs3:nsp"
-
-subsection{*declarations for tactics*}
-
-declare knows_Spy_partsEs [elim]
-declare Fake_parts_insert [THEN subsetD, dest]
-declare initState.simps [simp del]
-
-subsection{*general properties of nsp*}
-
-lemma nsp_has_no_Gets: "evs:nsp ==> ALL A X. Gets A X ~:set evs"
-by (erule nsp.induct, auto)
-
-lemma nsp_is_Gets_correct [iff]: "Gets_correct nsp"
-by (auto simp: Gets_correct_def dest: nsp_has_no_Gets)
-
-lemma nsp_is_one_step [iff]: "one_step nsp"
-by (unfold one_step_def, clarify, ind_cases "ev#evs:nsp", auto)
-
-lemma nsp_has_only_Says' [rule_format]: "evs:nsp ==>
-ev:set evs --> (EX A B X. ev=Says A B X)"
-by (erule nsp.induct, auto)
-
-lemma nsp_has_only_Says [iff]: "has_only_Says nsp"
-by (auto simp: has_only_Says_def dest: nsp_has_only_Says')
-
-lemma nsp_is_regular [iff]: "regular nsp"
-apply (simp only: regular_def, clarify)
-by (erule nsp.induct, auto simp: initState.simps knows.simps)
-
-subsection{*nonce are used only once*}
-
-lemma NA_is_uniq [rule_format]: "evs:nsp ==>
-Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
---> Crypt (pubK B') {|Nonce NA, Agent A'|}:parts (spies evs)
---> Nonce NA ~:analz (spies evs) --> A=A' & B=B'"
-apply (erule nsp.induct, simp_all)
-by (blast intro: analz_insertI)+
-
-lemma no_Nonce_NS1_NS2 [rule_format]: "evs:nsp ==>
-Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs)
---> Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
---> Nonce NA:analz (spies evs)"
-apply (erule nsp.induct, simp_all)
-by (blast intro: analz_insertI)+
-
-lemma no_Nonce_NS1_NS2' [rule_format]:
-"[| Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs);
-Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs); evs:nsp |]
-==> Nonce NA:analz (spies evs)"
-by (rule no_Nonce_NS1_NS2, auto)
- 
-lemma NB_is_uniq [rule_format]: "evs:nsp ==>
-Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
---> Crypt (pubK A') {|Nonce NA', Nonce NB, Agent B'|}:parts (spies evs)
---> Nonce NB ~:analz (spies evs) --> A=A' & B=B' & NA=NA'"
-apply (erule nsp.induct, simp_all)
-by (blast intro: analz_insertI)+
-
-subsection{*guardedness of NA*}
-
-lemma ns1_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
-ns1 A B NA:set evs --> Guard NA {priK A,priK B} (spies evs)"
-apply (erule nsp.induct)
-(* Nil *)
-apply simp_all
-(* Fake *)
-apply safe
-apply (erule in_synth_Guard, erule Guard_analz, simp)
-(* NS1 *)
-apply blast
-apply blast
-apply blast
-apply (drule Nonce_neq, simp+, rule No_Nonce, simp)
-(* NS2 *)
-apply (frule_tac A=A in Nonce_neq, simp+)
-apply (case_tac "NAa=NA")
-apply (drule Guard_Nonce_analz, simp+)
-apply (drule Says_imp_knows_Spy)+
-apply (drule_tac B=B and A'=Aa in NA_is_uniq, auto)
-(* NS3 *)
-apply (case_tac "NB=NA", clarify)
-apply (drule Guard_Nonce_analz, simp+)
-apply (drule Says_imp_knows_Spy)+
-by (drule no_Nonce_NS1_NS2, auto)
-
-subsection{*guardedness of NB*}
-
-lemma ns2_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
-ns2 B A NA NB:set evs --> Guard NB {priK A,priK B} (spies evs)" 
-apply (erule nsp.induct)
-(* Nil *)
-apply simp_all
-(* Fake *)
-apply safe
-apply (erule in_synth_Guard, erule Guard_analz, simp)
-(* NS1 *)
-apply (frule Nonce_neq, simp+, blast, rule No_Nonce, simp)
-(* NS2 *)
-apply blast
-apply blast
-apply blast
-apply (frule_tac A=B and n=NB in Nonce_neq, simp+)
-apply (case_tac "NAa=NB")
-apply (drule Guard_Nonce_analz, simp+)
-apply (drule Says_imp_knows_Spy)+
-apply (drule no_Nonce_NS1_NS2, auto)
-(* NS3 *)
-apply (case_tac "NBa=NB", clarify)
-apply (drule Guard_Nonce_analz, simp+)
-apply (drule Says_imp_knows_Spy)+
-by (drule_tac A=Aa and A'=A in NB_is_uniq, auto)
-
-subsection{*Agents' Authentication*}
-
-lemma B_trusts_NS1: "[| evs:nsp; A ~:bad; B ~:bad |] ==>
-Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs)
---> Nonce NA ~:analz (spies evs) --> ns1 A B NA:set evs"
-apply (erule nsp.induct, simp_all)
-by (blast intro: analz_insertI)+
-
-lemma A_trusts_NS2: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns1 A B NA:set evs
---> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs)
---> ns2 B A NA NB:set evs"
-apply (erule nsp.induct, simp_all, safe)
-apply (frule_tac B=B in ns1_imp_Guard, simp+)
-apply (drule Guard_Nonce_analz, simp+, blast)
-apply (frule_tac B=B in ns1_imp_Guard, simp+)
-apply (drule Guard_Nonce_analz, simp+, blast)
-apply (frule_tac B=B in ns1_imp_Guard, simp+)
-by (drule Guard_Nonce_analz, simp+, blast+)
-
-lemma B_trusts_NS3: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns2 B A NA NB:set evs
---> Crypt (pubK B) (Nonce NB):parts (spies evs) --> ns3 A B NB:set evs"
-apply (erule nsp.induct, simp_all, safe)
-apply (frule_tac B=B in ns2_imp_Guard, simp+)
-apply (drule Guard_Nonce_analz, simp+, blast)
-apply (frule_tac B=B in ns2_imp_Guard, simp+)
-apply (drule Guard_Nonce_analz, simp+, blast)
-apply (frule_tac B=B in ns2_imp_Guard, simp+)
-apply (drule Guard_Nonce_analz, simp+, blast, blast)
-apply (frule_tac B=B in ns2_imp_Guard, simp+)
-by (drule Guard_Nonce_analz, auto dest: Says_imp_knows_Spy NB_is_uniq)
-
-end

--- a/src/HOL/Auth/Guard/OtwayRees.thy	Wed Sep 14 23:06:02 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,195 +0,0 @@
-(******************************************************************************
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
-
-header{*Otway-Rees Protocol*}
-
-theory OtwayRees imports Guard_Shared begin
-
-subsection{*messages used in the protocol*}
-
-syntax nil :: "msg"
-
-translations "nil" == "Number 0"
-
-syntax or1 :: "agent => agent => nat => event"
-
-translations "or1 A B NA"
-=> "Says A B {|Nonce NA, Agent A, Agent B,
-               Ciph A {|Nonce NA, Agent A, Agent B|}|}"
-
-syntax or1' :: "agent => agent => agent => nat => msg => event"
-
-translations "or1' A' A B NA X"
-=> "Says A' B {|Nonce NA, Agent A, Agent B, X|}"
-
-syntax or2 :: "agent => agent => nat => nat => msg => event"
-
-translations "or2 A B NA NB X"
-=> "Says B Server {|Nonce NA, Agent A, Agent B, X,
-                    Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
-
-syntax or2' :: "agent => agent => agent => nat => nat => event"
-
-translations "or2' B' A B NA NB"
-=> "Says B' Server {|Nonce NA, Agent A, Agent B,
-                     Ciph A {|Nonce NA, Agent A, Agent B|},
-                     Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
-
-syntax or3 :: "agent => agent => nat => nat => key => event"
-
-translations "or3 A B NA NB K"
-=> "Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|},
-                    Ciph B {|Nonce NB, Key K|}|}"
-
-syntax or3':: "agent => msg => agent => agent => nat => nat => key => event"
-
-translations "or3' S Y A B NA NB K"
-=> "Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}"
-
-syntax or4 :: "agent => agent => nat => msg => event"
-
-translations "or4 A B NA X" => "Says B A {|Nonce NA, X, nil|}"
-
-syntax or4' :: "agent => agent => nat => msg => event"
-
-translations "or4' B' A NA K" =>
-"Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}"
-
-subsection{*definition of the protocol*}
-
-consts or :: "event list set"
-
-inductive or
-intros
-
-Nil: "[]:or"
-
-Fake: "[| evs:or; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:or"
-
-OR1: "[| evs1:or; Nonce NA ~:used evs1 |] ==> or1 A B NA # evs1:or"
-
-OR2: "[| evs2:or; or1' A' A B NA X:set evs2; Nonce NB ~:used evs2 |]
-==> or2 A B NA NB X # evs2:or"
-
-OR3: "[| evs3:or; or2' B' A B NA NB:set evs3; Key K ~:used evs3 |]
-==> or3 A B NA NB K # evs3:or"
-
-OR4: "[| evs4:or; or2 A B NA NB X:set evs4; or3' S Y A B NA NB K:set evs4 |]
-==> or4 A B NA X # evs4:or"
-
-subsection{*declarations for tactics*}
-
-declare knows_Spy_partsEs [elim]
-declare Fake_parts_insert [THEN subsetD, dest]
-declare initState.simps [simp del]
-
-subsection{*general properties of or*}
-
-lemma or_has_no_Gets: "evs:or ==> ALL A X. Gets A X ~:set evs"
-by (erule or.induct, auto)
-
-lemma or_is_Gets_correct [iff]: "Gets_correct or"
-by (auto simp: Gets_correct_def dest: or_has_no_Gets)
-
-lemma or_is_one_step [iff]: "one_step or"
-by (unfold one_step_def, clarify, ind_cases "ev#evs:or", auto)
-
-lemma or_has_only_Says' [rule_format]: "evs:or ==>
-ev:set evs --> (EX A B X. ev=Says A B X)"
-by (erule or.induct, auto)
-
-lemma or_has_only_Says [iff]: "has_only_Says or"
-by (auto simp: has_only_Says_def dest: or_has_only_Says')
-
-subsection{*or is regular*}
-
-lemma or1'_parts_spies [dest]: "or1' A' A B NA X:set evs
-==> X:parts (spies evs)"
-by blast
-
-lemma or2_parts_spies [dest]: "or2 A B NA NB X:set evs
-==> X:parts (spies evs)"
-by blast
-
-lemma or3_parts_spies [dest]: "Says S B {|NA, Y, Ciph B {|NB, K|}|}:set evs
-==> K:parts (spies evs)"
-by blast
-
-lemma or_is_regular [iff]: "regular or"
-apply (simp only: regular_def, clarify)
-apply (erule or.induct, simp_all add: initState.simps knows.simps)
-by (auto dest: parts_sub)
-
-subsection{*guardedness of KAB*}
-
-lemma Guard_KAB [rule_format]: "[| evs:or; A ~:bad; B ~:bad |] ==>
-or3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" 
-apply (erule or.induct)
-(* Nil *)
-apply simp_all
-(* Fake *)
-apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp)
-(* OR1 *)
-apply blast
-(* OR2 *)
-apply safe
-apply (blast dest: Says_imp_spies, blast)
-(* OR3 *)
-apply blast
-apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
-apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
-(* OR4 *)
-by (blast dest: Says_imp_spies in_GuardK_kparts)
-
-subsection{*guardedness of NB*}
-
-lemma Guard_NB [rule_format]: "[| evs:or; B ~:bad |] ==>
-or2 A B NA NB X:set evs --> Guard NB {shrK B} (spies evs)" 
-apply (erule or.induct)
-(* Nil *)
-apply simp_all
-(* Fake *)
-apply safe
-apply (erule in_synth_Guard, erule Guard_analz, simp)
-(* OR1 *)
-apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
-apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
-(* OR2 *)
-apply blast
-apply (drule_tac n=NA in Nonce_neq, simp+, rule No_Nonce, simp)
-apply (blast intro!: No_Nonce dest: used_parts)
-apply (drule_tac n=NA in Nonce_neq, simp+, rule No_Nonce, simp)
-apply (blast intro!: No_Nonce dest: used_parts)
-apply (blast dest: Says_imp_spies)
-apply (blast dest: Says_imp_spies)
-apply (case_tac "Ba=B", clarsimp)
-apply (drule_tac n=NB and A=B in Nonce_neq, simp+)
-apply (drule Says_imp_spies)
-apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+, rule No_Nonce, simp)
-(* OR3 *)
-apply (drule Says_imp_spies)
-apply (frule_tac n'=NAa in in_Guard_kparts_neq, simp+, rule No_Nonce, simp)
-apply (case_tac "Aa=B", clarsimp)
-apply (case_tac "NAa=NB", clarsimp)
-apply (drule Says_imp_spies)
-apply (drule_tac Y="{|Nonce NB, Agent Aa, Agent Ba|}"
-                 and K="shrK Aa" in in_Guard_kparts_Crypt, simp+)
-apply (simp add: No_Nonce) 
-apply (case_tac "Ba=B", clarsimp)
-apply (case_tac "NBa=NB", clarify)
-apply (drule Says_imp_spies)
-apply (drule_tac Y="{|Nonce NAa, Nonce NB, Agent Aa, Agent Ba|}"
-                 and K="shrK Ba" in in_Guard_kparts_Crypt, simp+)
-apply (simp add: No_Nonce) 
-(* OR4 *)
-by (blast dest: Says_imp_spies)+
-
-end

--- a/src/HOL/Auth/Guard/Yahalom.thy	Wed Sep 14 23:06:02 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,259 +0,0 @@
-(******************************************************************************
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
-
-header{*Yahalom Protocol*}
-
-theory Yahalom imports Guard_Shared begin
-
-subsection{*messages used in the protocol*}
-
-syntax ya1 :: "agent => agent => nat => event"
-
-translations "ya1 A B NA" => "Says A B {|Agent A, Nonce NA|}"
-
-syntax ya1' :: "agent => agent => agent => nat => event"
-
-translations "ya1' A' A B NA" => "Says A' B {|Agent A, Nonce NA|}"
-
-syntax ya2 :: "agent => agent => nat => nat => event"
-
-translations "ya2 A B NA NB"
-=> "Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
-
-syntax ya2' :: "agent => agent => agent => nat => nat => event"
-
-translations "ya2' B' A B NA NB"
-=> "Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
-
-syntax ya3 :: "agent => agent => nat => nat => key => event"
-
-translations "ya3 A B NA NB K"
-=> "Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
-                    Ciph B {|Agent A, Key K|}|}"
-
-syntax ya3':: "agent => msg => agent => agent => nat => nat => key => event"
-
-translations "ya3' S Y A B NA NB K"
-=> "Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
-
-syntax ya4 :: "agent => agent => nat => nat => msg => event"
-
-translations "ya4 A B K NB Y" => "Says A B {|Y, Crypt K (Nonce NB)|}"
-
-syntax ya4' :: "agent => agent => nat => nat => msg => event"
-
-translations "ya4' A' B K NB Y" => "Says A' B {|Y, Crypt K (Nonce NB)|}"
-
-subsection{*definition of the protocol*}
-
-consts ya :: "event list set"
-
-inductive ya
-intros
-
-Nil: "[]:ya"
-
-Fake: "[| evs:ya; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:ya"
-
-YA1: "[| evs1:ya; Nonce NA ~:used evs1 |] ==> ya1 A B NA # evs1:ya"
-
-YA2: "[| evs2:ya; ya1' A' A B NA:set evs2; Nonce NB ~:used evs2 |]
-==> ya2 A B NA NB # evs2:ya"
-
-YA3: "[| evs3:ya; ya2' B' A B NA NB:set evs3; Key K ~:used evs3 |]
-==> ya3 A B NA NB K # evs3:ya"
-
-YA4: "[| evs4:ya; ya1 A B NA:set evs4; ya3' S Y A B NA NB K:set evs4 |]
-==> ya4 A B K NB Y # evs4:ya"
-
-subsection{*declarations for tactics*}
-
-declare knows_Spy_partsEs [elim]
-declare Fake_parts_insert [THEN subsetD, dest]
-declare initState.simps [simp del]
-
-subsection{*general properties of ya*}
-
-lemma ya_has_no_Gets: "evs:ya ==> ALL A X. Gets A X ~:set evs"
-by (erule ya.induct, auto)
-
-lemma ya_is_Gets_correct [iff]: "Gets_correct ya"
-by (auto simp: Gets_correct_def dest: ya_has_no_Gets)
-
-lemma ya_is_one_step [iff]: "one_step ya"
-by (unfold one_step_def, clarify, ind_cases "ev#evs:ya", auto)
-
-lemma ya_has_only_Says' [rule_format]: "evs:ya ==>
-ev:set evs --> (EX A B X. ev=Says A B X)"
-by (erule ya.induct, auto)
-
-lemma ya_has_only_Says [iff]: "has_only_Says ya"
-by (auto simp: has_only_Says_def dest: ya_has_only_Says')
-
-lemma ya_is_regular [iff]: "regular ya"
-apply (simp only: regular_def, clarify)
-apply (erule ya.induct, simp_all add: initState.simps knows.simps)
-by (auto dest: parts_sub)
-
-subsection{*guardedness of KAB*}
-
-lemma Guard_KAB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
-ya3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)" 
-apply (erule ya.induct)
-(* Nil *)
-apply simp_all
-(* Fake *)
-apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp)
-(* YA1 *)
-(* YA2 *)
-apply safe
-apply (blast dest: Says_imp_spies)
-(* YA3 *)
-apply blast
-apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
-apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
-(* YA4 *)
-apply (blast dest: Says_imp_spies in_GuardK_kparts)
-by blast
-
-subsection{*session keys are not symmetric keys*}
-
-lemma KAB_isnt_shrK [rule_format]: "evs:ya ==>
-ya3 A B NA NB K:set evs --> K ~:range shrK"
-by (erule ya.induct, auto)
-
-lemma ya3_shrK: "evs:ya ==> ya3 A B NA NB (shrK C) ~:set evs"
-by (blast dest: KAB_isnt_shrK)
-
-subsection{*ya2' implies ya1'*}
-
-lemma ya2'_parts_imp_ya1'_parts [rule_format]:
-     "[| evs:ya; B ~:bad |] ==>
-      Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
-      {|Agent A, Nonce NA|}:spies evs"
-by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts)
-
-lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB:set evs; evs:ya; B ~:bad |]
-==> {|Agent A, Nonce NA|}:spies evs"
-by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts)
-
-subsection{*uniqueness of NB*}
-
-lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs:ya; B ~:bad; B' ~:bad |] ==>
-Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
-Ciph B' {|Agent A', Nonce NA', Nonce NB|}:parts (spies evs) -->
-A=A' & B=B' & NA=NA'"
-apply (erule ya.induct, simp_all, clarify)
-apply (drule Crypt_synth_insert, simp+)
-apply (drule Crypt_synth_insert, simp+, safe)
-apply (drule not_used_parts_false, simp+)+
-by (drule Says_not_parts, simp+)+
-
-lemma NB_is_uniq_in_ya2': "[| ya2' C A B NA NB:set evs;
-ya2' C' A' B' NA' NB:set evs; evs:ya; B ~:bad; B' ~:bad |]
-==> A=A' & B=B' & NA=NA'"
-by (drule NB_is_uniq_in_ya2'_parts, auto dest: Says_imp_spies)
-
-subsection{*ya3' implies ya2'*}
-
-lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs:ya; A ~:bad |] ==>
-Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
---> Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs)"
-apply (erule ya.induct, simp_all)
-apply (clarify, drule Crypt_synth_insert, simp+)
-apply (blast intro: parts_sub, blast)
-by (auto dest: Says_imp_spies parts_parts)
-
-lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs:ya; A ~:bad |] ==>
-Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
---> (EX B'. ya2' B' A B NA NB:set evs)"
-apply (erule ya.induct, simp_all, safe)
-apply (drule Crypt_synth_insert, simp+)
-apply (drule Crypt_synth_insert, simp+, blast)
-apply blast
-apply blast
-by (auto dest: Says_imp_spies2 parts_parts)
-
-lemma ya3'_imp_ya2': "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
-==> (EX B'. ya2' B' A B NA NB:set evs)"
-by (drule ya3'_parts_imp_ya2', auto dest: Says_imp_spies)
-
-subsection{*ya3' implies ya3*}
-
-lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs:ya; A ~:bad |] ==>
-Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts(spies evs)
---> ya3 A B NA NB K:set evs"
-apply (erule ya.induct, simp_all, safe)
-apply (drule Crypt_synth_insert, simp+)
-by (blast dest: Says_imp_spies2 parts_parts)
-
-lemma ya3'_imp_ya3: "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
-==> ya3 A B NA NB K:set evs"
-by (blast dest: Says_imp_spies ya3'_parts_imp_ya3)
-
-subsection{*guardedness of NB*}
-
-constdefs ya_keys :: "agent => agent => nat => nat => event list => key set"
-"ya_keys A B NA NB evs == {shrK A,shrK B} Un {K. ya3 A B NA NB K:set evs}"
-
-lemma Guard_NB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
-ya2 A B NA NB:set evs --> Guard NB (ya_keys A B NA NB evs) (spies evs)"
-apply (erule ya.induct)
-(* Nil *)
-apply (simp_all add: ya_keys_def)
-(* Fake *)
-apply safe
-apply (erule in_synth_Guard, erule Guard_analz, simp, clarify)
-apply (frule_tac B=B in Guard_KAB, simp+)
-apply (drule_tac p=ya in GuardK_Key_analz, simp+)
-apply (blast dest: KAB_isnt_shrK, simp)
-(* YA1 *)
-apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
-(* YA2 *)
-apply blast
-apply (drule Says_imp_spies)
-apply (drule_tac n=NB in Nonce_neq, simp+)
-apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+)
-apply (rule No_Nonce, simp)
-(* YA3 *)
-apply (rule Guard_extand, simp, blast)
-apply (case_tac "NAa=NB", clarify)
-apply (frule Says_imp_spies)
-apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
-apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
-apply (drule ya2'_imp_ya1'_parts, simp, blast, blast)
-apply (case_tac "NBa=NB", clarify)
-apply (frule Says_imp_spies)
-apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
-apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
-apply (drule NB_is_uniq_in_ya2', simp+, blast, simp+)
-apply (simp add: No_Nonce, blast)
-(* YA4 *)
-apply (blast dest: Says_imp_spies)
-apply (case_tac "NBa=NB", clarify)
-apply (frule_tac A=S in Says_imp_spies)
-apply (frule in_Guard_kparts_Crypt, simp+)
-apply (blast dest: Says_imp_spies)
-apply (case_tac "NBa=NB", clarify)
-apply (frule_tac A=S in Says_imp_spies)
-apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
-apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Aa in ya3_shrK, simp)
-apply (frule ya3'_imp_ya2', simp+, blast, clarify)
-apply (frule_tac A=B' in Says_imp_spies)
-apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+, blast, simp+)
-apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
-apply (drule NB_is_uniq_in_ya2', simp+, blast, clarify)
-apply (drule ya3'_imp_ya3, simp+)
-apply (simp add: Guard_Nonce)
-apply (simp add: No_Nonce)
-done
-
-end

--- a/src/HOL/Auth/ROOT.ML	Wed Sep 14 23:06:02 2005 +0200
+++ b/src/HOL/Auth/ROOT.ML	Wed Sep 14 23:14:57 2005 +0200
@@ -8,6 +8,8 @@
 
 no_document use_thy "NatPair";
 
+add_path "Guard";
+
 set timing;
 
 (*Shared-key protocols*)
@@ -31,9 +33,9 @@
 time_use_thy "CertifiedEmail";
 
 (*Blanqui's "guard" concept: protocol-independent secrecy*)
-time_use_thy "Guard/P1";
-time_use_thy "Guard/P2";
-time_use_thy "Guard/NS_Public";
-time_use_thy "Guard/OtwayRees";
-time_use_thy "Guard/Yahalom";
-time_use_thy "Guard/Proto";
+time_use_thy "P1";
+time_use_thy "P2";
+time_use_thy "Guard_NS_Public";
+time_use_thy "Guard_OtwayRees";
+time_use_thy "Guard_Yahalom";
+time_use_thy "Proto";

--- a/src/HOL/IsaMakefile	Wed Sep 14 23:06:02 2005 +0200
+++ b/src/HOL/IsaMakefile	Wed Sep 14 23:14:57 2005 +0200
@@ -390,9 +390,9 @@
   Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \
   Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \
   Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \
-  Auth/Guard/NS_Public.thy Auth/Guard/OtwayRees.thy \
+  Auth/Guard/Guard_NS_Public.thy Auth/Guard/Guard_OtwayRees.thy \
   Auth/Guard/P1.thy Auth/Guard/P2.thy \
-  Auth/Guard/Proto.thy Auth/Guard/Yahalom.thy\
+  Auth/Guard/Proto.thy Auth/Guard/Guard_Yahalom.thy\
   Auth/document/root.tex 
 	@$(ISATOOL) usedir -g true $(OUT)/HOL Auth

author	wenzelm
	Wed, 14 Sep 2005 23:14:57 +0200
changeset 17394	a8c9ed3f9818
parent 17393	23b7e14ce640
child 17395	a05e20f6a31a

src/HOL/Auth/Guard/Guard_NS_Public.thy		file \| annotate \| diff \| comparison \| revisions
src/HOL/Auth/Guard/Guard_OtwayRees.thy		file \| annotate \| diff \| comparison \| revisions
src/HOL/Auth/Guard/Guard_Yahalom.thy		file \| annotate \| diff \| comparison \| revisions
src/HOL/Auth/Guard/NS_Public.thy		file \| annotate \| diff \| comparison \| revisions
src/HOL/Auth/Guard/OtwayRees.thy		file \| annotate \| diff \| comparison \| revisions
src/HOL/Auth/Guard/Yahalom.thy		file \| annotate \| diff \| comparison \| revisions
src/HOL/Auth/ROOT.ML		file \| annotate \| diff \| comparison \| revisions
src/HOL/IsaMakefile		file \| annotate \| diff \| comparison \| revisions