src/HOL/Auth/Recur.ML
 changeset 2455 9c4444bfd44e parent 2451 ce85a2aafc7a child 2481 ee461c8bc9c3
```--- a/src/HOL/Auth/Recur.ML	Fri Dec 20 10:23:48 1996 +0100
+++ b/src/HOL/Auth/Recur.ML	Fri Dec 20 10:25:26 1996 +0100
@@ -406,6 +406,8 @@

(** The Nonce NA uniquely identifies A's message.
This theorem applies to rounds RA1 and RA2!
+
+  Unicity is not used in other proofs but is desirable in its own right.
**)

goal thy
@@ -464,6 +466,7 @@
***)

(*The response never contains Hashes*)
+(*NEEDED????????????????*)
goal thy
"!!evs. (j,PB,RB) : respond i \
\        ==> Hash {|Key (shrK B), M|} : parts (insert RB H) --> \
@@ -607,9 +610,8 @@

goal thy
- "!!evs. [| A ~: lost;  A' ~: lost;  \
-\           evs : recur lost |]       \
-\        ==> Says Server B RB : set_of_list evs -->   \
+ "!!evs. [| A ~: lost;  A' ~: lost;  evs : recur lost |]            \
+\        ==> Says Server B RB : set_of_list evs -->                 \
\            Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} -->  \
\            Key K ~: analz (sees lost Spy evs)";
by (etac recur.induct 1);
@@ -638,10 +640,10 @@

goal thy
- "!!evs. [| Says Server B RB : set_of_list evs;   \
+ "!!evs. [| Says Server B RB : set_of_list evs;                 \
\           Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB};  \
-\            C ~: {A,A',Server};                                           \
-\           A ~: lost;  A' ~: lost;  evs : recur lost |]                 \
+\           C ~: {A,A',Server};                                 \
+\           A ~: lost;  A' ~: lost;  evs : recur lost |]        \
\        ==> Key K ~: analz (sees lost C evs)";
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
@@ -652,6 +654,7 @@

(**** Authenticity properties for Agents ****)

+(*NEEDED????????????????*)
(*Only RA1 or RA2 can have caused such a part of a message to appear.*)
goal thy
"!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|}         \
@@ -665,7 +668,7 @@
(*RA3*)
by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 2);
(*RA2*)
-by ((REPEAT o CHANGED)     (*Push in XA*)
+by ((REPEAT o CHANGED)     (*Push in XA--for more simplification*)
(res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 1));
by (best_tac (!claset addSEs partsEs
addDs [parts_cut]
@@ -673,6 +676,7 @@
qed_spec_mp "Hash_auth_sender";

+(*NEEDED????????????????*)
goal thy "!!i. {|Hash {|Key (shrK Server), M|}, M|} : responses i ==> R";
be setup_induction 1;
be responses.induct 1;
@@ -688,51 +692,37 @@
**)

-(*Crucial property: If the encrypted message appears, and A has used NA
-  in a run, then it originated with the Server!*)
+(*Encrypted messages can only originate with the Server.*)
goal thy
- "!!evs. [| A ~: lost;  A ~= Spy;  evs : recur lost |]                 \
-\    ==> Crypt (shrK A) {|Key K, Agent A', NA|} : parts (sees lost Spy evs) \
-\        --> Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|},  \
-\                       Agent A, Agent B, NA, P|}      \
-\             : set_of_list evs                                    \
-\         --> (EX C RC. Says Server C RC : set_of_list evs &  \
-\                       Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RC})";
+ "!!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})";
by (parts_induct_tac 1);
(*RA4*)
-by (best_tac (!claset addSEs [MPair_parts]
-	              addSDs [Hash_auth_sender]
-		      addSIs [disjI2]) 4);
-(*RA1: it cannot be a new Nonce, contradiction.*)
-by (fast_tac (!claset delrules [impCE]
-	              addSEs [nonce_not_seen_now, MPair_parts]
-                      addDs  [parts.Body]) 1);
+by (Fast_tac 4);
+(*RA3*)
+by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 3
+    THEN Fast_tac 3);
+(*RA1*)
+by (Fast_tac 1);
(*RA2: it cannot be a new Nonce, contradiction.*)
-by ((REPEAT o CHANGED)     (*Push in XA*)
+by ((REPEAT o CHANGED)     (*Push in XA--for more simplification*)
(res_inst_tac [("x1","XA")] (insert_commute RS ssubst) 1));
by (deepen_tac (!claset delrules [impCE]
addSIs [disjI2]
-	              addSEs [MPair_parts]
+                      addSEs [MPair_parts]
addDs  [parts_cut, parts.Body]
addss  (!simpset)) 0 1);
-(*RA3*)  (** LEVEL 5 **)
-by (REPEAT (safe_step_tac (!claset addSEs [responses_no_Hash_Server]
-	                           delrules [impCE]) 1));
-by (full_simp_tac (!simpset addsimps [parts_insert_sees]) 1);
-by (Fast_tac 1);
qed_spec_mp "Crypt_imp_Server_msg";

-(*Corollary: if A receives B's message and the nonce NA agrees
-  then the key really did come from the Server!*)
+(*Corollary: if A receives B's message then the key came from the Server*)
goal thy
"!!evs. [| Says B' A RA : set_of_list evs;                        \
-\           Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RA};    \
-\           Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|},  \
-\                       Agent A, Agent B, NA, P|}   \
-\            : set_of_list evs;                                    \
+\           Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RA};   \
\           A ~: lost;  A ~= Spy;  evs : recur lost |]             \
-\        ==> EX C RC. Says Server C RC : set_of_list evs &  \
+\        ==> EX C RC. Says Server C RC : set_of_list evs &         \
\                       Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RC}";
by (best_tac (!claset addSIs [Crypt_imp_Server_msg]
addDs  [Says_imp_sees_Spy RS parts.Inj RSN (2,parts_cut)]
@@ -740,14 +730,11 @@
qed "Agent_trust";

-(*Overall guarantee: if A receives B's message and the nonce NA agrees
-  then the only other agent who knows the key is B.*)
+(*Overall guarantee: if A receives a certificant mentioning A'
+  then the only other agent who knows the key is A'.*)
goal thy
"!!evs. [| Says B' A RA : set_of_list evs;                           \
\           Crypt (shrK A) {|Key K, Agent A', NA|} : parts {RA};      \
-\           Says A B {|Hash{|Key(shrK A), Agent A, Agent B, NA, P|},  \
-\                      Agent A, Agent B, NA, P|}                      \
-\            : set_of_list evs;                                       \
\           C ~: {A,A',Server};                                       \
\           A ~: lost;  A' ~: lost;  A ~= Spy;  evs : recur lost |]   \
\        ==> Key K ~: analz (sees lost C evs)";```