Addition of message NS5
authorpaulson
Wed Aug 21 13:22:23 1996 +0200 (1996-08-21)
changeset 19338b24773de6db
parent 1932 cc9f1ba8f29a
child 1934 58573e7041b4
Addition of message NS5
src/HOL/Auth/Event.ML
src/HOL/Auth/Event.thy
     1.1 --- a/src/HOL/Auth/Event.ML	Wed Aug 21 11:43:37 1996 +0200
     1.2 +++ b/src/HOL/Auth/Event.ML	Wed Aug 21 13:22:23 1996 +0200
     1.3 @@ -395,11 +395,10 @@
     1.4  	      addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
     1.5  	      addss (!simpset)))
     1.6      [2,1];
     1.7 -(*NS4*)
     1.8 -by (step_tac (!claset addSDs [Suc_leD, newK_invKey]) 1);
     1.9 -by (deepen_tac (!claset addIs [impOfSubs keysFor_mono]) 0 2);
    1.10 -by (fast_tac (!claset addDs [Says_imp_old_keys]
    1.11 -	              addss (!simpset addsimps [le_def])) 1);
    1.12 +(*NS4 and NS5: nonce exchange*)
    1.13 +by (ALLGOALS (deepen_tac (!claset addSDs [newK_invKey, Says_imp_old_keys]
    1.14 +	                          addIs  [less_SucI, impOfSubs keysFor_mono]
    1.15 +		                  addss (!simpset addsimps [le_def])) 0));
    1.16  val lemma = result();
    1.17  
    1.18  goal thy 
    1.19 @@ -561,7 +560,7 @@
    1.20  ****)
    1.21  
    1.22  
    1.23 -(*Not useful in this form, but it says that session keys are not used
    1.24 +(*NOT useful in this form, but it says that session keys are not used
    1.25    to encrypt messages containing other keys, in the actual protocol.
    1.26    We require that agents should behave like this subsequently also.*)
    1.27  goal thy 
    1.28 @@ -576,7 +575,8 @@
    1.29  		      addDs [impOfSubs analz_subset_parts,
    1.30                               impOfSubs parts_insert_subset_Un]
    1.31                        addss (!simpset)) 1);
    1.32 -by (fast_tac (!claset addss (!simpset)) 1);
    1.33 +(*NS4 and NS5*)
    1.34 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.35  result();
    1.36  
    1.37  
     2.1 --- a/src/HOL/Auth/Event.thy	Wed Aug 21 11:43:37 1996 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Wed Aug 21 13:22:23 1996 +0200
     2.3 @@ -82,9 +82,6 @@
     2.4    isSym_newK "isSymKey (newK evs)"
     2.5  
     2.6  
     2.7 -(*NS3 DOESN'T ALLOW INTERLEAVING -- that is, it only responds to the
     2.8 -  MOST RECENT message.*)
     2.9 -
    2.10  (*Needham-Schroeder Shared-Key protocol (from BAN paper, page 247)*)
    2.11  consts  traces   :: "event list set"
    2.12  inductive traces
    2.13 @@ -105,7 +102,8 @@
    2.14  
    2.15           (*Server's response to Alice's message.
    2.16             !! It may respond more than once to A's request !!
    2.17 -	   We can't trust the sender field, hence the A' in it.*)
    2.18 +	   Server doesn't know who the true sender is, hence the A' in
    2.19 +               the sender field.*)
    2.20      NS2  "[| evs: traces;  A ~= B;  A ~= Server;
    2.21               (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    2.22            |] ==> (Says Server A 
    2.23 @@ -123,8 +121,18 @@
    2.24               (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    2.25            |] ==> (Says A B X) # evs : traces"
    2.26  
    2.27 +         (*Bob's nonce exchange.  He does not know who the message came
    2.28 +           from, but responds to A because she is mentioned inside.*)
    2.29      NS4  "[| evs: traces;  A ~= B;  
    2.30               (Says A' B (Crypt {|Key K, Agent A|} (serverKey B))) 
    2.31                 : set_of_list evs
    2.32            |] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : traces"
    2.33 +
    2.34 +         (*Alice responds with (Suc N), if she has seen the key before.*)
    2.35 +    NS5  "[| evs: traces;  A ~= B;  
    2.36 +             (Says B' A (Crypt (Nonce N) K)) : set_of_list evs;
    2.37 +             (Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
    2.38 +               : set_of_list evs
    2.39 +          |] ==> (Says A B (Crypt (Nonce (Suc N)) K)) # evs : traces"
    2.40 +
    2.41  end