--- a/src/HOL/Auth/Event.ML Wed Aug 21 11:43:37 1996 +0200
+++ b/src/HOL/Auth/Event.ML Wed Aug 21 13:22:23 1996 +0200
@@ -395,11 +395,10 @@
addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
addss (!simpset)))
[2,1];
-(*NS4*)
-by (step_tac (!claset addSDs [Suc_leD, newK_invKey]) 1);
-by (deepen_tac (!claset addIs [impOfSubs keysFor_mono]) 0 2);
-by (fast_tac (!claset addDs [Says_imp_old_keys]
- addss (!simpset addsimps [le_def])) 1);
+(*NS4 and NS5: nonce exchange*)
+by (ALLGOALS (deepen_tac (!claset addSDs [newK_invKey, Says_imp_old_keys]
+ addIs [less_SucI, impOfSubs keysFor_mono]
+ addss (!simpset addsimps [le_def])) 0));
val lemma = result();
goal thy
@@ -561,7 +560,7 @@
****)
-(*Not useful in this form, but it says that session keys are not used
+(*NOT useful in this form, but it says that session keys are not used
to encrypt messages containing other keys, in the actual protocol.
We require that agents should behave like this subsequently also.*)
goal thy
@@ -576,7 +575,8 @@
addDs [impOfSubs analz_subset_parts,
impOfSubs parts_insert_subset_Un]
addss (!simpset)) 1);
-by (fast_tac (!claset addss (!simpset)) 1);
+(*NS4 and NS5*)
+by (ALLGOALS (fast_tac (!claset addss (!simpset))));
result();
--- a/src/HOL/Auth/Event.thy Wed Aug 21 11:43:37 1996 +0200
+++ b/src/HOL/Auth/Event.thy Wed Aug 21 13:22:23 1996 +0200
@@ -82,9 +82,6 @@
isSym_newK "isSymKey (newK evs)"
-(*NS3 DOESN'T ALLOW INTERLEAVING -- that is, it only responds to the
- MOST RECENT message.*)
-
(*Needham-Schroeder Shared-Key protocol (from BAN paper, page 247)*)
consts traces :: "event list set"
inductive traces
@@ -105,7 +102,8 @@
(*Server's response to Alice's message.
!! It may respond more than once to A's request !!
- We can't trust the sender field, hence the A' in it.*)
+ Server doesn't know who the true sender is, hence the A' in
+ the sender field.*)
NS2 "[| evs: traces; A ~= B; A ~= Server;
(Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
|] ==> (Says Server A
@@ -123,8 +121,18 @@
(Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
|] ==> (Says A B X) # evs : traces"
+ (*Bob's nonce exchange. He does not know who the message came
+ from, but responds to A because she is mentioned inside.*)
NS4 "[| evs: traces; A ~= B;
(Says A' B (Crypt {|Key K, Agent A|} (serverKey B)))
: set_of_list evs
|] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : traces"
+
+ (*Alice responds with (Suc N), if she has seen the key before.*)
+ NS5 "[| evs: traces; A ~= B;
+ (Says B' A (Crypt (Nonce N) K)) : set_of_list evs;
+ (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)))
+ : set_of_list evs
+ |] ==> (Says A B (Crypt (Nonce (Suc N)) K)) # evs : traces"
+
end