# HG changeset patch
# User paulson
# Date 854039660 -3600
# Node ID 8d8344bcf98a1aa5488adf183aa5ddf5a057cf3a
# Parent  0c723635b9e6534dea6ae057ad8535b912299aaf
Re-ordering of certificates so that session keys appear in decreasing order

diff -r 0c723635b9e6 -r 8d8344bcf98a src/HOL/Auth/Recur.ML
--- a/src/HOL/Auth/Recur.ML	Thu Jan 23 18:13:07 1997 +0100
+++ b/src/HOL/Auth/Recur.ML	Thu Jan 23 18:14:20 1997 +0100
@@ -24,7 +24,7 @@
  "!!A. A ~= Server   \
 \ ==> EX K NA. EX evs: recur lost.          \
 \     Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
-\                       Agent Server|}      \
+\                     Agent Server|}      \
 \         : set_of_list evs";
 by (REPEAT (resolve_tac [exI,bexI] 1));
 by (rtac (recur.Nil RS recur.RA1 RS 
@@ -36,9 +36,9 @@
 (*Case two: Alice, Bob and the server*)
 goal thy
  "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
-\ ==> EX K. EX NA. EX evs: recur lost.          \
+\ ==> EX K. EX NA. EX evs: recur lost.            \
 \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
-\                       Agent Server|}                          \
+\                  Agent Server|}                               \
 \         : set_of_list evs";
 by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
 by (REPEAT (eresolve_tac [exE, conjE] 1));
@@ -56,9 +56,9 @@
   TOO SLOW to run every time!
 goal thy
  "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |]   \
-\ ==> EX K. EX NA. EX evs: recur lost.          \
+\ ==> EX K. EX NA. EX evs: recur lost.                          \
 \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
-\                       Agent Server|}                          \
+\                  Agent Server|}                               \
 \         : set_of_list evs";
 by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
 by (REPEAT (eresolve_tac [exE, conjE] 1));
@@ -126,7 +126,7 @@
 
 val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
 
-goal thy "!!evs. Says C' B {|X, X', RA|} : set_of_list evs \
+goal thy "!!evs. Says C' B {|Crypt K 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";
@@ -172,12 +172,13 @@
  "!!evs. evs : recur lost \
 \        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
 by (parts_induct_tac 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [parts_insert_sees])));
+(*RA3*)
+by (fast_tac (!claset addDs [Key_in_parts_respond]
+                      addss (!simpset addsimps [parts_insert_sees])) 2);
 (*RA2*)
 by (best_tac (!claset addSEs partsEs addSDs [parts_cut]
                       addss (!simpset)) 1);
-(*RA3*)
-by (fast_tac (!claset addDs [Key_in_parts_respond]
-                      addss (!simpset addsimps [parts_insert_sees])) 1);
 qed "Spy_see_shrK";
 Addsimps [Spy_see_shrK];
 
@@ -299,9 +300,10 @@
 
 
 (*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)";
+goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (sees lost Spy evs);  \
+\                   evs : recur lost;  A ~: lost |]                       \
+\                ==> X : parts (sees lost Spy evs)";
+by (etac rev_mp 1);
 by (etac recur.induct 1);
 by parts_Fake_tac;
 (*RA3 requires a further induction*)
@@ -313,7 +315,7 @@
                       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));
