# HG changeset patch
# User paulson
# Date 867319085 -7200
# Node ID 315694e22856a4d7aba897d4df3e139555ba0365
# Parent  8ea594a5ae53fef4b4336b8db6e609872c7d3fb8
Trivial changes in connection with the Yahalom paper.
Changed the order of the premises in no_nonce_YM1_YM2.

Installed B_trusts_YM4_newK using bind_thm.

Improved some comments.

diff -r 8ea594a5ae53 -r 315694e22856 src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Thu Jun 26 11:15:55 1997 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Thu Jun 26 11:58:05 1997 +0200
@@ -358,7 +358,7 @@
 (*A's certificate guarantees the existence of the Server message*)
 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS
 			      A_trusts_YM3]) 1);
-val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp);
+bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp));
 
 
 (**** Towards proving secrecy of Nonce NB ****)
@@ -382,6 +382,8 @@
 qed "KeyWithNonce_Says";
 Addsimps [KeyWithNonce_Says];
 
+(*A fresh key cannot be associated with any nonce 
+  (with respect to a given trace). *)
 goalw thy [KeyWithNonce_def]
  "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
 by (blast_tac (!claset addSEs sees_Spy_partsEs) 1);
@@ -510,18 +512,20 @@
 (** A nonce value is never used both as NA and as NB **)
 
 goal thy 
- "!!evs. [| B ~: lost;  evs : yahalom lost  |]               \
-\ ==> Nonce NB ~: analz (sees lost Spy evs) -->              \
-\     Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}: parts(sees lost Spy evs)\
-\ --> Crypt (shrK B') {|Agent A', Nonce NB, NB'|} ~: parts(sees lost Spy evs)";
+ "!!evs. [| B ~: lost;  evs : yahalom lost  |]       \
+\ ==> Nonce NB ~: analz (sees lost Spy evs) -->      \
+\     Crypt (shrK B') {|Agent A', Nonce NB, NB'|}    \
+\       : parts(sees lost Spy evs)                   \
+\ --> Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|} \
+\       ~: parts(sees lost Spy evs)";
 by analz_mono_parts_induct_tac;
 by (Fake_parts_insert_tac 1);
 by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj]
                        addSIs [parts_insertI]
                        addSEs partsEs) 1);
-bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2, rev_mp) RS notE);
+bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
 
-(*YM3 can only be triggered by YM2*)
+(*The Server sends YM3 only in response to YM2.*)
 goal thy 
  "!!evs. [| Says Server A                                           \
 \            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set_of_list evs; \
@@ -536,7 +540,7 @@
 qed "Says_Server_imp_YM2";
 
 
-(*Basic theorem for B: Nonce NB remains secure from the Spy.
+(*A vital theorem for B, that nonce NB remains secure from the Spy.
   Unusually, the Fake case requires Spy:lost.*)
 goal thy 
  "!!evs. [| A ~: lost;  B ~: lost;  Spy: lost;  evs : yahalom lost |]  \
@@ -594,11 +598,11 @@
 bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp));
 
 
-(*What can B deduce from receipt of YM4?  Note how the two components of
-  the message contribute to a single conclusion about the Server's message.
-  Note that the "Says A Spy" assumption must quantify over 
-  ALL POSSIBLE keys instead of our particular K.  If this run is broken and
-  the spy has a certificate for an old key, B has no means of telling.*)
+(*B's session key guarantee from YM4.  The two certificates contribute to a
+  single conclusion about the Server's message.  Note that the "Says A Spy"
+  assumption must quantify over ALL POSSIBLE keys instead of our particular K.
+  If this run is broken and the spy substitutes a certificate containing an
+  old key, B has no means of telling.*)
 goal thy 
  "!!evs. [| Says B Server                                                   \
 \             {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|}   \