author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 7499  23e090051cb8 
child 10833  c0844a30ea4e 
permissions  rwrr 
4598
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

1 
(* Title: HOL/Auth/OtwayRees_AN 
2090  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Inductive relation "otway" for the OtwayRees protocol. 

7 

4598
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

8 
AbadiNeedham version: minimal encryption, explicit messages 
2090  9 

10 
From page 11 of 

11 
Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols. 

12 
IEEE Trans. SE 22 (1), 1996 

13 
*) 

14 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

15 
AddEs knows_Spy_partsEs; 
4470  16 
AddDs [impOfSubs analz_subset_parts]; 
17 
AddDs [impOfSubs Fake_parts_insert]; 

18 

2090  19 

2331  20 
(*A "possibility property": there are traces that reach the end*) 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

21 
Goal "[ B ~= Server ] \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

22 
\ ==> EX K. EX NA. EX evs: otway. \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

23 
\ Says B A (Crypt (shrK A) {Nonce NA, Agent A, Agent B, Key K}) \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

24 
\ : set evs"; 
2090  25 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

26 
by (rtac (otway.Nil RS 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

27 
otway.OR1 RS otway.Reception RS 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

28 
otway.OR2 RS otway.Reception RS 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

29 
otway.OR3 RS otway.Reception RS otway.OR4) 2); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

30 
by possibility_tac; 
2090  31 
result(); 
32 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

33 
Goal "[ Gets B X : set evs; evs : otway ] ==> EX A. Says A B X : set evs"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

