author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 8215  d3eba67a9e67 
child 10833  c0844a30ea4e 
permissions  rwrr 
1941  1 
(* Title: HOL/Auth/OtwayRees 
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 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

8 
Version that encrypts Nonce NB 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

9 

1941  10 
From page 244 of 
11 
Burrows, Abadi and Needham. A Logic of Authentication. 

12 
Proc. Royal Soc. 426 (1989) 

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 

1996
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

19 

2328  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 ] \ 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

22 
\ ==> EX NA K. EX evs: otway. \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

24 
\ : set evs"; 
1996
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

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:
2451
diff
changeset

30 
by possibility_tac; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

31 
result(); 
1996
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

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 

1996
33c42cae3dd0
Uses the improved enemy_analz_tac of Shared.ML, with simpler proofs
paulson
parents:
1967
diff
changeset

45 

1941  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 {N, Agent A, Agent 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 "OR2_analz_knows_Spy"; 
1941  54 

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

55 
Goal "[ Gets B {N, 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

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

57 
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

58 
qed "OR4_analz_knows_Spy"; 
1941  59 

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

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

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

63 
qed "Oops_parts_knows_Spy"; 
1941  64 

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

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

66 
OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts)); 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

67 
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

68 
OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); 
2032  69 

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

70 
(*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

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

72 
etac otway.induct i THEN 
7499  73 
ftac Oops_parts_knows_Spy (i+7) THEN 
74 
ftac OR4_parts_knows_Spy (i+6) THEN 

75 
ftac OR2_parts_knows_Spy (i+4) THEN 

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

76 
prove_simple_subgoals_tac i; 
1941  77 

78 

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

79 
(** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

80 
sends messages containing X! **) 
1941  81 

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

82 
(*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

83 
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

84 
by (parts_induct_tac 1); 
3961  85 
by (ALLGOALS Blast_tac); 
2135  86 
qed "Spy_see_shrK"; 
87 
Addsimps [Spy_see_shrK]; 

1941  88 

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

89 
Goal "evs : otway ==> (Key (shrK A) : analz (knows Spy evs)) = (A : bad)"; 
4091  90 
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); 
2135  91 
qed "Spy_analz_shrK"; 
92 
Addsimps [Spy_analz_shrK]; 

1941  93 

4470  94 
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
95 
Spy_analz_shrK RSN (2, rev_iffD1)]; 

1941  96 

97 

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

98 
(*Nobody can have used nonexistent keys!*) 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

99 
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

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

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

102 
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

103 
(*OR2, OR3*) 
3102  104 
by (ALLGOALS Blast_tac); 
2160  105 
qed_spec_mp "new_keys_not_used"; 
1941  106 

107 
bind_thm ("new_keys_not_analzd", 

2032  108 
[analz_subset_parts RS keysFor_mono, 
109 
new_keys_not_used] MRS contra_subsetD); 

1941  110 

111 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 

112 

113 

2064  114 

115 
(*** Proofs involving analz ***) 

116 

2135  117 
(*Describes the form of K and NA when the Server sends this message. Also 
118 
for Oops case.*) 

5278  119 
Goal "[ Says Server B {NA, X, Crypt (shrK B) {NB, Key K}} : set evs; \ 
5359  120 
\ evs : otway ] \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

121 
\ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; 
2135  122 
by (etac rev_mp 1); 
123 
by (etac otway.induct 1); 

3102  124 
by (ALLGOALS Simp_tac); 
125 
by (ALLGOALS Blast_tac); 

2135  126 
qed "Says_Server_message_form"; 
2064  127 

128 

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

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

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

131 
dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

132 
dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN 
7499  133 
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

134 
REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8); 
1941  135 

136 

137 
(**** 

138 
The following is to prove theorems of the form 

139 

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

140 
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

141 
Key K : analz (knows Spy evs) 
1941  142 

143 
A more general formula must be proved inductively. 

144 
****) 

