# HG changeset patch
# User paulson
# Date 898523459 -7200
# Node ID 99abb086212ef6c3238cae3f35ef9760650545d6
# Parent  77bd19f782e6526c07f332dbe8ca2a1c234db08a
comments and minor tidying

diff -r 77bd19f782e6 -r 99abb086212e src/HOL/Auth/Yahalom.ML
--- a/src/HOL/Auth/Yahalom.ML	Mon Jun 22 15:49:29 1998 +0200
+++ b/src/HOL/Auth/Yahalom.ML	Mon Jun 22 15:50:59 1998 +0200
@@ -269,8 +269,8 @@
 (*B knows, by the first part of A's message, that the Server distributed 
   the key for A and B.  But this part says nothing about nonces.*)
 goal thy 
- "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs);   \
-\           B ~: bad;  evs : yahalom |]                                \
+ "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs);      \
+\           B ~: bad;  evs : yahalom |]                                 \
 \        ==> EX NA NB. Says Server A                                    \
 \                        {|Crypt (shrK A) {|Agent B, Key K,             \
 \                                           Nonce NA, Nonce NB|},       \
@@ -285,15 +285,16 @@
 
 (*B knows, by the second part of A's message, that the Server distributed 
   the key quoting nonce NB.  This part says nothing about agent names. 
-  Secrecy of NB is crucial.*)
+  Secrecy of NB is crucial.  Note that  Nonce NB  ~: analz (spies evs)  must
+  be the FIRST antecedent of the induction formula.*)
 goal thy 
- "!!evs. evs : yahalom                                             \
+ "!!evs. evs : yahalom                                          \
 \        ==> Nonce NB ~: analz (spies evs) -->                  \
 \            Crypt K (Nonce NB) : parts (spies evs) -->         \
-\            (EX A B NA. Says Server A                             \
-\                        {|Crypt (shrK A) {|Agent B, Key K,        \
-\                                  Nonce NA, Nonce NB|},           \
-\                          Crypt (shrK B) {|Agent A, Key K|}|}     \
+\            (EX A B NA. Says Server A                          \
+\                        {|Crypt (shrK A) {|Agent B, Key K,     \
+\                                  Nonce NA, Nonce NB|},        \
+\                          Crypt (shrK B) {|Agent A, Key K|}|}  \
 \                       : set evs)";
 by (parts_induct_tac 1);
 by (ALLGOALS Clarify_tac);
@@ -349,7 +350,7 @@
  "!!evs. [| Says Server A                                                \
 \                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
 \             : set evs;                                                 \
-\           NB ~= NB';  evs : yahalom |]                            \
+\           NB ~= NB';  evs : yahalom |]                                 \
 \        ==> ~ KeyWithNonce K NB evs";
 by (blast_tac (claset() addDs [unique_session_keys]) 1);
 qed "Says_Server_KeyWithNonce";
@@ -369,9 +370,9 @@
 val Nonce_secrecy_lemma = result();
 
 goal thy 
- "!!evs. evs : yahalom ==>                                         \
-\        (ALL KK. KK <= Compl (range shrK) -->                          \
-\             (ALL K: KK. ~ KeyWithNonce K NB evs)   -->                \
+ "!!evs. evs : yahalom ==>                                      \
+\        (ALL KK. KK <= Compl (range shrK) -->                  \
+\             (ALL K: KK. ~ KeyWithNonce K NB evs)   -->        \
 \             (Nonce NB : analz (Key``KK Un (spies evs))) =     \
 \             (Nonce NB : analz (spies evs)))";
 by (etac yahalom.induct 1);
@@ -404,11 +405,11 @@
   was distributed with that key.  The more general form above is required
   for the induction to carry through.*)
 goal thy 
- "!!evs. [| Says Server A                                                 \
-\            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}    \
-\           : set evs;                                                    \
-\           NB ~= NB';  KAB ~: range shrK;  evs : yahalom |]         \
-\        ==> (Nonce NB : analz (insert (Key KAB) (spies evs))) =  \
+ "!!evs. [| Says Server A                                               \
+\            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}  \
+\           : set evs;                                                  \
+\           NB ~= NB';  KAB ~: range shrK;  evs : yahalom |]            \
+\        ==> (Nonce NB : analz (insert (Key KAB) (spies evs))) =        \
 \            (Nonce NB : analz (spies evs))";
 by (asm_simp_tac (analz_image_freshK_ss addsimps 
 		  [Nonce_secrecy, Says_Server_KeyWithNonce]) 1);
@@ -418,8 +419,8 @@
 (*** The Nonce NB uniquely identifies B's message. ***)
 
 goal thy 
- "!!evs. evs : yahalom ==>                                            \
-\   EX NA' A' B'. ALL NA A B.                                              \
+ "!!evs. evs : yahalom ==>                                         \
+\   EX NA' A' B'. ALL NA A B.                                      \
 \      Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(spies evs) \
 \      --> B ~: bad --> NA = NA' & A = A' & B = B'";
 by (parts_induct_tac 1);
@@ -434,7 +435,7 @@
 val lemma = result();
 
 goal thy 
- "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs); \
+ "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs);    \
 \          Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (spies evs); \
 \          evs : yahalom;  B ~: bad;  B' ~: bad |]  \
 \        ==> NA' = NA & A' = A & B' = B";
@@ -446,10 +447,10 @@
   not_bad_tac to remove the assumption B' ~: bad.*)
 goal thy 
  "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}    \
-\            : set evs;          B ~: bad;                               \
+\            : set evs;          B ~: bad;                                \
 \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
 \            : set evs;                                                   \
-\          nb ~: analz (spies evs);  evs : yahalom |]        \
+\          nb ~: analz (spies evs);  evs : yahalom |]                     \
 \        ==> NA' = NA & A' = A & B' = B";
 by (not_bad_tac "B'" 1);
 by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj]
@@ -461,10 +462,10 @@
 (** A nonce value is never used both as NA and as NB **)
 
 goal thy 
- "!!evs. [| B ~: bad;  evs : yahalom  |]            \
+ "!!evs. [| B ~: bad;  evs : yahalom  |]          \
 \ ==> Nonce NB ~: analz (spies evs) -->           \
 \     Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \
-\     Crypt (shrK B)  {|Agent A, Nonce NA, Nonce NB|} ~: parts(spies evs)";
+\     Crypt (shrK B)  {|Agent A, na, Nonce NB|} ~: parts(spies evs)";
 by (parts_induct_tac 1);
 by (Fake_parts_insert_tac 1);
 by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj]
@@ -472,6 +473,9 @@
                         addSEs partsEs) 1);
 bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE));
 
+(*more readable version cited in Yahalom paper*)
+standard (result() RS mp RSN (2,rev_mp));
+
 (*The Server sends YM3 only in response to YM2.*)
 goal thy 
  "!!evs. [| Says Server A                                                \