# HG changeset patch
# User paulson
# Date 844184694 -7200
# Node ID 067bf19a71b7d464ca1788b947f61e08285ff6e4
# Parent  1b3343fa1278663236c23f5533e5a195dfd93542
Simplified main theorem by abstracting out newK

diff -r 1b3343fa1278 -r 067bf19a71b7 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Tue Oct 01 17:07:41 1996 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Tue Oct 01 17:44:54 1996 +0200
@@ -39,27 +39,9 @@
                               :: yahalom.intrs))));
 qed "yahalom_mono";
 
-(*The Spy can see more than anybody else, except for their initial state*)
-goal thy 
- "!!evs. evs : yahalom lost ==> \
-\     sees lost A evs <= initState lost A Un sees lost Spy evs";
-by (etac yahalom.induct 1);
-by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
-                                addss (!simpset))));
-qed "sees_agent_subset_sees_Spy";
-
-(*The Spy can see more than anybody else who's lost their key!*)
-goal thy 
- "!!evs. evs : yahalom lost ==> \
-\        A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
-by (etac yahalom.induct 1);
-by (agent.induct_tac "A" 1);
-by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
-qed_spec_mp "sees_lost_agent_subset_sees_Spy";
-
 
 (*Nobody sends themselves messages*)
-goal thy "!!evs. evs : yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
+goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs";
 by (etac yahalom.induct 1);
 by (Auto_tac());
 qed_spec_mp "not_Says_to_self";
@@ -290,12 +272,13 @@
     As with Otway-Rees, proof does not need uniqueness of session keys. **)
 
 goal thy 
- "!!evs. [| A ~: lost;  B ~: lost;  evs : yahalom lost;  evt : yahalom lost |]        \
-\        ==> Says Server A                                                \
-\              {|Crypt {|Agent B, Key(newK evt), NA, NB|} (shrK A),       \
-\                Crypt {|Agent A, Key(newK evt)|} (shrK B)|}              \
+ "!!evs. [| A ~: lost;  B ~: lost;                                \
+\           evs : yahalom lost;  evt : yahalom lost |]            \
+\        ==> Says Server A                                        \
+\              {|Crypt {|Agent B, Key K, NA, NB|} (shrK A),       \
+\                Crypt {|Agent A, Key K|} (shrK B)|}              \
 \             : set_of_list evs -->    \
-\            Key(newK evt) ~: analz (sees lost Spy evs)";
+\            Key K ~: analz (sees lost Spy evs)";
 by (etac yahalom.induct 1);
 by (dtac YM4_analz_sees_Spy 6);
 by (ALLGOALS
@@ -344,7 +327,7 @@
 
 goal thy 
  "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees lost Spy evs); \
-\           B ~: lost;  evs : yahalom lost |]                                 \
+\           B ~: lost;  evs : yahalom lost |]                           \
 \        ==> EX NA NB. Says Server A                                    \
 \                        {|Crypt {|Agent B, Key K,                      \
 \                                  Nonce NA, Nonce NB|} (shrK A),       \
@@ -366,13 +349,13 @@
 qed "Crypt_imp_Server_msg";
 
 
-(*What can B deduce from receipt of YM4?  
-  NOT THAT THE NONCES AGREE (in this version).  But what does the Nonce
-        give us??*)
+(*What can B deduce from receipt of YM4?  NOT THAT THE NONCES AGREE.  Cf the
+  BAN paper page 259.  "If A chose to replay an old key to B in message 4,
+  B could not detect the fraud." *)
 goal thy 
  "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
 \                       Crypt (Nonce NB) K|} : set_of_list evs;         \
-\           B ~: lost;  evs : yahalom lost |]                                 \
+\           B ~: lost;  evs : yahalom lost |]                           \
 \        ==> EX NA NB. Says Server A                                    \
 \                     {|Crypt {|Agent B, Key K,                         \
 \                               Nonce NA, Nonce NB|} (shrK A),          \
@@ -386,12 +369,10 @@
                                         Crypt_imp_Server_msg])));
 qed "YM4_imp_Says_Server_A";
 
-
-
 goal thy 
  "!!evs. [| Says A' B {|Crypt {|Agent A, Key K|} (shrK B),              \
 \                       Crypt (Nonce NB) K|} : set_of_list evs;         \
-\           A ~: lost;  B ~: lost;  evs : yahalom lost |]                      \
+\           A ~: lost;  B ~: lost;  evs : yahalom lost |]               \
 \        ==> Key K ~: analz (sees lost Spy evs)";
 by (fast_tac (!claset addSDs [YM4_imp_Says_Server_A,
                               Spy_not_see_encrypted_key]) 1);