--- a/src/HOL/Auth/Recur.ML Fri Jan 17 11:50:09 1997 +0100
+++ b/src/HOL/Auth/Recur.ML Fri Jan 17 12:49:31 1997 +0100
@@ -10,29 +10,26 @@
proof_timing:=true;
HOL_quantifiers := false;
-Pretty.setdepth 25;
+Pretty.setdepth 30;
(** Possibility properties: traces that reach the end
- ONE theorem would be more elegant and faster!
- By induction on a list of agents (no repetitions)
+ ONE theorem would be more elegant and faster!
+ By induction on a list of agents (no repetitions)
**)
+
(*Simplest case: Alice goes directly to the server*)
goal thy
"!!A. A ~= Server \
\ ==> EX K NA. EX evs: recur lost. \
-\ Says Server A {|Agent A, \
-\ Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
+\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
\ Agent Server|} \
\ : set_of_list evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (recur.Nil RS recur.RA1 RS
- (respond.One RSN (4,recur.RA3))) 2);
-by (REPEAT
- (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))
- THEN
- REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])));
+ (respond.One RSN (4,recur.RA3))) 2);
+by possibility_tac;
result();
@@ -40,44 +37,42 @@
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
\ ==> EX K. EX NA. EX evs: recur lost. \
-\ Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
+\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
\ Agent Server|} \
\ : set_of_list evs";
+by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
+by (REPEAT (eresolve_tac [exE, conjE] 1));
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS
- (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
- recur.RA4) 2);
-bw HPair_def;
-by (REPEAT
- (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
- THEN
- ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))));
+ (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
+ recur.RA4) 2);
+by basic_possibility_tac;
+by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2,
+ less_not_refl2 RS not_sym] 1));
result();
-(*Case three: Alice, Bob, Charlie and the server*)
+(*Case three: Alice, Bob, Charlie and the server
goal thy
- "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
+ "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |] \
\ ==> EX K. EX NA. EX evs: recur lost. \
-\ Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
+\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
\ Agent Server|} \
\ : set_of_list evs";
+by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
+by (REPEAT (eresolve_tac [exE, conjE] 1));
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS
- (respond.One RS respond.Cons RS respond.Cons RSN
- (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
-bw HPair_def;
-by (REPEAT (*SLOW: 37 seconds*)
- (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
- THEN
- ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))));
-by (ALLGOALS
- (SELECT_GOAL (DEPTH_SOLVE
- (swap_res_tac [refl, conjI, disjI1, disjI2] 1 APPEND
- etac not_sym 1))));
+ (respond.One RS respond.Cons RS respond.Cons RSN
+ (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
+(*SLOW: 70 seconds*)
+by basic_possibility_tac;
+by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1
+ ORELSE
+ eresolve_tac [asm_rl, less_not_refl2,
+ less_not_refl2 RS not_sym] 1));
result();
-
-
+****************)
(**** Inductive proofs about recur ****)
@@ -99,10 +94,30 @@
AddSEs [not_Says_to_self RSN (2, rev_notE)];
+
+goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
+by (etac respond.induct 1);
+by (ALLGOALS Simp_tac);
+qed "respond_Key_in_parts";
+
+goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs";
+by (etac respond.induct 1);
+by (REPEAT (assume_tac 1));
+qed "respond_imp_not_used";
+
+goal thy
+ "!!evs. [| Key K : parts {RB}; (PB,RB,K') : respond evs |] \
+\ ==> Key K ~: used evs";
+by (etac rev_mp 1);
+by (etac respond.induct 1);
+by (auto_tac(!claset addDs [Key_not_used, respond_imp_not_used],
+ !simpset));
+qed_spec_mp "Key_in_parts_respond";
+
(*Simple inductive reasoning about responses*)
-goal thy "!!j. (j,PA,RB) : respond i ==> RB : responses i";
+goal thy "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs";
by (etac respond.induct 1);
-by (REPEAT (ares_tac responses.intrs 1));
+by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1));
qed "respond_imp_responses";
@@ -110,7 +125,7 @@
val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
-goal thy "!!evs. Says C' B {|Agent B, X, Agent B, X', RA|} : set_of_list evs \
+goal thy "!!evs. Says C' B {|X, X', RA|} : set_of_list evs \
\ ==> RA : analz (sees lost Spy evs)";
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
qed "RA4_analz_sees_Spy";
@@ -131,8 +146,8 @@
let val tac = forw_inst_tac [("lost","lost")]
in tac RA2_parts_sees_Spy 4 THEN
etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN
- forward_tac [respond_imp_responses] 5 THEN
- tac RA4_parts_sees_Spy 6
+ forward_tac [respond_imp_responses] 5 THEN
+ tac RA4_parts_sees_Spy 6
end;
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
@@ -153,14 +168,6 @@
(** Spy never sees another agent's long-term key (unless initially lost) **)
goal thy
- "!!evs. (j,PB,RB) : respond i \
-\ ==> Key K : parts {RB} --> (EX j'. K = newK2(i,j') & j<=j')";
-be respond.induct 1;
-by (Auto_tac());
-by (best_tac (!claset addDs [Suc_leD]) 1);
-qed_spec_mp "Key_in_parts_respond";
-
-goal thy
"!!evs. evs : recur lost \
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
by (parts_induct_tac 1);
@@ -189,115 +196,30 @@
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
-(*** Future keys can't be seen or used! ***)
+
+(** Nobody can have used non-existent keys! **)
-(*Nobody can have SEEN keys that will be generated in the future. *)
-goal thy "!!evs. evs : recur lost ==> \
-\ length evs <= i --> \
-\ Key (newK2(i,j)) ~: parts (sees lost Spy evs)";
-by (parts_induct_tac 1);
-(*RA2*)
-by (best_tac (!claset addSEs partsEs
- addSDs [parts_cut]
- addDs [Suc_leD]
- addss (!simpset)) 3);
-(*Fake*)
-by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset)) 1);
-(*For RA3*)
-by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 2);
-(*RA1-RA4*)
-by (REPEAT (best_tac (!claset addDs [Key_in_parts_respond, Suc_leD]
- addss (!simpset)) 1));
-qed_spec_mp "new_keys_not_seen";
-Addsimps [new_keys_not_seen];
-
-(*Variant: old messages must contain old keys!*)
-goal thy
- "!!evs. [| Says A B X : set_of_list evs; \
-\ Key (newK2(i,j)) : parts {X}; \
-\ evs : recur lost \
-\ |] ==> i < length evs";
-by (rtac ccontr 1);
-by (dtac leI 1);
-by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
- addIs [impOfSubs parts_mono]) 1);
-qed "Says_imp_old_keys";
-
-
-(*** Future nonces can't be seen or used! ***)
-
-goal thy
- "!!evs. (j, PB, RB) : respond i \
-\ ==> Nonce N : parts {RB} --> Nonce N : parts {PB}";
-be respond.induct 1;
+goal thy
+ "!!evs. [| K : keysFor (parts {RB}); (PB,RB,K') : respond evs |] \
+\ ==> K : range shrK";
+by (etac rev_mp 1);
+by (etac (respond_imp_responses RS responses.induct) 1);
by (Auto_tac());
-qed_spec_mp "Nonce_in_parts_respond";
+qed_spec_mp "Key_in_keysFor_parts";
-goal thy "!!i. evs : recur lost ==> \
-\ length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)";
-by (parts_induct_tac 1);
-(*For RA3*)
-by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 4);
-by (deepen_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
- addDs [Nonce_in_parts_respond, parts_cut, Suc_leD]
- addss (!simpset)) 0 4);
-(*Fake*)
-by (fast_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset)) 1);
-(*RA1, RA2, RA4*)
-by (REPEAT_FIRST (fast_tac (!claset
- addSEs partsEs
- addEs [leD RS notE]
- addDs [Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_nonces_not_seen";
-Addsimps [new_nonces_not_seen];
-
-(*Variant: old messages must contain old nonces!*)
-goal thy "!!evs. [| Says A B X : set_of_list evs; \
-\ Nonce (newN i) : parts {X}; \
-\ evs : recur lost \
-\ |] ==> i < length evs";
-by (rtac ccontr 1);
-by (dtac leI 1);
-by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
- addIs [impOfSubs parts_mono]) 1);
-qed "Says_imp_old_nonces";
-
-
-(** Nobody can have USED keys that will be generated in the future. **)
-
-goal thy
- "!!evs. (j,PB,RB) : respond i \
-\ ==> K : keysFor (parts {RB}) --> (EX A. K = shrK A)";
-be (respond_imp_responses RS responses.induct) 1;
-by (Auto_tac());
-qed_spec_mp "Key_in_keysFor_parts_respond";
-
-
-goal thy "!!i. evs : recur lost ==> \
-\ length evs <= i --> newK2(i,j) ~: keysFor (parts (sees lost Spy evs))";
+goal thy "!!evs. evs : recur lost ==> \
+\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
by (parts_induct_tac 1);
(*RA3*)
-by (fast_tac (!claset addDs [Key_in_keysFor_parts_respond, Suc_leD]
- addss (!simpset addsimps [parts_insert_sees])) 4);
-(*RA2*)
-by (fast_tac (!claset addSEs partsEs
- addDs [Suc_leD] addss (!simpset)) 3);
-(*Fake, RA1, RA4*)
-by (REPEAT
- (best_tac
- (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
- impOfSubs (parts_insert_subset_Un RS keysFor_mono),
- Suc_leD]
- addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
- addss (!simpset)) 1));
+by (best_tac (!claset addDs [Key_in_keysFor_parts]
+ addss (!simpset addsimps [parts_insert_sees])) 2);
+(*Fake*)
+by (best_tac
+ (!claset addIs [impOfSubs analz_subset_parts]
+ addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
+ impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
+ addss (!simpset)) 1);
qed_spec_mp "new_keys_not_used";
@@ -319,86 +241,82 @@
dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6;
-Delsimps [image_insert];
-
(** Session keys are not used to encrypt other session keys **)
(*Version for "responses" relation. Handles case RA3 in the theorem below.
Note that it holds for *any* set H (not just "sees lost Spy evs")
satisfying the inductive hypothesis.*)
goal thy
- "!!evs. [| RB : responses i; \
-\ ALL K I. (Key K : analz (Key``(newK``I) Un H)) = \
-\ (K : newK``I | Key K : analz H) |] \
-\ ==> ALL K I. (Key K : analz (insert RB (Key``(newK``I) Un H))) = \
-\ (K : newK``I | Key K : analz (insert RB H))";
-be responses.induct 1;
-by (ALLGOALS
- (asm_simp_tac
- (!simpset addsimps [insert_Key_singleton, insert_Key_image,
- Un_assoc RS sym, pushKey_newK]
- setloop split_tac [expand_if])));
-by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
-qed "resp_analz_image_newK_lemma";
+ "!!evs. [| RB : responses evs; \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un H)) = \
+\ (K : KK | Key K : analz H) |] \
+\ ==> ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (insert RB (Key``KK Un H))) = \
+\ (K : KK | Key K : analz (insert RB H))";
+by (etac responses.induct 1);
+by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
+qed "resp_analz_image_freshK_lemma";
(*Version for the protocol. Proof is almost trivial, thanks to the lemma.*)
goal thy
- "!!evs. evs : recur lost ==> \
-\ ALL K I. (Key K : analz (Key``(newK``I) Un (sees lost Spy evs))) = \
-\ (K : newK``I | Key K : analz (sees lost Spy evs))";
+ "!!evs. evs : recur lost ==> \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
+\ (K : KK | Key K : analz (sees lost Spy evs))";
by (etac recur.induct 1);
by analz_Fake_tac;
-by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [resp_analz_image_newK_lemma])));
+by (REPEAT_FIRST (resolve_tac [allI, impI]));
+by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
+by (ALLGOALS
+ (asm_simp_tac
+ (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
(*Base*)
by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
(*RA4, RA2, Fake*)
by (REPEAT (spy_analz_tac 1));
-val raw_analz_image_newK = result();
-qed_spec_mp "analz_image_newK";
+val raw_analz_image_freshK = result();
+qed_spec_mp "analz_image_freshK";
(*Instance of the lemma with H replaced by (sees lost Spy evs):
- [| RB : responses i; evs : recur lost |]
- ==> Key xa : analz (insert RB (Key``newK``x Un sees lost Spy evs)) =
- (xa : newK``x | Key xa : analz (insert RB (sees lost Spy evs)))
+ [| RB : responses evs; evs : recur lost; |]
+ ==> KK <= Compl (range shrK) -->
+ Key K : analz (insert RB (Key``KK Un sees lost Spy evs)) =
+ (K : KK | Key K : analz (insert RB (sees lost Spy evs)))
*)
-bind_thm ("resp_analz_image_newK",
- raw_analz_image_newK RSN
- (2, resp_analz_image_newK_lemma) RS spec RS spec);
+bind_thm ("resp_analz_image_freshK",
+ raw_analz_image_freshK RSN
+ (2, resp_analz_image_freshK_lemma) RS spec RS spec);
goal thy
- "!!evs. evs : recur lost ==> \
-\ Key K : analz (insert (Key (newK x)) (sees lost Spy evs)) = \
-\ (K = newK x | Key K : analz (sees lost Spy evs))";
-by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
- insert_Key_singleton]) 1);
-by (Fast_tac 1);
-qed "analz_insert_Key_newK";
+ "!!evs. [| evs : recur lost; KAB ~: range shrK |] ==> \
+\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
+\ (K = KAB | Key K : analz (sees lost Spy evs))";
+by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
+qed "analz_insert_freshK";
-(*This is more general than proving Hash_new_nonces_not_seen: we don't prove
- that "future nonces" can't be hashed, but that everything that's hashed is
- already in past traffic. *)
+(*Everything that's hashed is already in past traffic. *)
goal thy "!!i. [| evs : recur lost; A ~: lost |] ==> \
\ Hash {|Key(shrK A), X|} : parts (sees lost Spy evs) --> \
\ X : parts (sees lost Spy evs)";
-be recur.induct 1;
+by (etac recur.induct 1);
by parts_Fake_tac;
(*RA3 requires a further induction*)
-be responses.induct 5;
+by (etac responses.induct 5);
by (ALLGOALS Asm_simp_tac);
(*Fake*)
by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
- impOfSubs Fake_parts_insert]
- addss (!simpset addsimps [parts_insert_sees])) 2);
+ impOfSubs Fake_parts_insert]
+ addss (!simpset addsimps [parts_insert_sees])) 2);
(*Two others*)
by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
bind_thm ("Hash_imp_body", result() RSN (2, rev_mp));
(** The Nonce NA uniquely identifies A's message.
- This theorem applies to rounds RA1 and RA2!
+ This theorem applies to steps RA1 and RA2!
Unicity is not used in other proofs but is desirable in its own right.
**)
@@ -409,29 +327,20 @@
\ Hash {|Key(shrK A), Agent A, Agent B, Nonce NA, P|} \
\ : parts (sees lost Spy evs) --> B=B' & P=P'";
by (parts_induct_tac 1);
-be responses.induct 3;
+by (etac responses.induct 3);
by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib])));
by (step_tac (!claset addSEs partsEs) 1);
-(*RA1: creation of new Nonce. Move assertion into global context*)
-by (expand_case_tac "NA = ?y" 1);
-by (best_tac (!claset addSIs [exI]
- addSDs [Hash_imp_body]
- addSEs (new_nonces_not_seen::partsEs)
- addss (!simpset)) 1);
-by (best_tac (!claset addss (!simpset)) 1);
-(*RA2: creation of new Nonce*)
-by (expand_case_tac "NA = ?y" 1);
-by (best_tac (!claset addSIs [exI]
- addSDs [Hash_imp_body]
- addSEs (new_nonces_not_seen::partsEs)
- addss (!simpset)) 1);
-by (best_tac (!claset addss (!simpset)) 1);
+(*RA1,2: creation of new Nonce. Move assertion into global context*)
+by (ALLGOALS (expand_case_tac "NA = ?y"));
+by (REPEAT_FIRST (ares_tac [exI]));
+by (REPEAT (best_tac (!claset addSDs [Hash_imp_body]
+ addSEs sees_Spy_partsEs) 1));
val lemma = result();
goalw thy [HPair_def]
- "!!evs.[| HPair (Key(shrK A)) {|Agent A, Agent B, Nonce NA, P|} \
+ "!!evs.[| Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} \
\ : parts (sees lost Spy evs); \
-\ HPair (Key(shrK A)) {|Agent A, Agent B', Nonce NA, P'|} \
+\ Hash[Key(shrK A)] {|Agent A, Agent B', Nonce NA, P'|} \
\ : parts (sees lost Spy evs); \
\ evs : recur lost; A ~: lost |] \
\ ==> B=B' & P=P'";
@@ -445,39 +354,36 @@
***)
goal thy
- "!!evs. [| RB : responses i; evs : recur lost |] \
+ "!!evs. [| RB : responses evs; evs : recur lost |] \
\ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)";
-be responses.induct 1;
+by (etac responses.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps [resp_analz_image_newK, insert_Key_singleton]
- setloop split_tac [expand_if])));
+ (analz_image_freshK_ss addsimps [Spy_analz_shrK,
+ resp_analz_image_freshK])));
qed "shrK_in_analz_respond";
Addsimps [shrK_in_analz_respond];
goal thy
- "!!evs. [| RB : responses i; \
-\ ALL K I. (Key K : analz (Key``(newK``I) Un H)) = \
-\ (K : newK``I | Key K : analz H) |] \
+ "!!evs. [| RB : responses evs; \
+\ ALL K KK. KK <= Compl (range shrK) --> \
+\ (Key K : analz (Key``KK Un H)) = \
+\ (K : KK | Key K : analz H) |] \
\ ==> (Key K : analz (insert RB H)) --> \
-\ (Key K : parts{RB} | Key K : analz H)";
-be responses.induct 1;
+\ (Key K : parts{RB} | Key K : analz H)";
+by (etac responses.induct 1);
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps [read_instantiate [("H", "?ff``?xx")] parts_insert,
- resp_analz_image_newK_lemma,
- insert_Key_singleton, insert_Key_image,
- Un_assoc RS sym, pushKey_newK]
- setloop split_tac [expand_if])));
-(*The "Message" simpset gives the standard treatment of "image"*)
-by (simp_tac (simpset_of "Message") 1);
+ (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
+(*Simplification using two distinct treatments of "image"*)
+by (simp_tac (!simpset addsimps [parts_insert2]) 1);
by (fast_tac (!claset delrules [allE]) 1);
qed "resp_analz_insert_lemma";
bind_thm ("resp_analz_insert",
- raw_analz_image_newK RSN
- (2, resp_analz_insert_lemma) RSN(2, rev_mp));
+ raw_analz_image_freshK RSN
+ (2, resp_analz_insert_lemma) RSN(2, rev_mp));
(*The Server does not send such messages. This theorem lets us avoid
@@ -487,44 +393,51 @@
\ ==> ALL C X Y P. Says Server C {|X, Agent Server, Agent C, Y, P|} \
\ ~: set_of_list evs";
by (etac recur.induct 1);
-be (respond.induct) 5;
+by (etac (respond.induct) 5);
by (Auto_tac());
qed_spec_mp "Says_Server_not";
AddSEs [Says_Server_not RSN (2,rev_notE)];
+(*The last key returned by respond indeed appears in a certificate*)
goal thy
- "!!i. (j,PB,RB) : respond i \
-\ ==> EX A' B'. ALL A B N. \
+ "!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
+\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
+by (etac respond.elim 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "respond_certificate";
+
+
+goal thy
+ "!!K'. (PB,RB,KXY) : respond evs \
+\ ==> EX A' B'. ALL A B N. \
\ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
\ --> (A'=A & B'=B) | (A'=B & B'=A)";
-be respond.induct 1;
+by (etac respond.induct 1);
by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib])));
(*Base case*)
by (Fast_tac 1);
by (Step_tac 1);
+(*Case analysis on K=KBC*)
by (expand_case_tac "K = ?y" 1);
+by (dtac respond_Key_in_parts 1);
by (best_tac (!claset addSIs [exI]
addSEs partsEs
- addDs [Key_in_parts_respond]
- addss (!simpset)) 1);
+ addDs [Key_in_parts_respond]) 1);
+(*Case analysis on K=KAB*)
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [exI] 2));
by (ex_strip_tac 1);
-be respond.elim 1;
-by (REPEAT_FIRST (etac Pair_inject ORELSE' hyp_subst_tac));
-by (ALLGOALS (asm_full_simp_tac
- (!simpset addsimps [all_conj_distrib, ex_disj_distrib])));
-by (Fast_tac 1);
+by (dtac respond_certificate 1);
by (Fast_tac 1);
val lemma = result();
goal thy
"!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB}; \
\ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \
-\ (j,PB,RB) : respond i |] \
+\ (PB,RB,KXY) : respond evs |] \
\ ==> (A'=A & B'=B) | (A'=B & B'=A)";
-by (prove_unique_tac lemma 1); (*50 seconds??, due to the disjunctions*)
+by (prove_unique_tac lemma 1); (*50 seconds??, due to the disjunctions*)
qed "unique_session_keys";
@@ -533,47 +446,34 @@
the premises, e.g. by having A=Spy **)
goal thy
- "!!j. (j, HPair (Key(shrK A)) {|Agent A, B, NA, P|}, RA) : respond i \
-\ ==> Crypt (shrK A) {|Key (newK2 (i,j)), B, NA|} : parts {RA}";
-be respond.elim 1;
-by (ALLGOALS Asm_full_simp_tac);
-qed "newK2_respond_lemma";
-
-
-goal thy
- "!!evs. [| (j,PB,RB) : respond (length evs); evs : recur lost |] \
+ "!!evs. [| (PB,RB,KAB) : respond evs; evs : recur lost |] \
\ ==> ALL A A' N. A ~: lost & A' ~: lost --> \
\ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \
\ Key K ~: analz (insert RB (sees lost Spy evs))";
-be respond.induct 1;
+by (etac respond.induct 1);
by (forward_tac [respond_imp_responses] 2);
-by (ALLGOALS (*4 MINUTES???*)
+by (forward_tac [respond_imp_not_used] 2);
+by (ALLGOALS (*43 seconds*)
(asm_simp_tac
- (!simpset addsimps
- ([analz_image_newK, not_parts_not_analz,
- read_instantiate [("H", "?ff``?xx")] parts_insert,
- Un_assoc RS sym, resp_analz_image_newK,
- insert_Key_singleton, analz_insert_Key_newK])
- setloop split_tac [expand_if])));
-by (ALLGOALS (simp_tac (simpset_of "Message")));
-by (Fast_tac 1);
+ (analz_image_freshK_ss addsimps
+ [analz_image_freshK, not_parts_not_analz,
+ shrK_in_analz_respond,
+ read_instantiate [("H", "?ff``?xx")] parts_insert,
+ resp_analz_image_freshK, analz_insert_freshK])));
+by (ALLGOALS Simp_tac);
+by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
by (step_tac (!claset addSEs [MPair_parts]) 1);
-(** LEVEL 6 **)
-by (fast_tac (!claset addDs [resp_analz_insert, Key_in_parts_respond]
- addSEs [new_keys_not_seen RS not_parts_not_analz
- RSN(2,rev_notE)]
- addss (!simpset)) 4);
-by (fast_tac (!claset addSDs [newK2_respond_lemma]) 3);
+(** LEVEL 7 **)
+by (fast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond]
+ addDs [impOfSubs analz_subset_parts]) 4);
+by (fast_tac (!claset addSDs [respond_certificate]) 3);
by (best_tac (!claset addSEs partsEs
addDs [Key_in_parts_respond]
addss (!simpset)) 2);
-by (thin_tac "ALL x.?P(x)" 1);
-be respond.elim 1;
-by (fast_tac (!claset addss (!simpset)) 1);
-by (step_tac (!claset addss (!simpset)) 1);
-by (best_tac (!claset addSEs partsEs
- addDs [Key_in_parts_respond]
- addss (!simpset)) 1);
+by (dtac unique_session_keys 1);
+by (etac respond_certificate 1);
+by (assume_tac 1);
+by (Fast_tac 1);
qed_spec_mp "respond_Spy_not_see_encrypted_key";
@@ -586,7 +486,7 @@
by analz_Fake_tac;
by (ALLGOALS
(asm_simp_tac
- (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
+ (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
setloop split_tac [expand_if])));
(*RA4*)
by (spy_analz_tac 4);
@@ -596,13 +496,14 @@
(*RA2*)
by (spy_analz_tac 1);
(*RA3, case 2: K is an old key*)
-by (fast_tac (!claset addSDs [resp_analz_insert]
- addSEs partsEs
- addDs [Key_in_parts_respond]
- addEs [Says_imp_old_keys RS less_irrefl]) 2);
+by (best_tac (!claset addSDs [resp_analz_insert]
+ addSEs partsEs
+ addDs [Key_in_parts_respond,
+ Says_imp_sees_Spy RS parts.Inj RSN (2, parts_cut)]
+ addss (!simpset)) 2);
(*RA3, case 1: use lemma previously proved by induction*)
by (fast_tac (!claset addSEs [respond_Spy_not_see_encrypted_key RSN
- (2,rev_notE)]) 1);
+ (2,rev_notE)]) 1);
bind_thm ("Spy_not_see_encrypted_key", result() RS mp RSN (2, rev_mp));
@@ -622,34 +523,29 @@
(**** Authenticity properties for Agents ****)
(*The response never contains Hashes*)
-(*NEEDED????????????????*)
goal thy
- "!!evs. (j,PB,RB) : respond i \
+ "!!evs. (PB,RB,K) : respond evs \
\ ==> Hash {|Key (shrK B), M|} : parts (insert RB H) --> \
\ Hash {|Key (shrK B), M|} : parts H";
-be (respond_imp_responses RS responses.induct) 1;
+by (etac (respond_imp_responses RS responses.induct) 1);
by (Auto_tac());
bind_thm ("Hash_in_parts_respond", result() RSN (2, rev_mp));
-(*NEEDED????????????????*)
(*Only RA1 or RA2 can have caused such a part of a message to appear.*)
goalw thy [HPair_def]
"!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \
\ : parts (sees lost Spy evs); \
\ A ~: lost; evs : recur lost |] \
-\ ==> Says A B (HPair (Key(shrK A)) {|Agent A, Agent B, NA, P|}) \
+\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \
\ : set_of_list evs";
-be rev_mp 1;
+by (etac rev_mp 1);
by (parts_induct_tac 1);
(*RA3*)
by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
qed_spec_mp "Hash_auth_sender";
-val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
-
-
-(** These two results should subsume (for all agents) the guarantees proved
+(** These two results subsume (for all agents) the guarantees proved
separately for A and B in the Otway-Rees protocol.
**)