145 

146 

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

148 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

149 
(*The equality makes the induction hypothesis easier to apply*) 
5492  150 
Goal "evs : otway ==> 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

151 
\ (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

152 
\ (K : KK  Key K : analz (knows Spy evs))"; 
2032  153 
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

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

155 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
5359  156 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

157 
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

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

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

160 
qed_spec_mp "analz_image_freshK"; 
1941  161 

162 

5359  163 
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

164 
\ ==> 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

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

166 
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:
2451
diff
changeset

167 
qed "analz_insert_freshK"; 
1941  168 

169 

2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

170 
(*** The Key K uniquely identifies the Server's message. **) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

171 

5278  172 
Goal "evs : otway ==> \ 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

173 
\ EX B' NA' NB' X'. ALL B NA NB X. \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

174 
\ Says Server B {NA, X, Crypt (shrK B) {NB, K}} : set evs > \ 
2135  175 
\ B=B' & NA=NA' & NB=NB' & X=X'"; 
2032  176 
by (etac otway.induct 1); 
4091  177 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
3730  178 
by (ALLGOALS Clarify_tac); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

179 
(*Remaining cases: OR3 and OR4*) 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

180 
by (ex_strip_tac 2); 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

181 
by (Best_tac 2); (*Blast_tac's too slow (in reconstruction)*) 
2064  182 
by (expand_case_tac "K = ?y" 1); 
183 
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:
2451
diff
changeset

184 
(*...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

185 
by (blast_tac (claset() addSEs knows_Spy_partsEs) 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

186 
val lemma = result(); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

187 

5278  188 
Goal "[ Says Server B {NA, X, Crypt (shrK B) {NB, K}} : set evs; \ 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

189 
\ Says Server B' {NA',X',Crypt (shrK B') {NB',K}} : set evs; \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

190 
\ evs : otway ] ==> X=X' & B=B' & NA=NA' & NB=NB'"; 
2417  191 
by (prove_unique_tac lemma 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

192 
qed "unique_session_keys"; 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

193 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

194 

2048  195 
(**** Authenticity properties relating to NA ****) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

196 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

197 
(*Only OR1 can have caused such a part of a message to appear.*) 
5278  198 
Goal "[ A ~: bad; evs : otway ] \ 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

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

200 
\ Says A B {NA, Agent A, Agent B, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

201 
\ Crypt (shrK A) {NA, Agent A, Agent B}} \ 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

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

203 
by (parts_induct_tac 1); 
4470  204 
by (Blast_tac 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

205 
qed_spec_mp "Crypt_imp_OR1"; 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

206 

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

207 
Goal "[ Gets B {NA, Agent A, Agent B, \ 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

208 
\ Crypt (shrK A) {NA, Agent A, Agent B}} : set evs; \ 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

209 
\ A ~: bad; evs : otway ] \ 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

210 
\ ==> Says A B {NA, Agent A, Agent B, \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

211 
\ Crypt (shrK A) {NA, Agent A, Agent B}} \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

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

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

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

215 

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

216 

2064  217 
(** The Nonce NA uniquely identifies A's message. **) 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

218 

5278  219 
Goal "[ evs : otway; A ~: bad ] \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

220 
\ ==> EX B'. ALL B. \ 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

221 
\ Crypt (shrK A) {NA, Agent A, Agent B} : parts (knows Spy evs) \ 
2048  222 
\ > B = B'"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

223 
by (parts_induct_tac 1); 
4470  224 
by (Blast_tac 1); 
4091  225 
by (simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
2026
0df5a96bf77e
Last working version prior to introduction of "lost"
paulson
parents:
2014
diff
changeset

226 
(*OR1: creation of new Nonce. Move assertion into global context*) 
2064  227 
by (expand_case_tac "NA = ?y" 1); 
4470  228 
by (Blast_tac 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

229 
val lemma = result(); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

230 

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

231 
Goal "[ Crypt (shrK A) {NA, Agent A, Agent B}: parts (knows Spy evs); \ 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

232 
\ Crypt (shrK A) {NA, Agent A, Agent C}: parts (knows Spy evs); \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

233 
\ evs : otway; A ~: bad ] \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

234 
\ ==> B = C"; 
2417  235 
by (prove_unique_tac lemma 1); 
2048  236 
qed "unique_NA"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

237 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

238 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

239 
(*It is impossible to reuse a nonce in both OR1 and OR2. This holds because 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

240 
OR2 encrypts Nonce NB. It prevents the attack that can occur in the 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

241 
oversimplified version of this protocol: see OtwayRees_Bad.*) 
5278  242 
Goal "[ A ~: bad; evs : otway ] \ 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

243 
\ ==> Crypt (shrK A) {NA, Agent A, Agent B} : parts (knows Spy evs) > \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

244 
\ Crypt (shrK A) {NA', NA, Agent A', Agent A} \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

245 
\ ~: parts (knows Spy evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

248 
qed_spec_mp "no_nonce_OR1_OR2"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

249 

4470  250 
val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

251 

2053  252 
(*Crucial property: If the encrypted message appears, and A has used NA 
253 
to start a run, then it originated with the Server!*) 

5278  254 
Goal "[ A ~: bad; evs : otway ] \ 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

255 
\ ==> Crypt (shrK A) {NA, Key K} : parts (knows Spy evs) \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

256 
\ > Says A B {NA, Agent A, Agent B, \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

257 
\ Crypt (shrK A) {NA, Agent A, Agent B}} \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

258 
\ : set evs > \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

259 
\ (EX NB. Says Server B \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

260 
\ {NA, \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

261 
\ Crypt (shrK A) {NA, Key K}, \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

262 
\ Crypt (shrK B) {NB, Key K}} \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

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

264 
by (parts_induct_tac 1); 
4470  265 
by (Blast_tac 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

266 
(*OR1: it cannot be a new Nonce, contradiction.*) 
4470  267 
by (Blast_tac 1); 
3730  268 
(*OR3 and OR4*) 
4091  269 
by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); 
3730  270 
by (rtac conjI 1); 
271 
by (ALLGOALS Clarify_tac); 

272 
(*OR4*) 

4470  273 
by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 3); 
274 
(*OR3, two cases*) (** LEVEL 7 **) 

275 
by (blast_tac (claset() addSEs [nonce_OR1_OR2_E] 

276 
delrules [conjI] (*stop splitup into 4 subgoals*)) 2); 

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

277 
by (blast_tac (claset() addIs [unique_NA]) 1); 
2048  278 
qed_spec_mp "NA_Crypt_imp_Server_msg"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

279 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

280 

2053  281 
(*Corollary: if A receives B's OR4 message and the nonce NA agrees 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

282 
then the key really did come from the Server! CANNOT prove this of the 
2048  283 
bad form of this protocol, even though we can prove 
2032  284 
Spy_not_see_encrypted_key*) 
5278  285 
Goal "[ Says A B {NA, Agent A, Agent B, \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

286 
\ Crypt (shrK A) {NA, Agent A, Agent B}} : set evs; \ 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

287 
\ Gets A {NA, Crypt (shrK A) {NA, Key K}} : set evs; \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

290 
\ {NA, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

293 
\ : set evs"; 
4470  294 
by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); 
2328  295 
qed "A_trusts_OR4"; 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

296 

5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

297 

2048  298 
(** Crucial secrecy property: Spy does not see the keys sent in msg OR3 
299 
Does not in itself guarantee security: an attack could violate 

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

2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

301 

8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

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

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

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

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

306 
\ 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

307 
\ Key K ~: analz (knows Spy evs)"; 
2032  308 
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

309 
by analz_knows_Spy_tac; 
1964  310 
by (ALLGOALS 
4091  311 
(asm_simp_tac (simpset() addcongs [conj_cong] 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

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

314 
(*Oops*) 
4091  315 
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

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

317 
by (Blast_tac 3); 
1941  318 
(*OR3*) 
4470  319 
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

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

321 
by (spy_analz_tac 1); 
2014
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

322 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
5be4c8ca7b25
Correction of protocol; addition of Reveal message; proofs of
paulson
parents:
1999
diff
changeset

323 

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

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

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

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

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

328 
\ 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

329 
\ ==> Key K ~: analz (knows Spy evs)"; 
7499  330 
by (ftac Says_Server_message_form 1 THEN assume_tac 1); 
4091  331 
by (blast_tac (claset() addSEs [lemma]) 1); 
2032  332 
qed "Spy_not_see_encrypted_key"; 
333 

1945  334 

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

335 
(*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

336 
what it is.*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

337 
Goal "[ Says A B {NA, Agent A, Agent B, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

338 
\ Crypt (shrK A) {NA, Agent A, Agent B}} : set evs; \ 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

339 
\ Gets A {NA, Crypt (shrK A) {NA, Key K}} : set evs; \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

341 
\ 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

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

343 
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

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

345 

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

346 

2048  347 
(**** Authenticity properties relating to NB ****) 
348 

349 
(*Only OR2 can have caused such a part of a message to appear. We do not 

2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

350 
know anything about X: it does NOT have to have the right form.*) 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

351 
Goal "[ Crypt (shrK B) {NA, NB, Agent A, Agent B} \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

352 
\ : parts (knows Spy evs); \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

353 
\ B ~: bad; evs : otway ] \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

354 
\ ==> EX X. Says B Server \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

355 
\ {NA, Agent A, Agent B, X, \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

356 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B}} \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

357 
\ : set evs"; 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

358 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

359 
by (parts_induct_tac 1); 
3102  360 
by (ALLGOALS Blast_tac); 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

361 
qed "Crypt_imp_OR2"; 
2048  362 

363 

364 
(** The Nonce NB uniquely identifies B's message. **) 

365 

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

366 
Goal "[ evs : otway; B ~: bad ] \ 
4598
649bf14debe7
Added some more explicit guarantees of key secrecy for agents
paulson
parents:
4537
diff
changeset

367 
\ ==> EX NA' A'. ALL NA A. \ 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

368 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B} : parts(knows Spy evs) \ 
2048  369 
\ > NA = NA' & A = A'"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

370 
by (parts_induct_tac 1); 
4470  371 
by (Blast_tac 1); 
4091  372 
by (simp_tac (simpset() addsimps [all_conj_distrib]) 1); 
2048  373 
(*OR2: creation of new Nonce. Move assertion into global context*) 
2064  374 
by (expand_case_tac "NB = ?y" 1); 
4470  375 
by (Blast_tac 1); 
2048  376 
val lemma = result(); 
377 

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

378 
Goal "[ Crypt (shrK B) {NA, NB, Agent A, Agent B} : parts(knows Spy evs); \ 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

379 
\ Crypt (shrK B) {NC, NB, Agent C, Agent B} : parts(knows Spy evs); \ 
3683  380 
\ evs : otway; B ~: bad ] \ 
2048  381 
\ ==> NC = NA & C = A"; 
2417  382 
by (prove_unique_tac lemma 1); 
2048  383 
qed "unique_NB"; 
384 

385 
(*If the encrypted message appears, and B has used Nonce NB, 

386 
then it originated with the Server!*) 

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

387 
Goal "[ B ~: bad; evs : otway ] \ 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

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

389 
\ > (ALL X'. Says B Server \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

390 
\ {NA, Agent A, Agent B, X', \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

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

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

395 
\ Crypt (shrK B) {NB, Key K}} \ 
3465  396 
\ : set evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

397 
by (parts_induct_tac 1); 
4470  398 
by (Blast_tac 1); 
2048  399 
(*OR1: it cannot be a new Nonce, contradiction.*) 
4470  400 
by (Blast_tac 1); 
2048  401 
(*OR4*) 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

402 
by (blast_tac (claset() addSDs [Crypt_imp_OR2]) 2); 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

403 
(*OR3*) 
4470  404 
(*Provable in 38s by the single command 
405 
by (blast_tac (claset() addDs [unique_NB] addEs[nonce_OR1_OR2_E]) 1); 

406 
*) 

4091  407 
by (safe_tac (claset() delrules [disjCI, impCE])); 
4470  408 
by (Blast_tac 3); 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

409 
by (blast_tac (claset() addSDs [unique_NB] 
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5535
diff
changeset

410 
delrules [impCE] (*stop splitup*)) 2); 
4470  411 
by (blast_tac (claset() addSEs [nonce_OR1_OR2_E] 
412 
delrules [conjI] (*stop splitup*)) 1); 

2048  413 
qed_spec_mp "NB_Crypt_imp_Server_msg"; 
414 

415 

416 
(*Guarantee for B: if it gets a message with matching NB then the Server 

417 
has sent the correct message.*) 

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

418 
Goal "[ Says B Server {NA, Agent A, Agent B, X', \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

419 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B} } \ 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

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

421 
\ Gets B {NA, X, Crypt (shrK B) {NB, Key K}} : set evs; \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

424 
\ {NA, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

427 
\ : set evs"; 
4470  428 
by (blast_tac (claset() addSIs [NB_Crypt_imp_Server_msg]) 1); 
2328  429 
qed "B_trusts_OR3"; 
2048  430 

431 

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

432 
(*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

433 
Goal "[ Says B Server {NA, Agent A, Agent B, X', \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

436 
\ Gets B {NA, X, Crypt (shrK B) {NB, Key K}} : set evs; \ 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

438 
\ 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

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

440 
by (blast_tac (claset() addSDs [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

441 
qed "B_gets_good_key"; 
2048  442 

443 

8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

444 
Goal "[ Says Server B \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

445 
\ {NA, Crypt (shrK A) {NA, Key K}, \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

446 
\ Crypt (shrK B) {NB, Key K}} : set evs; \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

447 
\ B ~: bad; evs : otway ] \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

448 
\ ==> EX X. Says B Server {NA, Agent A, Agent B, X, \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

449 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B} } \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

450 
\ : set evs"; 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

451 
by (etac rev_mp 1); 
2032  452 
by (etac otway.induct 1); 
3102  453 
by (ALLGOALS Asm_simp_tac); 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

454 
by (blast_tac (claset() addSDs [Crypt_imp_OR2]) 3); 
3102  455 
by (ALLGOALS Blast_tac); 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

456 
qed "OR3_imp_OR2"; 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

457 

63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

458 

63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

459 
(*After getting and checking OR4, agent A can trust that B has been active. 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

460 
We could probably prove that X has the expected form, but that is not 
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

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

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

463 
\ Says A B {NA, Agent A, Agent B, \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

465 
\ A ~: bad; B ~: bad; evs : otway ] \ 
8215
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

466 
\ ==> EX NB X. Says B Server {NA, Agent A, Agent B, X, \ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

467 
\ Crypt (shrK B) {NA, NB, Agent A, Agent B} }\ 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

468 
\ : set evs"; 
d3eba67a9e67
tidying: mostly spacing, but also simpler forms for Crypt_imp_OR2 & OR3_imp_OR2
paulson
parents:
7499
diff
changeset

469 
by (blast_tac (claset() addSDs [A_trusts_OR4, OR3_imp_OR2]) 1); 
2194
63a68a3a8a76
Removal of an obsolete result, and authentication of
paulson
parents:
2171
diff
changeset

470 
qed "A_auths_B"; 