34 
by (etac rev_mp 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

35 
by (etac otway.induct 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

36 
by Auto_tac; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

37 
qed"Gets_imp_Says"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

38 

76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

39 
(*Must be proved separately for each protocol*) 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

40 
Goal "[ Gets B X : set evs; evs : otway ] ==> X : knows Spy evs"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

41 
by (blast_tac (claset() addSDs [Gets_imp_Says, Says_imp_knows_Spy]) 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

42 
qed"Gets_imp_knows_Spy"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

43 
AddDs [Gets_imp_knows_Spy RS parts.Inj]; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

44 

2090  45 

46 
(**** Inductive proofs about otway ****) 

47 

48 
(** For reasoning about the encrypted portion of messages **) 

49 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

50 
Goal "[ Gets B {X, Crypt(shrK B) X'} : set evs; evs : otway ] ==> \ 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

51 
\ X : analz (knows Spy evs)"; 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

52 
by (blast_tac (claset() addSDs [Gets_imp_knows_Spy RS analz.Inj]) 1); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

53 
qed "OR4_analz_knows_Spy"; 
2090  54 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

55 
Goal "Says Server B {X, Crypt K' {NB, a, Agent B, K}} : set evs \ 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

56 
\ ==> K : parts (knows Spy evs)"; 
4470  57 
by (Blast_tac 1); 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

58 
qed "Oops_parts_knows_Spy"; 
2090  59 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

60 
bind_thm ("OR4_parts_knows_Spy", 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

61 
OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); 
2090  62 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

63 
(*For proving the easier theorems about X ~: parts (knows Spy evs).*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

64 
fun parts_induct_tac i = 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

65 
etac otway.induct i THEN 
7499  66 
ftac Oops_parts_knows_Spy (i+7) THEN 
67 
ftac OR4_parts_knows_Spy (i+6) THEN 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

68 
prove_simple_subgoals_tac i; 
2090  69 

70 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

71 
(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY 
2090  72 
sends messages containing X! **) 
73 

4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

74 
(*Spy never sees a good agent's shared key!*) 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

75 
Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

76 
by (parts_induct_tac 1); 
3961  77 
by (ALLGOALS Blast_tac); 
2131  78 
qed "Spy_see_shrK"; 
79 
Addsimps [Spy_see_shrK]; 

2090  80 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

81 
Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)"; 
4091  82 
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); 
2131  83 
qed "Spy_analz_shrK"; 
84 
Addsimps [Spy_analz_shrK]; 

2090  85 

4470  86 
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
87 
Spy_analz_shrK RSN (2, rev_iffD1)]; 

2090  88 

89 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

90 
(*Nobody can have used nonexistent keys!*) 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

91 
Goal "evs : otway ==> Key K ~: used evs > K ~: keysFor (parts (knows Spy evs))"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

92 
by (parts_induct_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

93 
(*Fake*) 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

94 
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

95 
(*OR3*) 
3102  96 
by (Blast_tac 1); 
2160  97 
qed_spec_mp "new_keys_not_used"; 
2090  98 

99 
bind_thm ("new_keys_not_analzd", 

100 
[analz_subset_parts RS keysFor_mono, 

101 
new_keys_not_used] MRS contra_subsetD); 

102 

103 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

104 

105 

106 

107 
(*** Proofs involving analz ***) 

108 

2131  109 
(*Describes the form of K and NA when the Server sends this message.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

110 
Goal "[ Says Server B \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

111 
\ {Crypt (shrK A) {NA, Agent A, Agent B, Key K}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

112 
\ Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

113 
\ : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

114 
\ evs : otway ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

115 
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; 
2131  116 
by (etac rev_mp 1); 
117 
by (etac otway.induct 1); 

3102  118 
by (ALLGOALS Asm_simp_tac); 
119 
by (Blast_tac 1); 

2131  120 
qed "Says_Server_message_form"; 
2090  121 

122 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

123 
(*For proofs involving analz.*) 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

124 
val analz_knows_Spy_tac = 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

125 
dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN 
7499  126 
ftac Says_Server_message_form 8 THEN assume_tac 8 THEN 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

127 
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8); 
2090  128 

129 

130 
(**** 

131 
The following is to prove theorems of the form 

132 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

133 
Key K : analz (insert (Key KAB) (knows Spy evs)) ==> 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

134 
Key K : analz (knows Spy evs) 
2090  135 

136 
A more general formula must be proved inductively. 

137 
****) 

138 

139 

140 
(** Session keys are not used to encrypt other session keys **) 

141 

142 
(*The equality makes the induction hypothesis easier to apply*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

143 
Goal "evs : otway ==> \ 
5492  144 
\ ALL K KK. KK <= (range shrK) > \ 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

145 
\ (Key K : analz (Key``KK Un (knows Spy evs))) = \ 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

146 
\ (K : KK  Key K : analz (knows Spy evs))"; 
2090  147 
by (etac otway.induct 1); 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

148 
by analz_knows_Spy_tac; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

149 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

150 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

151 
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

152 
(*Fake*) 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4155
diff
changeset

153 
by (spy_analz_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

154 
qed_spec_mp "analz_image_freshK"; 
2090  155 

156 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

157 
Goal "[ evs : otway; KAB ~: range shrK ] ==> \ 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

158 
\ Key K : analz (insert (Key KAB) (knows Spy evs)) = \ 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

159 
\ (K = KAB  Key K : analz (knows Spy evs))"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

160 
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

161 
qed "analz_insert_freshK"; 
2090  162 

163 

4155  164 
(*** The Key K uniquely identifies the Server's message. **) 
2090  165 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

166 
Goal "evs : otway ==> \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

167 
\ EX A' B' NA' NB'. ALL A B NA NB. \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

168 
\ Says Server B \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

169 
\ {Crypt (shrK A) {NA, Agent A, Agent B, K}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

170 
\ Crypt (shrK B) {NB, Agent A, Agent B, K}} : set evs \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

171 
\ > A=A' & B=B' & NA=NA' & NB=NB'"; 
2090  172 
by (etac otway.induct 1); 
4091  173 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
3730  174 
by (ALLGOALS Clarify_tac); 
2090  175 
(*Remaining cases: OR3 and OR4*) 
176 
by (ex_strip_tac 2); 

3102  177 
by (Blast_tac 2); 
2090  178 
by (expand_case_tac "K = ?y" 1); 
179 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

180 
(*...we assume X is a recent message and handle this case by contradiction*) 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

181 
by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); 
2090  182 
val lemma = result(); 
183 

184 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

185 
Goal "[ Says Server B \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

186 
\ {Crypt (shrK A) {NA, Agent A, Agent B, K}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

187 
\ Crypt (shrK B) {NB, Agent A, Agent B, K}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

188 
\ : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

189 
\ Says Server B' \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

190 
\ {Crypt (shrK A') {NA', Agent A', Agent B', K}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

191 
\ Crypt (shrK B') {NB', Agent A', Agent B', K}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

192 
\ : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

193 
\ evs : otway ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

194 
\ ==> A=A' & B=B' & NA=NA' & NB=NB'"; 
2417  195 
by (prove_unique_tac lemma 1); 
2090  196 
qed "unique_session_keys"; 
197 

198 

199 

200 
(**** Authenticity properties relating to NA ****) 

201 

202 
(*If the encrypted message appears then it originated with the Server!*) 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

203 
Goal "[ A ~: bad; A ~= B; evs : otway ] \ 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

204 
\ ==> Crypt (shrK A) {NA, Agent A, Agent B, Key K} : parts (knows Spy evs) \ 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

205 
\ > (EX NB. Says Server B \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

206 
\ {Crypt (shrK A) {NA, Agent A, Agent B, Key K}, \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

207 
\ Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

208 
\ : set evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

209 
by (parts_induct_tac 1); 
4470  210 
by (Blast_tac 1); 
4091  211 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); 
2090  212 
(*OR3*) 
3102  213 
by (Blast_tac 1); 
2090  214 
qed_spec_mp "NA_Crypt_imp_Server_msg"; 
215 

216 

2454  217 
(*Corollary: if A receives B's OR4 message then it originated with the Server. 
218 
Freshness may be inferred from nonce NA.*) 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

219 
Goal "[ Gets A (Crypt (shrK A) {NA, Agent A, Agent B, Key K}) \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

220 
\ : set evs; \ 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

221 
\ A ~: bad; A ~= B; evs : otway ] \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

222 
\ ==> EX NB. Says Server B \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

223 
\ {Crypt (shrK A) {NA, Agent A, Agent B, Key K}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

224 
\ Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

225 
\ : set evs"; 
4470  226 
by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); 
2331  227 
qed "A_trusts_OR4"; 
2090  228 

229 

230 
(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 

231 
Does not in itself guarantee security: an attack could violate 

232 
the premises, e.g. by having A=Spy **) 

233 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

234 
Goal "[ A ~: bad; B ~: bad; evs : otway ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

235 
\ ==> Says Server B \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

236 
\ {Crypt (shrK A) {NA, Agent A, Agent B, Key K}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

237 
\ Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

238 
\ : set evs > \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

239 
\ Notes Spy {NA, NB, Key K} ~: set evs > \ 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

240 
\ Key K ~: analz (knows Spy evs)"; 
2090  241 
by (etac otway.induct 1); 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

242 
by analz_knows_Spy_tac; 
2090  243 
by (ALLGOALS 
6915  244 
(asm_simp_tac (simpset() addcongs [conj_cong] 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

245 
addsimps [analz_insert_eq, analz_insert_freshK] 
5535  246 
@ pushes @ split_ifs))); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

247 
(*Oops*) 
4091  248 
by (blast_tac (claset() addSDs [unique_session_keys]) 4); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

249 
(*OR4*) 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

250 
by (Blast_tac 3); 
2090  251 
(*OR3*) 
4470  252 
by (Blast_tac 2); 
3451
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

253 
(*Fake*) 
d10f100676d8
Made proofs more concise by replacing calls to spy_analz_tac by uses of
paulson
parents:
3207
diff
changeset

254 
by (spy_analz_tac 1); 
2090  255 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
256 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

257 
Goal "[ Says Server B \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

258 
\ {Crypt (shrK A) {NA, Agent A, Agent B, Key K}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

259 
\ Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

260 
\ : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

261 
\ Notes Spy {NA, NB, Key K} ~: set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

262 
\ A ~: bad; B ~: bad; evs : otway ] \ 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

263 
\ ==> Key K ~: analz (knows Spy evs)"; 
7499  264 
by (ftac Says_Server_message_form 1 THEN assume_tac 1); 
4091  265 
by (blast_tac (claset() addSEs [lemma]) 1); 
2090  266 
qed "Spy_not_see_encrypted_key"; 
267 

268 

4598
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

269 
(*A's guarantee. The Oops premise quantifies over NB because A cannot know 
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

270 
what it is.*) 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

271 
Goal "[ Gets A (Crypt (shrK A) {NA, Agent A, Agent B, Key K}) \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

272 
\ : set evs; \ 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

273 
\ ALL NB. Notes Spy {NA, NB, Key K} ~: set evs; \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

274 
\ A ~: bad; B ~: bad; A ~= B; evs : otway ] \ 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

275 
\ ==> Key K ~: analz (knows Spy evs)"; 
4598
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

276 
by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1); 
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

277 
qed "A_gets_good_key"; 
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

278 

649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

279 

2090  280 
(**** Authenticity properties relating to NB ****) 
281 

282 
(*If the encrypted message appears then it originated with the Server!*) 

5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

283 
Goal "[ B ~: bad; A ~= B; evs : otway ] \ 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

284 
\ ==> Crypt (shrK B) {NB, Agent A, Agent B, Key K} : parts (knows Spy evs) \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

285 
\ > (EX NA. Says Server B \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

286 
\ {Crypt (shrK A) {NA, Agent A, Agent B, Key K}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

287 
\ Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

288 
\ : set evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

289 
by (parts_induct_tac 1); 
4470  290 
by (Blast_tac 1); 
4091  291 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); 
2090  292 
(*OR3*) 
3102  293 
by (Blast_tac 1); 
2090  294 
qed_spec_mp "NB_Crypt_imp_Server_msg"; 
295 

296 

2454  297 
(*Guarantee for B: if it gets a wellformed certificate then the Server 
298 
has sent the correct message in round 3.*) 

6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

299 
Goal "[ Gets B {X, Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

300 
\ : set evs; \ 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

301 
\ B ~: bad; A ~= B; evs : otway ] \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

302 
\ ==> EX NA. Says Server B \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

303 
\ {Crypt (shrK A) {NA, Agent A, Agent B, Key K}, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

304 
\ Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

305 
\ : set evs"; 
4470  306 
by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); 
2331  307 
qed "B_trusts_OR3"; 
4598
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

308 

649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

309 

649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

310 
(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

311 
Goal "[ Gets B {X, Crypt (shrK B) {NB, Agent A, Agent B, Key K}} \ 
5434
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

312 
\ : set evs; \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

313 
\ ALL NA. Notes Spy {NA, NB, Key K} ~: set evs; \ 
9b4bed3f394c
Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents:
5421
diff
changeset

314 
\ A ~: bad; B ~: bad; A ~= B; evs : otway ] \ 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

315 
\ ==> Key K ~: analz (knows Spy evs)"; 
4598
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

316 
by (blast_tac (claset() addDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1); 
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

317 
qed "B_gets_good_key"; 