+qed "Hash_imp_body";
 
 
 (** The Nonce NA uniquely identifies A's message. 
@@ -419,14 +421,12 @@
 (*Base case*)
 by (Fast_tac 1);
 by (Step_tac 1);
-(*Case analysis on K=KBC*)
-by (expand_case_tac "K = ?y" 1);
+by (expand_case_tac "K = KBC" 1);
 by (dtac respond_Key_in_parts 1);
 by (best_tac (!claset addSIs [exI]
                       addSEs partsEs
                       addDs [Key_in_parts_respond]) 1);
-(*Case analysis on K=KAB*)
-by (expand_case_tac "K = ?y" 1);
+by (expand_case_tac "K = KAB" 1);
 by (REPEAT (ares_tac [exI] 2));
 by (ex_strip_tac 1);
 by (dtac respond_certificate 1);
@@ -476,10 +476,11 @@
 
 
 goal thy
- "!!evs. [| A ~: lost;  A' ~: lost;  evs : recur lost |]   \
-\        ==> Crypt (shrK A) {|Key K, Agent A', N|}         \
-\              : parts (sees lost Spy evs) -->             \
-\            Key K ~: analz (sees lost Spy evs)";
+ "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|}          \
+\              : parts (sees lost Spy evs);                \
+\           A ~: lost;  A' ~: lost;  evs : recur lost |]   \
+\        ==> Key K ~: analz (sees lost Spy evs)";
+by (etac rev_mp 1);
 by (etac recur.induct 1);
 by analz_Fake_tac;
 by (ALLGOALS
@@ -504,7 +505,7 @@
 (*RA3, case 1: use lemma previously proved by induction*)
 by (fast_tac (!claset addSEs [respond_Spy_not_see_session_key RSN
                               (2,rev_notE)]) 1);
-bind_thm ("Spy_not_see_session_key", result() RSN (2, rev_mp));
+qed "Spy_not_see_session_key";
 
 
 goal thy 
@@ -526,12 +527,13 @@
 
 (*The response never contains Hashes*)
 goal thy
- "!!evs. (PB,RB,K) : respond evs \
-\        ==> Hash {|Key (shrK B), M|} : parts (insert RB H) --> \
-\            Hash {|Key (shrK B), M|} : parts H";
+ "!!evs. [| Hash {|Key (shrK B), M|} : parts (insert RB H); \
+\           (PB,RB,K) : respond evs |]                      \
+\        ==> Hash {|Key (shrK B), M|} : parts H";
+by (etac rev_mp 1);
 by (etac (respond_imp_responses RS responses.induct) 1);
 by (Auto_tac());
-bind_thm ("Hash_in_parts_respond", result() RSN (2, rev_mp));
+qed "Hash_in_parts_respond";
 
 (*Only RA1 or RA2 can have caused such a part of a message to appear.
   This result is of no use to B, who cannot verify the Hash.  Moreover,
@@ -556,10 +558,11 @@
 
 (*Certificates can only originate with the Server.*)
 goal thy 
- "!!evs. [| A ~: lost;  A ~= Spy;  evs : recur lost |]       \
-\    ==> Crypt (shrK A) Y : parts (sees lost Spy evs)        \
-\        --> (EX C RC. Says Server C RC : set_of_list evs &  \
-\                      Crypt (shrK A) Y : parts {RC})";
+ "!!evs. [| Crypt (shrK A) Y : parts (sees lost Spy evs);    \
+\           A ~: lost;  A ~= Spy;  evs : recur lost |]       \
+\        ==> EX C RC. Says Server C RC : set_of_list evs &   \
+\                     Crypt (shrK A) Y : parts {RC}";
+by (etac rev_mp 1);
 by (parts_induct_tac 1);
 (*RA4*)
 by (Fast_tac 4);
@@ -574,4 +577,4 @@
                       addSEs [MPair_parts]
                       addDs  [parts.Body]
                       addss  (!simpset)) 0 1);
-bind_thm ("Cert_imp_Server_msg", result() RSN (2, rev_mp));
+qed "Cert_imp_Server_msg";
diff -r 0c723635b9e6 -r 8d8344bcf98a src/HOL/Auth/Recur.thy
--- a/src/HOL/Auth/Recur.thy	Thu Jan 23 18:13:07 1997 +0100
+++ b/src/HOL/Auth/Recur.thy	Thu Jan 23 18:14:20 1997 +0100
@@ -27,8 +27,8 @@
              PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|};
              B ~= Server |]
           ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, 
-               {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
-                 Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
+               {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
+                 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
                  RA|},
                KBC)
               : respond evs"
@@ -80,8 +80,7 @@
           ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
               # evs : recur lost"
 
-         (*The Server receives and decodes Bob's message.  Then he generates
-           a new session key and a response.*)
+         (*The Server receives Bob's message and prepares a response.*)
     RA3  "[| evs: recur lost;  B ~= Server;
              Says B' Server PB : set_of_list evs;
              (PB,RB,K) : respond evs |]
@@ -90,11 +89,12 @@
          (*Bob receives the returned message and compares the Nonces with
            those in the message he previously sent the Server.*)
     RA4  "[| evs: recur lost;  A ~= B;  
-             Says C' B {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
-                         Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, RA|}
-               : set_of_list evs;
              Says B  C {|XH, Agent B, Agent C, Nonce NB, 
                          XA, Agent A, Agent B, Nonce NA, P|} 
+               : set_of_list evs;
+             Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
+                         Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
+                         RA|}
                : set_of_list evs |]
           ==> Says B A RA # evs : recur lost"