author | wenzelm |
Mon, 13 Apr 2020 22:08:14 +0200 | |
changeset 71751 | abf3e80bd815 |
parent 67613 | ce654b0e6d69 |
child 76287 | cdc14f94c754 |
permissions | -rw-r--r-- |
41775 | 1 |
(* Title: HOL/Auth/Guard/Guard_Yahalom.thy |
2 |
Author: Frederic Blanqui, University of Cambridge Computer Laboratory |
|
3 |
Copyright 2002 University of Cambridge |
|
4 |
*) |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
5 |
|
61830 | 6 |
section\<open>Yahalom Protocol\<close> |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
7 |
|
39216 | 8 |
theory Guard_Yahalom imports "../Shared" Guard_Shared begin |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
9 |
|
61830 | 10 |
subsection\<open>messages used in the protocol\<close> |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
11 |
|
20768 | 12 |
abbreviation (input) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
13 |
ya1 :: "agent => agent => nat => event" where |
61956 | 14 |
"ya1 A B NA == Says A B \<lbrace>Agent A, Nonce NA\<rbrace>" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
15 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
16 |
abbreviation (input) |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
17 |
ya1' :: "agent => agent => agent => nat => event" where |
61956 | 18 |
"ya1' A' A B NA == Says A' B \<lbrace>Agent A, Nonce NA\<rbrace>" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
19 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
20 |
abbreviation (input) |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
21 |
ya2 :: "agent => agent => nat => nat => event" where |
61956 | 22 |
"ya2 A B NA NB == Says B Server \<lbrace>Agent B, Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
23 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
24 |
abbreviation (input) |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
25 |
ya2' :: "agent => agent => agent => nat => nat => event" where |
61956 | 26 |
"ya2' B' A B NA NB == Says B' Server \<lbrace>Agent B, Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace>\<rbrace>" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
27 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
28 |
abbreviation (input) |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
29 |
ya3 :: "agent => agent => nat => nat => key => event" where |
20768 | 30 |
"ya3 A B NA NB K == |
61956 | 31 |
Says Server A \<lbrace>Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, |
32 |
Ciph B \<lbrace>Agent A, Key K\<rbrace>\<rbrace>" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
33 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
34 |
abbreviation (input) |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
35 |
ya3':: "agent => msg => agent => agent => nat => nat => key => event" where |
20768 | 36 |
"ya3' S Y A B NA NB K == |
61956 | 37 |
Says S A \<lbrace>Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace>, Y\<rbrace>" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
38 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
39 |
abbreviation (input) |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
40 |
ya4 :: "agent => agent => nat => nat => msg => event" where |
61956 | 41 |
"ya4 A B K NB Y == Says A B \<lbrace>Y, Crypt K (Nonce NB)\<rbrace>" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
42 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
43 |
abbreviation (input) |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
44 |
ya4' :: "agent => agent => nat => nat => msg => event" where |
61956 | 45 |
"ya4' A' B K NB Y == Says A' B \<lbrace>Y, Crypt K (Nonce NB)\<rbrace>" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
46 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
47 |
|
61830 | 48 |
subsection\<open>definition of the protocol\<close> |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
49 |
|
23746 | 50 |
inductive_set ya :: "event list set" |
51 |
where |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
52 |
|
67613 | 53 |
Nil: "[] \<in> ya" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
54 |
|
67613 | 55 |
| Fake: "[| evs \<in> ya; X \<in> synth (analz (spies evs)) |] ==> Says Spy B X # evs \<in> ya" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
56 |
|
67613 | 57 |
| YA1: "[| evs1 \<in> ya; Nonce NA \<notin> used evs1 |] ==> ya1 A B NA # evs1 \<in> ya" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
58 |
|
67613 | 59 |
| YA2: "[| evs2 \<in> ya; ya1' A' A B NA \<in> set evs2; Nonce NB \<notin> used evs2 |] |
60 |
==> ya2 A B NA NB # evs2 \<in> ya" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
61 |
|
67613 | 62 |
| YA3: "[| evs3 \<in> ya; ya2' B' A B NA NB \<in> set evs3; Key K \<notin> used evs3 |] |
63 |
==> ya3 A B NA NB K # evs3 \<in> ya" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
64 |
|
67613 | 65 |
| YA4: "[| evs4 \<in> ya; ya1 A B NA \<in> set evs4; ya3' S Y A B NA NB K \<in> set evs4 |] |
66 |
==> ya4 A B K NB Y # evs4 \<in> ya" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
67 |
|
61830 | 68 |
subsection\<open>declarations for tactics\<close> |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
69 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
70 |
declare knows_Spy_partsEs [elim] |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
71 |
declare Fake_parts_insert [THEN subsetD, dest] |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
72 |
declare initState.simps [simp del] |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
73 |
|
61830 | 74 |
subsection\<open>general properties of ya\<close> |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
75 |
|
67613 | 76 |
lemma ya_has_no_Gets: "evs \<in> ya \<Longrightarrow> \<forall>A X. Gets A X \<notin> set evs" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
77 |
by (erule ya.induct, auto) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
78 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
79 |
lemma ya_is_Gets_correct [iff]: "Gets_correct ya" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
80 |
by (auto simp: Gets_correct_def dest: ya_has_no_Gets) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
81 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
82 |
lemma ya_is_one_step [iff]: "one_step ya" |
67613 | 83 |
by (unfold one_step_def, clarify, ind_cases "ev#evs \<in> ya" for ev evs, auto) |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
84 |
|
67613 | 85 |
lemma ya_has_only_Says' [rule_format]: "evs \<in> ya \<Longrightarrow> |
86 |
ev \<in> set evs \<longrightarrow> (\<exists>A B X. ev=Says A B X)" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
87 |
by (erule ya.induct, auto) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
88 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
89 |
lemma ya_has_only_Says [iff]: "has_only_Says ya" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
90 |
by (auto simp: has_only_Says_def dest: ya_has_only_Says') |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
91 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
92 |
lemma ya_is_regular [iff]: "regular ya" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
93 |
apply (simp only: regular_def, clarify) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
94 |
apply (erule ya.induct, simp_all add: initState.simps knows.simps) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
95 |
by (auto dest: parts_sub) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
96 |
|
61830 | 97 |
subsection\<open>guardedness of KAB\<close> |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
98 |
|
67613 | 99 |
lemma Guard_KAB [rule_format]: "[| evs \<in> ya; A \<notin> bad; B \<notin> bad |] ==> |
100 |
ya3 A B NA NB K \<in> set evs \<longrightarrow> GuardK K {shrK A,shrK B} (spies evs)" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
101 |
apply (erule ya.induct) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
102 |
(* Nil *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
103 |
apply simp_all |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
104 |
(* Fake *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
105 |
apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
106 |
(* YA1 *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
107 |
(* YA2 *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
108 |
apply safe |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
109 |
apply (blast dest: Says_imp_spies) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
110 |
(* YA3 *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
111 |
apply blast |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
112 |
apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
113 |
apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
114 |
(* YA4 *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
115 |
apply (blast dest: Says_imp_spies in_GuardK_kparts) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
116 |
by blast |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
117 |
|
61830 | 118 |
subsection\<open>session keys are not symmetric keys\<close> |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
119 |
|
67613 | 120 |
lemma KAB_isnt_shrK [rule_format]: "evs \<in> ya \<Longrightarrow> |
121 |
ya3 A B NA NB K \<in> set evs \<longrightarrow> K \<notin> range shrK" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
122 |
by (erule ya.induct, auto) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
123 |
|
67613 | 124 |
lemma ya3_shrK: "evs \<in> ya \<Longrightarrow> ya3 A B NA NB (shrK C) \<notin> set evs" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
125 |
by (blast dest: KAB_isnt_shrK) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
126 |
|
61830 | 127 |
subsection\<open>ya2' implies ya1'\<close> |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
128 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
129 |
lemma ya2'_parts_imp_ya1'_parts [rule_format]: |
67613 | 130 |
"[| evs \<in> ya; B \<notin> bad |] ==> |
131 |
Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow> |
|
132 |
\<lbrace>Agent A, Nonce NA\<rbrace> \<in> spies evs" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
133 |
by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
134 |
|
67613 | 135 |
lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB \<in> set evs; evs \<in> ya; B \<notin> bad |] |
136 |
==> \<lbrace>Agent A, Nonce NA\<rbrace> \<in> spies evs" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
137 |
by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
138 |
|
61830 | 139 |
subsection\<open>uniqueness of NB\<close> |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
140 |
|
67613 | 141 |
lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs \<in> ya; B \<notin> bad; B' \<notin> bad |] ==> |
142 |
Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow> |
|
143 |
Ciph B' \<lbrace>Agent A', Nonce NA', Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow> |
|
144 |
A=A' \<and> B=B' \<and> NA=NA'" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
145 |
apply (erule ya.induct, simp_all, clarify) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
146 |
apply (drule Crypt_synth_insert, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
147 |
apply (drule Crypt_synth_insert, simp+, safe) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
148 |
apply (drule not_used_parts_false, simp+)+ |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
149 |
by (drule Says_not_parts, simp+)+ |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
150 |
|
67613 | 151 |
lemma NB_is_uniq_in_ya2': "[| ya2' C A B NA NB \<in> set evs; |
152 |
ya2' C' A' B' NA' NB \<in> set evs; evs \<in> ya; B \<notin> bad; B' \<notin> bad |] |
|
153 |
==> A=A' \<and> B=B' \<and> NA=NA'" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
154 |
by (drule NB_is_uniq_in_ya2'_parts, auto dest: Says_imp_spies) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
155 |
|
61830 | 156 |
subsection\<open>ya3' implies ya2'\<close> |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
157 |
|
67613 | 158 |
lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs \<in> ya; A \<notin> bad |] ==> |
159 |
Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) |
|
160 |
\<longrightarrow> Ciph B \<lbrace>Agent A, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs)" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
161 |
apply (erule ya.induct, simp_all) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
162 |
apply (clarify, drule Crypt_synth_insert, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
163 |
apply (blast intro: parts_sub, blast) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
164 |
by (auto dest: Says_imp_spies parts_parts) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
165 |
|
67613 | 166 |
lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs \<in> ya; A \<notin> bad |] ==> |
167 |
Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) |
|
168 |
\<longrightarrow> (\<exists>B'. ya2' B' A B NA NB \<in> set evs)" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
169 |
apply (erule ya.induct, simp_all, safe) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
170 |
apply (drule Crypt_synth_insert, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
171 |
apply (drule Crypt_synth_insert, simp+, blast) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
172 |
apply blast |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
173 |
apply blast |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
174 |
by (auto dest: Says_imp_spies2 parts_parts) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
175 |
|
67613 | 176 |
lemma ya3'_imp_ya2': "[| ya3' S Y A B NA NB K \<in> set evs; evs \<in> ya; A \<notin> bad |] |
177 |
==> (\<exists>B'. ya2' B' A B NA NB \<in> set evs)" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
178 |
by (drule ya3'_parts_imp_ya2', auto dest: Says_imp_spies) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
179 |
|
61830 | 180 |
subsection\<open>ya3' implies ya3\<close> |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
181 |
|
67613 | 182 |
lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs \<in> ya; A \<notin> bad |] ==> |
183 |
Ciph A \<lbrace>Agent B, Key K, Nonce NA, Nonce NB\<rbrace> \<in> parts(spies evs) |
|
184 |
\<longrightarrow> ya3 A B NA NB K \<in> set evs" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
185 |
apply (erule ya.induct, simp_all, safe) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
186 |
apply (drule Crypt_synth_insert, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
187 |
by (blast dest: Says_imp_spies2 parts_parts) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
188 |
|
67613 | 189 |
lemma ya3'_imp_ya3: "[| ya3' S Y A B NA NB K \<in> set evs; evs \<in> ya; A \<notin> bad |] |
190 |
==> ya3 A B NA NB K \<in> set evs" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
191 |
by (blast dest: Says_imp_spies ya3'_parts_imp_ya3) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
192 |
|
61830 | 193 |
subsection\<open>guardedness of NB\<close> |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
194 |
|
67613 | 195 |
definition ya_keys :: "agent \<Rightarrow> agent \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> event list \<Rightarrow> key set" where |
196 |
"ya_keys A B NA NB evs \<equiv> {shrK A,shrK B} \<union> {K. ya3 A B NA NB K \<in> set evs}" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
197 |
|
67613 | 198 |
lemma Guard_NB [rule_format]: "[| evs \<in> ya; A \<notin> bad; B \<notin> bad |] ==> |
199 |
ya2 A B NA NB \<in> set evs \<longrightarrow> Guard NB (ya_keys A B NA NB evs) (spies evs)" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
200 |
apply (erule ya.induct) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
201 |
(* Nil *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
202 |
apply (simp_all add: ya_keys_def) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
203 |
(* Fake *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
204 |
apply safe |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
205 |
apply (erule in_synth_Guard, erule Guard_analz, simp, clarify) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
206 |
apply (frule_tac B=B in Guard_KAB, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
207 |
apply (drule_tac p=ya in GuardK_Key_analz, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
208 |
apply (blast dest: KAB_isnt_shrK, simp) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
209 |
(* YA1 *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
210 |
apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
211 |
(* YA2 *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
212 |
apply blast |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
213 |
apply (drule Says_imp_spies) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
214 |
apply (drule_tac n=NB in Nonce_neq, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
215 |
apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
216 |
apply (rule No_Nonce, simp) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
217 |
(* YA3 *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
218 |
apply (rule Guard_extand, simp, blast) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
219 |
apply (case_tac "NAa=NB", clarify) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
220 |
apply (frule Says_imp_spies) |
56073
29e308b56d23
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
nipkow
parents:
41775
diff
changeset
|
221 |
apply (frule in_Guard_kparts_Crypt, simp+) |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
222 |
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
223 |
apply (drule ya2'_imp_ya1'_parts, simp, blast, blast) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
224 |
apply (case_tac "NBa=NB", clarify) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
225 |
apply (frule Says_imp_spies) |
56073
29e308b56d23
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
nipkow
parents:
41775
diff
changeset
|
226 |
apply (frule in_Guard_kparts_Crypt, simp+) |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
227 |
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
228 |
apply (drule NB_is_uniq_in_ya2', simp+, blast, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
229 |
apply (simp add: No_Nonce, blast) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
230 |
(* YA4 *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
231 |
apply (blast dest: Says_imp_spies) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
232 |
apply (case_tac "NBa=NB", clarify) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
233 |
apply (frule_tac A=S in Says_imp_spies) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
234 |
apply (frule in_Guard_kparts_Crypt, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
235 |
apply (blast dest: Says_imp_spies) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
236 |
apply (case_tac "NBa=NB", clarify) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
237 |
apply (frule_tac A=S in Says_imp_spies) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
238 |
apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
239 |
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Aa in ya3_shrK, simp) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
240 |
apply (frule ya3'_imp_ya2', simp+, blast, clarify) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
241 |
apply (frule_tac A=B' in Says_imp_spies) |
56073
29e308b56d23
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
nipkow
parents:
41775
diff
changeset
|
242 |
apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+) |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
243 |
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
244 |
apply (drule NB_is_uniq_in_ya2', simp+, blast, clarify) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
245 |
apply (drule ya3'_imp_ya3, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
246 |
apply (simp add: Guard_Nonce) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
247 |
apply (simp add: No_Nonce) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
248 |
done |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
249 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
250 |
end |