--- a/src/HOL/Auth/OtwayRees_AN.ML Thu Dec 19 17:02:27 1996 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Fri Dec 20 10:23:48 1996 +0100
@@ -295,11 +295,8 @@
qed_spec_mp "NA_Crypt_imp_Server_msg";
-(*Corollary: if A receives B's OR4 message and the nonce NA agrees
- then the key really did come from the Server! CANNOT prove this of the
- bad form of this protocol, even though we can prove
- Spy_not_see_encrypted_key. (We can implicitly infer freshness of
- the Server's message from its nonce NA.)*)
+(*Corollary: if A receives B's OR4 message then it originated with the Server.
+ Freshness may be inferred from nonce NA.*)
goal thy
"!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|}) \
\ : set_of_list evs; \
@@ -386,8 +383,8 @@
qed_spec_mp "NB_Crypt_imp_Server_msg";
-(*Guarantee for B: if it gets a message with matching NB then the Server
- has sent the correct message.*)
+(*Guarantee for B: if it gets a well-formed certificate then the Server
+ has sent the correct message in round 3.*)
goal thy
"!!evs. [| B ~: lost; evs : otway lost; \
\ Says S B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
--- a/src/HOL/Auth/Yahalom.ML Thu Dec 19 17:02:27 1996 +0100
+++ b/src/HOL/Auth/Yahalom.ML Fri Dec 20 10:23:48 1996 +0100
@@ -625,8 +625,7 @@
by analz_Fake_tac;
by (ALLGOALS (*22 seconds*)
(asm_simp_tac
- (!simpset addsimps ([not_parts_not_analz,
- analz_image_newK,
+ (!simpset addsimps ([not_parts_not_analz, analz_image_newK,
insert_Key_singleton, insert_Key_image]
@ pushes)
setloop split_tac [expand_if])));
@@ -644,13 +643,13 @@
addDs [unique_session_keys]
addss (!simpset)) 2);
(*YM4*)
-(** LEVEL 11 **)
+(** LEVEL 10 **)
by (rtac (impI RS allI) 1);
by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1);
by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1);
by (asm_simp_tac (!simpset addsimps [analz_image_newK]
setloop split_tac [expand_if]) 1);
-(** LEVEL 15 **)
+(** LEVEL 14 **)
by (grind_tac 1);
by (REPEAT (dtac not_analz_insert 1));
by (lost_tac "A" 1);