author | paulson <lp15@cam.ac.uk> |
Wed, 26 Apr 2017 15:53:35 +0100 | |
changeset 65583 | 8d53b3bebab4 |
parent 63975 | 6728b5007ad0 |
child 67443 | 3abf6a722518 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/Auth/OtwayRees.thy |
11251 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1996 University of Cambridge |
|
1941 | 4 |
*) |
5 |
||
61830 | 6 |
section\<open>The Original Otway-Rees Protocol\<close> |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
7 |
|
16417 | 8 |
theory OtwayRees imports Public begin |
13907 | 9 |
|
61830 | 10 |
text\<open>From page 244 of |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
11 |
Burrows, Abadi and Needham (1989). A Logic of Authentication. |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
12 |
Proc. Royal Soc. 426 |
1941 | 13 |
|
61830 | 14 |
This is the original version, which encrypts Nonce NB.\<close> |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
15 |
|
23746 | 16 |
inductive_set otway :: "event list set" |
17 |
where |
|
1941 | 18 |
(*Initial trace is empty*) |
11251 | 19 |
Nil: "[] \<in> otway" |
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5359
diff
changeset
|
20 |
|
2032 | 21 |
(*The spy MAY say anything he CAN say. We do not expect him to |
1941 | 22 |
invent new nonces here, but he can also use NS1. Common to |
23 |
all similar protocols.*) |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
24 |
| Fake: "\<lbrakk>evsf \<in> otway; X \<in> synth (analz (knows Spy evsf)) \<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
25 |
\<Longrightarrow> Says Spy B X # evsf \<in> otway" |
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
26 |
|
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
27 |
(*A message that has been sent can be received by the |
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5434
diff
changeset
|
28 |
intended recipient.*) |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
29 |
| Reception: "\<lbrakk>evsr \<in> otway; Says A B X \<in>set evsr\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
30 |
\<Longrightarrow> Gets B X # evsr \<in> otway" |
1941 | 31 |
|
32 |
(*Alice initiates a protocol run*) |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
33 |
| OR1: "\<lbrakk>evs1 \<in> otway; Nonce NA \<notin> used evs1\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
34 |
\<Longrightarrow> Says A B \<lbrace>Nonce NA, Agent A, Agent B, |
61956 | 35 |
Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace> \<rbrace> |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
36 |
# evs1 \<in> otway" |
1941 | 37 |
|
6333 | 38 |
(*Bob's response to Alice's message. Note that NB is encrypted.*) |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
39 |
| OR2: "\<lbrakk>evs2 \<in> otway; Nonce NB \<notin> used evs2; |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
40 |
Gets B \<lbrace>Nonce NA, Agent A, Agent B, X\<rbrace> : set evs2\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
41 |
\<Longrightarrow> Says B Server |
61956 | 42 |
\<lbrace>Nonce NA, Agent A, Agent B, X, |
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2378
diff
changeset
|
43 |
Crypt (shrK B) |
61956 | 44 |
\<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace> |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
45 |
# evs2 \<in> otway" |
1941 | 46 |
|
47 |
(*The Server receives Bob's message and checks that the three NAs |
|
48 |
match. Then he sends a new session key to Bob with a packet for |
|
49 |
forwarding to Alice.*) |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
50 |
| OR3: "\<lbrakk>evs3 \<in> otway; Key KAB \<notin> used evs3; |
11251 | 51 |
Gets Server |
61956 | 52 |
\<lbrace>Nonce NA, Agent A, Agent B, |
53 |
Crypt (shrK A) \<lbrace>Nonce NA, Agent A, Agent B\<rbrace>, |
|
54 |
Crypt (shrK B) \<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace> |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
55 |
: set evs3\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
56 |
\<Longrightarrow> Says Server B |
61956 | 57 |
\<lbrace>Nonce NA, |
58 |
Crypt (shrK A) \<lbrace>Nonce NA, Key KAB\<rbrace>, |
|
59 |
Crypt (shrK B) \<lbrace>Nonce NB, Key KAB\<rbrace>\<rbrace> |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
60 |
# evs3 \<in> otway" |
1941 | 61 |
|
62 |
(*Bob receives the Server's (?) message and compares the Nonces with |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23746
diff
changeset
|
63 |
those in the message he previously sent the Server. |
11251 | 64 |
Need B \<noteq> Server because we allow messages to self.*) |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
65 |
| OR4: "\<lbrakk>evs4 \<in> otway; B \<noteq> Server; |
61956 | 66 |
Says B Server \<lbrace>Nonce NA, Agent A, Agent B, X', |
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2135
diff
changeset
|
67 |
Crypt (shrK B) |
61956 | 68 |
\<lbrace>Nonce NA, Nonce NB, Agent A, Agent B\<rbrace>\<rbrace> |
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset
|
69 |
: set evs4; |
61956 | 70 |
Gets B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace> |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
71 |
: set evs4\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
72 |
\<Longrightarrow> Says B A \<lbrace>Nonce NA, X\<rbrace> # evs4 \<in> otway" |
1941 | 73 |
|
2135 | 74 |
(*This message models possible leaks of session keys. The nonces |
75 |
identify the protocol run.*) |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
76 |
| Oops: "\<lbrakk>evso \<in> otway; |
61956 | 77 |
Says Server B \<lbrace>Nonce NA, X, Crypt (shrK B) \<lbrace>Nonce NB, Key K\<rbrace>\<rbrace> |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
78 |
: set evso\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
79 |
\<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> otway" |
1941 | 80 |
|
11251 | 81 |
|
18570 | 82 |
declare Says_imp_analz_Spy [dest] |
11251 | 83 |
declare parts.Body [dest] |
84 |
declare analz_into_parts [dest] |
|
85 |
declare Fake_parts_insert_in_Un [dest] |
|
86 |
||
87 |
||
61830 | 88 |
text\<open>A "possibility property": there are traces that reach the end\<close> |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
89 |
lemma "\<lbrakk>B \<noteq> Server; Key K \<notin> used []\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
90 |
\<Longrightarrow> \<exists>evs \<in> otway. |
61956 | 91 |
Says B A \<lbrace>Nonce NA, Crypt (shrK A) \<lbrace>Nonce NA, Key K\<rbrace>\<rbrace> |
11251 | 92 |
\<in> set evs" |
93 |
apply (intro exI bexI) |
|
94 |
apply (rule_tac [2] otway.Nil |
|
95 |
[THEN otway.OR1, THEN otway.Reception, |
|
96 |
THEN otway.OR2, THEN otway.Reception, |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13907
diff
changeset
|
97 |
THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13907
diff
changeset
|
98 |
apply (possibility, simp add: used_Cons) |
11251 | 99 |
done |
100 |
||
101 |
lemma Gets_imp_Says [dest!]: |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
102 |
"\<lbrakk>Gets B X \<in> set evs; evs \<in> otway\<rbrakk> \<Longrightarrow> \<exists>A. Says A B X \<in> set evs" |
11251 | 103 |
apply (erule rev_mp) |
13507 | 104 |
apply (erule otway.induct, auto) |
11251 | 105 |
done |
106 |
||
107 |
||
108 |
(** For reasoning about the encrypted portion of messages **) |
|
109 |
||
110 |
lemma OR2_analz_knows_Spy: |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
111 |
"\<lbrakk>Gets B \<lbrace>N, Agent A, Agent B, X\<rbrace> \<in> set evs; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
112 |
\<Longrightarrow> X \<in> analz (knows Spy evs)" |
11251 | 113 |
by blast |
114 |
||
115 |
lemma OR4_analz_knows_Spy: |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
116 |
"\<lbrakk>Gets B \<lbrace>N, X, Crypt (shrK B) X'\<rbrace> \<in> set evs; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
117 |
\<Longrightarrow> X \<in> analz (knows Spy evs)" |
11251 | 118 |
by blast |
119 |
||
120 |
(*These lemmas assist simplification by removing forwarded X-variables. |
|
121 |
We can replace them by rewriting with parts_insert2 and proving using |
|
122 |
dest: parts_cut, but the proofs become more difficult.*) |
|
123 |
lemmas OR2_parts_knows_Spy = |
|
45605 | 124 |
OR2_analz_knows_Spy [THEN analz_into_parts] |
11251 | 125 |
|
126 |
(*There could be OR4_parts_knows_Spy and Oops_parts_knows_Spy, but for |
|
127 |
some reason proofs work without them!*) |
|
128 |
||
129 |
||
61830 | 130 |
text\<open>Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that |
131 |
NOBODY sends messages containing X!\<close> |
|
11251 | 132 |
|
61830 | 133 |
text\<open>Spy never sees a good agent's shared key!\<close> |
11251 | 134 |
lemma Spy_see_shrK [simp]: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
135 |
"evs \<in> otway \<Longrightarrow> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
13907 | 136 |
by (erule otway.induct, force, |
137 |
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
|
138 |
||
11251 | 139 |
|
140 |
lemma Spy_analz_shrK [simp]: |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
141 |
"evs \<in> otway \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
11251 | 142 |
by auto |
143 |
||
144 |
lemma Spy_see_shrK_D [dest!]: |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
145 |
"\<lbrakk>Key (shrK A) \<in> parts (knows Spy evs); evs \<in> otway\<rbrakk> \<Longrightarrow> A \<in> bad" |
11251 | 146 |
by (blast dest: Spy_see_shrK) |
147 |
||
148 |
||
61830 | 149 |
subsection\<open>Towards Secrecy: Proofs Involving @{term analz}\<close> |
11251 | 150 |
|
151 |
(*Describes the form of K and NA when the Server sends this message. Also |
|
152 |
for Oops case.*) |
|
153 |
lemma Says_Server_message_form: |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
154 |
"\<lbrakk>Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs; |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
155 |
evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
156 |
\<Longrightarrow> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)" |
17778 | 157 |
by (erule rev_mp, erule otway.induct, simp_all) |
11251 | 158 |
|
159 |
||
160 |
(**** |
|
161 |
The following is to prove theorems of the form |
|
162 |
||
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
163 |
Key K \<in> analz (insert (Key KAB) (knows Spy evs)) \<Longrightarrow> |
11251 | 164 |
Key K \<in> analz (knows Spy evs) |
165 |
||
166 |
A more general formula must be proved inductively. |
|
167 |
****) |
|
168 |
||
169 |
||
61830 | 170 |
text\<open>Session keys are not used to encrypt other session keys\<close> |
11251 | 171 |
|
61830 | 172 |
text\<open>The equality makes the induction hypothesis easier to apply\<close> |
11251 | 173 |
lemma analz_image_freshK [rule_format]: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
174 |
"evs \<in> otway \<Longrightarrow> |
11251 | 175 |
\<forall>K KK. KK <= -(range shrK) --> |
176 |
(Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
|
177 |
(K \<in> KK | Key K \<in> analz (knows Spy evs))" |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
178 |
apply (erule otway.induct) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
179 |
apply (frule_tac [8] Says_Server_message_form) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
180 |
apply (drule_tac [7] OR4_analz_knows_Spy) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
181 |
apply (drule_tac [5] OR2_analz_knows_Spy, analz_freshK, spy_analz, auto) |
11251 | 182 |
done |
183 |
||
184 |
lemma analz_insert_freshK: |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
185 |
"\<lbrakk>evs \<in> otway; KAB \<notin> range shrK\<rbrakk> \<Longrightarrow> |
11655 | 186 |
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = |
11251 | 187 |
(K = KAB | Key K \<in> analz (knows Spy evs))" |
188 |
by (simp only: analz_image_freshK analz_image_freshK_simps) |
|
189 |
||
190 |
||
61830 | 191 |
text\<open>The Key K uniquely identifies the Server's message.\<close> |
11251 | 192 |
lemma unique_session_keys: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
193 |
"\<lbrakk>Says Server B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, K\<rbrace>\<rbrace> \<in> set evs; |
61956 | 194 |
Says Server B' \<lbrace>NA',X',Crypt (shrK B') \<lbrace>NB',K\<rbrace>\<rbrace> \<in> set evs; |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
195 |
evs \<in> otway\<rbrakk> \<Longrightarrow> X=X' & B=B' & NA=NA' & NB=NB'" |
11251 | 196 |
apply (erule rev_mp) |
197 |
apply (erule rev_mp) |
|
198 |
apply (erule otway.induct, simp_all) |
|
61830 | 199 |
apply blast+ \<comment>\<open>OR3 and OR4\<close> |
11251 | 200 |
done |
201 |
||
202 |
||
61830 | 203 |
subsection\<open>Authenticity properties relating to NA\<close> |
11251 | 204 |
|
61830 | 205 |
text\<open>Only OR1 can have caused such a part of a message to appear.\<close> |
11251 | 206 |
lemma Crypt_imp_OR1 [rule_format]: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
207 |
"\<lbrakk>A \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
208 |
\<Longrightarrow> Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs) --> |
61956 | 209 |
Says A B \<lbrace>NA, Agent A, Agent B, |
210 |
Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> |
|
11251 | 211 |
\<in> set evs" |
14225 | 212 |
by (erule otway.induct, force, |
213 |
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
|
11251 | 214 |
|
215 |
lemma Crypt_imp_OR1_Gets: |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
216 |
"\<lbrakk>Gets B \<lbrace>NA, Agent A, Agent B, |
61956 | 217 |
Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs; |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
218 |
A \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
219 |
\<Longrightarrow> Says A B \<lbrace>NA, Agent A, Agent B, |
61956 | 220 |
Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> |
11251 | 221 |
\<in> set evs" |
222 |
by (blast dest: Crypt_imp_OR1) |
|
223 |
||
224 |
||
61830 | 225 |
text\<open>The Nonce NA uniquely identifies A's message\<close> |
11251 | 226 |
lemma unique_NA: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
227 |
"\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs); |
61956 | 228 |
Crypt (shrK A) \<lbrace>NA, Agent A, Agent C\<rbrace> \<in> parts (knows Spy evs); |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
229 |
evs \<in> otway; A \<notin> bad\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
230 |
\<Longrightarrow> B = C" |
11251 | 231 |
apply (erule rev_mp, erule rev_mp) |
232 |
apply (erule otway.induct, force, |
|
13507 | 233 |
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
11251 | 234 |
done |
235 |
||
236 |
||
61830 | 237 |
text\<open>It is impossible to re-use a nonce in both OR1 and OR2. This holds because |
11251 | 238 |
OR2 encrypts Nonce NB. It prevents the attack that can occur in the |
61830 | 239 |
over-simplified version of this protocol: see \<open>OtwayRees_Bad\<close>.\<close> |
11251 | 240 |
lemma no_nonce_OR1_OR2: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
241 |
"\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs); |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
242 |
A \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
243 |
\<Longrightarrow> Crypt (shrK A) \<lbrace>NA', NA, Agent A', Agent A\<rbrace> \<notin> parts (knows Spy evs)" |
11251 | 244 |
apply (erule rev_mp) |
245 |
apply (erule otway.induct, force, |
|
13507 | 246 |
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
11251 | 247 |
done |
248 |
||
61830 | 249 |
text\<open>Crucial property: If the encrypted message appears, and A has used NA |
250 |
to start a run, then it originated with the Server!\<close> |
|
11251 | 251 |
lemma NA_Crypt_imp_Server_msg [rule_format]: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
252 |
"\<lbrakk>A \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
253 |
\<Longrightarrow> Says A B \<lbrace>NA, Agent A, Agent B, |
61956 | 254 |
Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs --> |
255 |
Crypt (shrK A) \<lbrace>NA, Key K\<rbrace> \<in> parts (knows Spy evs) |
|
11251 | 256 |
--> (\<exists>NB. Says Server B |
61956 | 257 |
\<lbrace>NA, |
258 |
Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, |
|
259 |
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs)" |
|
11251 | 260 |
apply (erule otway.induct, force, |
13507 | 261 |
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast) |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
262 |
subgoal \<comment>\<open>OR1: by freshness\<close> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
263 |
by blast |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
264 |
subgoal \<comment>\<open>OR3\<close> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
265 |
by (blast dest!: no_nonce_OR1_OR2 intro: unique_NA) |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
266 |
subgoal \<comment>\<open>OR4\<close> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
267 |
by (blast intro!: Crypt_imp_OR1) |
11251 | 268 |
done |
269 |
||
270 |
||
61830 | 271 |
text\<open>Corollary: if A receives B's OR4 message and the nonce NA agrees |
11251 | 272 |
then the key really did come from the Server! CANNOT prove this of the |
273 |
bad form of this protocol, even though we can prove |
|
61830 | 274 |
\<open>Spy_not_see_encrypted_key\<close>\<close> |
11251 | 275 |
lemma A_trusts_OR4: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
276 |
"\<lbrakk>Says A B \<lbrace>NA, Agent A, Agent B, |
61956 | 277 |
Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs; |
278 |
Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs; |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
279 |
A \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
280 |
\<Longrightarrow> \<exists>NB. Says Server B |
61956 | 281 |
\<lbrace>NA, |
282 |
Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, |
|
283 |
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> |
|
11251 | 284 |
\<in> set evs" |
285 |
by (blast intro!: NA_Crypt_imp_Server_msg) |
|
286 |
||
287 |
||
61830 | 288 |
text\<open>Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
11251 | 289 |
Does not in itself guarantee security: an attack could violate |
61830 | 290 |
the premises, e.g. by having @{term "A=Spy"}\<close> |
11251 | 291 |
lemma secrecy_lemma: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
292 |
"\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
293 |
\<Longrightarrow> Says Server B |
61956 | 294 |
\<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, |
295 |
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs --> |
|
296 |
Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs --> |
|
11251 | 297 |
Key K \<notin> analz (knows Spy evs)" |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
298 |
apply (erule otway.induct, force, simp_all) |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
299 |
subgoal \<comment>\<open>Fake\<close> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
300 |
by spy_analz |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
301 |
subgoal \<comment>\<open>OR2\<close> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
302 |
by (drule OR2_analz_knows_Spy) (auto simp: analz_insert_eq) |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
303 |
subgoal \<comment>\<open>OR3\<close> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
304 |
by (auto simp add: analz_insert_freshK pushes) |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
305 |
subgoal \<comment>\<open>OR4\<close> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
306 |
by (drule OR4_analz_knows_Spy) (auto simp: analz_insert_eq) |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
307 |
subgoal \<comment>\<open>Oops\<close> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
308 |
by (auto simp add: Says_Server_message_form analz_insert_freshK unique_session_keys) |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
309 |
done |
11251 | 310 |
|
13907 | 311 |
theorem Spy_not_see_encrypted_key: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
312 |
"\<lbrakk>Says Server B |
61956 | 313 |
\<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, |
314 |
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs; |
|
315 |
Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
316 |
A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
317 |
\<Longrightarrow> Key K \<notin> analz (knows Spy evs)" |
11251 | 318 |
by (blast dest: Says_Server_message_form secrecy_lemma) |
319 |
||
61830 | 320 |
text\<open>This form is an immediate consequence of the previous result. It is |
13907 | 321 |
similar to the assertions established by other methods. It is equivalent |
322 |
to the previous result in that the Spy already has @{term analz} and |
|
323 |
@{term synth} at his disposal. However, the conclusion |
|
324 |
@{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases |
|
325 |
other than Fake are trivial, while Fake requires |
|
61830 | 326 |
@{term "Key K \<notin> analz (knows Spy evs)"}.\<close> |
13907 | 327 |
lemma Spy_not_know_encrypted_key: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
328 |
"\<lbrakk>Says Server B |
61956 | 329 |
\<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, |
330 |
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs; |
|
331 |
Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
332 |
A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
333 |
\<Longrightarrow> Key K \<notin> knows Spy evs" |
13907 | 334 |
by (blast dest: Spy_not_see_encrypted_key) |
335 |
||
11251 | 336 |
|
61830 | 337 |
text\<open>A's guarantee. The Oops premise quantifies over NB because A cannot know |
338 |
what it is.\<close> |
|
11251 | 339 |
lemma A_gets_good_key: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
340 |
"\<lbrakk>Says A B \<lbrace>NA, Agent A, Agent B, |
61956 | 341 |
Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs; |
342 |
Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs; |
|
343 |
\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
344 |
A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
345 |
\<Longrightarrow> Key K \<notin> analz (knows Spy evs)" |
11251 | 346 |
by (blast dest!: A_trusts_OR4 Spy_not_see_encrypted_key) |
347 |
||
348 |
||
61830 | 349 |
subsection\<open>Authenticity properties relating to NB\<close> |
11251 | 350 |
|
61830 | 351 |
text\<open>Only OR2 can have caused such a part of a message to appear. We do not |
352 |
know anything about X: it does NOT have to have the right form.\<close> |
|
11251 | 353 |
lemma Crypt_imp_OR2: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
354 |
"\<lbrakk>Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace> \<in> parts (knows Spy evs); |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
355 |
B \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
356 |
\<Longrightarrow> \<exists>X. Says B Server |
61956 | 357 |
\<lbrace>NA, Agent A, Agent B, X, |
358 |
Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace> |
|
11251 | 359 |
\<in> set evs" |
360 |
apply (erule rev_mp) |
|
361 |
apply (erule otway.induct, force, |
|
13507 | 362 |
drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
11251 | 363 |
done |
364 |
||
365 |
||
61830 | 366 |
text\<open>The Nonce NB uniquely identifies B's message\<close> |
11251 | 367 |
lemma unique_NB: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
368 |
"\<lbrakk>Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace> \<in> parts(knows Spy evs); |
61956 | 369 |
Crypt (shrK B) \<lbrace>NC, NB, Agent C, Agent B\<rbrace> \<in> parts(knows Spy evs); |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
370 |
evs \<in> otway; B \<notin> bad\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
371 |
\<Longrightarrow> NC = NA & C = A" |
11251 | 372 |
apply (erule rev_mp, erule rev_mp) |
373 |
apply (erule otway.induct, force, |
|
374 |
drule_tac [4] OR2_parts_knows_Spy, simp_all) |
|
61830 | 375 |
apply blast+ \<comment>\<open>Fake, OR2\<close> |
11251 | 376 |
done |
377 |
||
61830 | 378 |
text\<open>If the encrypted message appears, and B has used Nonce NB, |
379 |
then it originated with the Server! Quite messy proof.\<close> |
|
11251 | 380 |
lemma NB_Crypt_imp_Server_msg [rule_format]: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
381 |
"\<lbrakk>B \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
382 |
\<Longrightarrow> Crypt (shrK B) \<lbrace>NB, Key K\<rbrace> \<in> parts (knows Spy evs) |
11251 | 383 |
--> (\<forall>X'. Says B Server |
61956 | 384 |
\<lbrace>NA, Agent A, Agent B, X', |
385 |
Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace> |
|
11251 | 386 |
\<in> set evs |
387 |
--> Says Server B |
|
61956 | 388 |
\<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, |
389 |
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> |
|
11251 | 390 |
\<in> set evs)" |
391 |
apply simp |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
392 |
apply (erule otway.induct, force, simp_all) |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
393 |
subgoal \<comment>\<open>Fake\<close> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
394 |
by blast |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
395 |
subgoal \<comment>\<open>OR2\<close> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
396 |
by (force dest!: OR2_parts_knows_Spy) |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
397 |
subgoal \<comment>\<open>OR3\<close> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
398 |
by (blast dest: unique_NB dest!: no_nonce_OR1_OR2) \<comment>\<open>OR3\<close> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
399 |
subgoal \<comment>\<open>OR4\<close> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
400 |
by (blast dest!: Crypt_imp_OR2) |
11251 | 401 |
done |
402 |
||
403 |
||
61830 | 404 |
text\<open>Guarantee for B: if it gets a message with matching NB then the Server |
405 |
has sent the correct message.\<close> |
|
13907 | 406 |
theorem B_trusts_OR3: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
407 |
"\<lbrakk>Says B Server \<lbrace>NA, Agent A, Agent B, X', |
61956 | 408 |
Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace> |
11251 | 409 |
\<in> set evs; |
61956 | 410 |
Gets B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs; |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
411 |
B \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
412 |
\<Longrightarrow> Says Server B |
61956 | 413 |
\<lbrace>NA, |
414 |
Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, |
|
415 |
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> |
|
11251 | 416 |
\<in> set evs" |
417 |
by (blast intro!: NB_Crypt_imp_Server_msg) |
|
418 |
||
419 |
||
61830 | 420 |
text\<open>The obvious combination of \<open>B_trusts_OR3\<close> with |
421 |
\<open>Spy_not_see_encrypted_key\<close>\<close> |
|
11251 | 422 |
lemma B_gets_good_key: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
423 |
"\<lbrakk>Says B Server \<lbrace>NA, Agent A, Agent B, X', |
61956 | 424 |
Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace> |
11251 | 425 |
\<in> set evs; |
61956 | 426 |
Gets B \<lbrace>NA, X, Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs; |
427 |
Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
428 |
A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
429 |
\<Longrightarrow> Key K \<notin> analz (knows Spy evs)" |
11251 | 430 |
by (blast dest!: B_trusts_OR3 Spy_not_see_encrypted_key) |
431 |
||
432 |
||
433 |
lemma OR3_imp_OR2: |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
434 |
"\<lbrakk>Says Server B |
61956 | 435 |
\<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>, |
436 |
Crypt (shrK B) \<lbrace>NB, Key K\<rbrace>\<rbrace> \<in> set evs; |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
437 |
B \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
438 |
\<Longrightarrow> \<exists>X. Says B Server \<lbrace>NA, Agent A, Agent B, X, |
61956 | 439 |
Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace> |
11251 | 440 |
\<in> set evs" |
441 |
apply (erule rev_mp) |
|
442 |
apply (erule otway.induct, simp_all) |
|
443 |
apply (blast dest!: Crypt_imp_OR2)+ |
|
444 |
done |
|
445 |
||
446 |
||
61830 | 447 |
text\<open>After getting and checking OR4, agent A can trust that B has been active. |
11251 | 448 |
We could probably prove that X has the expected form, but that is not |
61830 | 449 |
strictly necessary for authentication.\<close> |
13907 | 450 |
theorem A_auths_B: |
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
451 |
"\<lbrakk>Says B' A \<lbrace>NA, Crypt (shrK A) \<lbrace>NA, Key K\<rbrace>\<rbrace> \<in> set evs; |
61956 | 452 |
Says A B \<lbrace>NA, Agent A, Agent B, |
453 |
Crypt (shrK A) \<lbrace>NA, Agent A, Agent B\<rbrace>\<rbrace> \<in> set evs; |
|
63975
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
454 |
A \<notin> bad; B \<notin> bad; evs \<in> otway\<rbrakk> |
6728b5007ad0
Trying out "subgoal", and no more [| |]
paulson <lp15@cam.ac.uk>
parents:
61956
diff
changeset
|
455 |
\<Longrightarrow> \<exists>NB X. Says B Server \<lbrace>NA, Agent A, Agent B, X, |
61956 | 456 |
Crypt (shrK B) \<lbrace>NA, NB, Agent A, Agent B\<rbrace>\<rbrace> |
11251 | 457 |
\<in> set evs" |
458 |
by (blast dest!: A_trusts_OR4 OR3_imp_OR2) |
|
459 |
||
1941 | 460 |
end |