# HG changeset patch
# User paulson
# Date 848331277 -3600
# Node ID 63a68a3a8a768d42fbe3bb01e43d51c18d4b38d9
# Parent  b7e59795c75bc9831c5f5e5431914acae924997d
Removal of an obsolete result, and authentication of
B to A

diff -r b7e59795c75b -r 63a68a3a8a76 src/HOL/Auth/OtwayRees.ML
--- a/src/HOL/Auth/OtwayRees.ML	Mon Nov 18 16:30:06 1996 +0100
+++ b/src/HOL/Auth/OtwayRees.ML	Mon Nov 18 16:34:37 1996 +0100
@@ -493,18 +493,18 @@
 (**** Authenticity properties relating to NB ****)
 
 (*Only OR2 can have caused such a part of a message to appear.  We do not
-  know anything about X'.*)
+  know anything about X: it does NOT have to have the right form.*)
 goal thy 
  "!!evs. [| B ~: lost;  evs : otway lost |]                    \
 \        ==> Crypt {|NA, NB, Agent A, Agent B|} (shrK B)       \
 \             : parts (sees lost Spy evs) -->                  \
-\            (EX X'. Says B Server                             \
-\             {|NA, Agent A, Agent B, X',                      \
+\            (EX X. Says B Server                              \
+\             {|NA, Agent A, Agent B, X,                       \
 \               Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|}  \
 \             : set_of_list evs)";
 by (parts_induct_tac 1);
 by (auto_tac (!claset, !simpset addcongs [conj_cong]));
-qed_spec_mp "Crypt_imp_OR2";
+bind_thm ("Crypt_imp_OR2", result() RSN (2,rev_mp) RS exE);
 
 
 (** The Nonce NB uniquely identifies B's  message. **)
@@ -556,12 +556,9 @@
                       addSEs partsEs
                       addEs [Says_imp_old_nonces RS less_irrefl]
                       addss (!simpset)) 1);
-(*OR3 and OR4*)  (** LEVEL 5 **)
 (*OR4*)
-by (REPEAT (Safe_step_tac 2));
-by (rtac (Crypt_imp_OR2 RS exE) 2);
-by (REPEAT (fast_tac (!claset addEs partsEs) 2));
-(*OR3*)  (** LEVEL 8 **)
+by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 2);
+(*OR3*)
 by (step_tac (!claset delrules [disjCI, impCE]) 1);
 by (fast_tac (!claset delrules [conjI] (*stop split-up*)) 3); 
 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
@@ -598,36 +595,38 @@
 B_trust_OR3 RS Spy_not_see_encrypted_key;
 
 
-(** A session key uniquely identifies a pair of senders in the message
-    encrypted by a good agent C.  NEEDED?  INTERESTING?**)
 goal thy 
- "!!evs. evs : otway lost ==>                                           \
-\      EX A B. ALL C N.                                                 \
-\         C ~: lost -->                                                 \
-\         Crypt {|N, Key K|} (shrK C) : parts (sees lost Spy evs) -->   \
-\         C=A | C=B";
-by (Simp_tac 1);        (*Miniscoping*)
+ "!!evs. [| B ~: lost;  evs : otway lost |]                    \
+\        ==> Says Server B                                                 \
+\              {|NA, Crypt {|NA, Key K|} (shrK A),                         \
+\                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs -->      \
+\            (EX X. Says B Server {|NA, Agent A, Agent B, X,              \
+\                            Crypt {|NA, NB, Agent A, Agent B|}     \
+\                                  (shrK B)|}                       \
+\            : set_of_list evs)";
 by (etac otway.induct 1);
-by analz_Fake_tac;
-(*spy_analz_tac just does not work here: it is an entirely different proof!*)
-by (ALLGOALS 
-    (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib,
-                                      imp_conjR, parts_insert_sees,
-                                      parts_insert2])));
-by (REPEAT_FIRST (etac exE));
-(*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **)
-by (expand_case_tac "K = ?y" 4);
-by (REPEAT (ares_tac [exI] 5));
-(*...we prove this case by contradiction: the key is too new!*)
-by (fast_tac (!claset addSEs partsEs
-                      addEs [Says_imp_old_keys RS less_irrefl]
-                      addss (!simpset)) 4);
-(*Base, Fake, OR2, OR4*)
-by (REPEAT_FIRST ex_strip_tac);
-by (dtac synth.Inj 4);
-by (dtac synth.Inj 3);
-(*Now in effect there are three Fake cases*)
-by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs Fake_parts_insert]
-                                    delrules [disjCI, disjE]
-                                    addss (!simpset))));
-qed "key_identifies_senders";
+by (Auto_tac());
+bd (Says_imp_sees_Spy RS parts.Inj) 1;
+by (fast_tac (!claset addSEs [MPair_parts, Crypt_imp_OR2]) 1);
+bind_thm ("OR3_imp_OR2", result() RSN (2,rev_mp) RS exE);
+
+
+(*After getting and checking OR4, agent A can trust that B has been active.
+  We could probably prove that X has the expected form, but that is not
+  strictly necessary for authentication.*)
+goal thy 
+ "!!evs. [| Says B' A {|NA, Crypt {|NA, Key K|} (shrK A)|}         \
+\            : set_of_list evs;                                    \
+\           Says A B {|NA, Agent A, Agent B,                       \
+\                      Crypt {|NA, Agent A, Agent B|} (shrK A)|}   \
+\            : set_of_list evs;                                    \
+\           A ~: lost;  A ~= Spy;  B ~: lost;  evs : otway lost |] \
+\        ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X,     \
+\                            Crypt {|NA, NB, Agent A, Agent B|}    \
+\                                  (shrK B)|}                      \
+\            : set_of_list evs";
+by (fast_tac (!claset addSDs  [A_trust_OR4]
+	              addSEs [OR3_imp_OR2]) 1);
+qed "A_auths_B";
+
+