author | berghofe |
Wed, 11 Jul 2007 11:14:51 +0200 | |
changeset 23746 | a455e69c31cc |
parent 21404 | eb85850d3eb7 |
child 41775 | 6214816d79d3 |
permissions | -rw-r--r-- |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
1 |
(****************************************************************************** |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
2 |
incorporating Lowe's fix (inclusion of B's identity in round 2) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
3 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
4 |
date: march 2002 |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
5 |
author: Frederic Blanqui |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
6 |
email: blanqui@lri.fr |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
7 |
webpage: http://www.lri.fr/~blanqui/ |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
8 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
9 |
University of Cambridge, Computer Laboratory |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
10 |
William Gates Building, JJ Thomson Avenue |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
11 |
Cambridge CB3 0FD, United Kingdom |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
12 |
******************************************************************************) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
13 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
14 |
header{*Needham-Schroeder-Lowe Public-Key Protocol*} |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
15 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
16 |
theory Guard_NS_Public imports Guard_Public begin |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
17 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
18 |
subsection{*messages used in the protocol*} |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
19 |
|
20768 | 20 |
abbreviation (input) |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
21 |
ns1 :: "agent => agent => nat => event" where |
20768 | 22 |
"ns1 A B NA == Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})" |
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 |
ns1' :: "agent => agent => agent => nat => event" where |
20768 | 26 |
"ns1' A' A B NA == Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})" |
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 |
ns2 :: "agent => agent => nat => nat => event" where |
20768 | 30 |
"ns2 B A NA NB == Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
31 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
32 |
abbreviation (input) |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
33 |
ns2' :: "agent => agent => agent => nat => nat => event" where |
20768 | 34 |
"ns2' B' B A NA NB == Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
35 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
36 |
abbreviation (input) |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
37 |
ns3 :: "agent => agent => nat => event" where |
20768 | 38 |
"ns3 A B NB == Says A B (Crypt (pubK B) (Nonce NB))" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
39 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
40 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
41 |
subsection{*definition of the protocol*} |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
42 |
|
23746 | 43 |
inductive_set nsp :: "event list set" |
44 |
where |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
45 |
|
23746 | 46 |
Nil: "[]:nsp" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
47 |
|
23746 | 48 |
| Fake: "[| evs:nsp; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs : nsp" |
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 |
| NS1: "[| evs1:nsp; Nonce NA ~:used evs1 |] ==> ns1 A B NA # evs1 : nsp" |
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
51 |
|
23746 | 52 |
| NS2: "[| evs2:nsp; Nonce NB ~:used evs2; ns1' A' A B NA:set evs2 |] ==> |
53 |
ns2 B A NA NB # evs2:nsp" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
54 |
|
23746 | 55 |
| NS3: "!!A B B' NA NB evs3. [| evs3:nsp; ns1 A B NA:set evs3; ns2' B' B A NA NB:set evs3 |] ==> |
56 |
ns3 A B NB # evs3:nsp" |
|
17394
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
57 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
58 |
subsection{*declarations for tactics*} |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
59 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
60 |
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
|
61 |
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
|
62 |
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
|
63 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
64 |
subsection{*general properties of nsp*} |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
65 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
66 |
lemma nsp_has_no_Gets: "evs:nsp ==> ALL A X. Gets A X ~:set evs" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
67 |
by (erule nsp.induct, auto) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
68 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
69 |
lemma nsp_is_Gets_correct [iff]: "Gets_correct nsp" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
70 |
by (auto simp: Gets_correct_def dest: nsp_has_no_Gets) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
71 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
72 |
lemma nsp_is_one_step [iff]: "one_step nsp" |
23746 | 73 |
by (unfold one_step_def, clarify, ind_cases "ev#evs:nsp" 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
|
74 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
75 |
lemma nsp_has_only_Says' [rule_format]: "evs:nsp ==> |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
76 |
ev:set evs --> (EX A B X. ev=Says A B X)" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
77 |
by (erule nsp.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 nsp_has_only_Says [iff]: "has_only_Says nsp" |
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: has_only_Says_def dest: nsp_has_only_Says') |
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 nsp_is_regular [iff]: "regular nsp" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
83 |
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
|
84 |
by (erule nsp.induct, auto simp: 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
|
85 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
86 |
subsection{*nonce are used only once*} |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
87 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
88 |
lemma NA_is_uniq [rule_format]: "evs:nsp ==> |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
89 |
Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
90 |
--> Crypt (pubK B') {|Nonce NA, Agent A'|}:parts (spies evs) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
91 |
--> Nonce NA ~:analz (spies evs) --> A=A' & B=B'" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
92 |
apply (erule nsp.induct, simp_all) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
93 |
by (blast intro: analz_insertI)+ |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
94 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
95 |
lemma no_Nonce_NS1_NS2 [rule_format]: "evs:nsp ==> |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
96 |
Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
97 |
--> Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
98 |
--> Nonce NA:analz (spies evs)" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
99 |
apply (erule nsp.induct, simp_all) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
100 |
by (blast intro: analz_insertI)+ |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
101 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
102 |
lemma no_Nonce_NS1_NS2' [rule_format]: |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
103 |
"[| Crypt (pubK B') {|Nonce NA', Nonce NA, Agent A'|}:parts (spies evs); |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
104 |
Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs); evs:nsp |] |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
105 |
==> Nonce NA:analz (spies evs)" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
106 |
by (rule no_Nonce_NS1_NS2, auto) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
107 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
108 |
lemma NB_is_uniq [rule_format]: "evs:nsp ==> |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
109 |
Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
110 |
--> Crypt (pubK A') {|Nonce NA', Nonce NB, Agent B'|}:parts (spies evs) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
111 |
--> Nonce NB ~:analz (spies evs) --> A=A' & B=B' & NA=NA'" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
112 |
apply (erule nsp.induct, simp_all) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
113 |
by (blast intro: analz_insertI)+ |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
114 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
115 |
subsection{*guardedness of NA*} |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
116 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
117 |
lemma ns1_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==> |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
118 |
ns1 A B NA:set evs --> Guard NA {priK A,priK B} (spies evs)" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
119 |
apply (erule nsp.induct) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
120 |
(* Nil *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
121 |
apply simp_all |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
122 |
(* Fake *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
123 |
apply safe |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
124 |
apply (erule in_synth_Guard, erule Guard_analz, simp) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
125 |
(* NS1 *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
126 |
apply blast |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
127 |
apply blast |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
128 |
apply blast |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
129 |
apply (drule 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
|
130 |
(* NS2 *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
131 |
apply (frule_tac A=A 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
|
132 |
apply (case_tac "NAa=NA") |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
133 |
apply (drule Guard_Nonce_analz, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
134 |
apply (drule Says_imp_knows_Spy)+ |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
135 |
apply (drule_tac B=B and A'=Aa in NA_is_uniq, auto) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
136 |
(* NS3 *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
137 |
apply (case_tac "NB=NA", clarify) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
138 |
apply (drule Guard_Nonce_analz, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
139 |
apply (drule Says_imp_knows_Spy)+ |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
140 |
by (drule no_Nonce_NS1_NS2, auto) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
141 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
142 |
subsection{*guardedness of NB*} |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
143 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
144 |
lemma ns2_imp_Guard [rule_format]: "[| evs:nsp; A ~:bad; B ~:bad |] ==> |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
145 |
ns2 B A NA NB:set evs --> Guard NB {priK A,priK B} (spies evs)" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
146 |
apply (erule nsp.induct) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
147 |
(* Nil *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
148 |
apply simp_all |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
149 |
(* Fake *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
150 |
apply safe |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
151 |
apply (erule in_synth_Guard, erule Guard_analz, simp) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
152 |
(* NS1 *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
153 |
apply (frule Nonce_neq, simp+, blast, 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
|
154 |
(* NS2 *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
155 |
apply blast |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
156 |
apply blast |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
157 |
apply blast |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
158 |
apply (frule_tac A=B and 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
|
159 |
apply (case_tac "NAa=NB") |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
160 |
apply (drule Guard_Nonce_analz, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
161 |
apply (drule Says_imp_knows_Spy)+ |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
162 |
apply (drule no_Nonce_NS1_NS2, auto) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
163 |
(* NS3 *) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
164 |
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
|
165 |
apply (drule Guard_Nonce_analz, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
166 |
apply (drule Says_imp_knows_Spy)+ |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
167 |
by (drule_tac A=Aa and A'=A in NB_is_uniq, auto) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
168 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
169 |
subsection{*Agents' Authentication*} |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
170 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
171 |
lemma B_trusts_NS1: "[| evs:nsp; A ~:bad; B ~:bad |] ==> |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
172 |
Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
173 |
--> Nonce NA ~:analz (spies evs) --> ns1 A B NA:set evs" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
174 |
apply (erule nsp.induct, simp_all) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
175 |
by (blast intro: analz_insertI)+ |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
176 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
177 |
lemma A_trusts_NS2: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns1 A B NA:set evs |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
178 |
--> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}:parts (spies evs) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
179 |
--> ns2 B A NA NB:set evs" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
180 |
apply (erule nsp.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
|
181 |
apply (frule_tac B=B in ns1_imp_Guard, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
182 |
apply (drule Guard_Nonce_analz, simp+, blast) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
183 |
apply (frule_tac B=B in ns1_imp_Guard, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
184 |
apply (drule Guard_Nonce_analz, simp+, blast) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
185 |
apply (frule_tac B=B in ns1_imp_Guard, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
186 |
by (drule Guard_Nonce_analz, simp+, blast+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
187 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
188 |
lemma B_trusts_NS3: "[| evs:nsp; A ~:bad; B ~:bad |] ==> ns2 B A NA NB:set evs |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
189 |
--> Crypt (pubK B) (Nonce NB):parts (spies evs) --> ns3 A B NB:set evs" |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
190 |
apply (erule nsp.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
|
191 |
apply (frule_tac B=B in ns2_imp_Guard, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
192 |
apply (drule Guard_Nonce_analz, simp+, blast) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
193 |
apply (frule_tac B=B in ns2_imp_Guard, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
194 |
apply (drule Guard_Nonce_analz, simp+, blast) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
195 |
apply (frule_tac B=B in ns2_imp_Guard, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
196 |
apply (drule Guard_Nonce_analz, simp+, blast, blast) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
197 |
apply (frule_tac B=B in ns2_imp_Guard, simp+) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
198 |
by (drule Guard_Nonce_analz, auto dest: Says_imp_knows_Spy NB_is_uniq) |
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
199 |
|
a8c9ed3f9818
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
wenzelm
parents:
diff
changeset
|
200 |
end |