Working version of NS, messages 1-4!
authorpaulson
Tue Aug 20 18:53:17 1996 +0200 (1996-08-20)
changeset 1930cdf9bcd53749
parent 1929 f0839bab4b00
child 1931 c77409a88b75
Working version of NS, messages 1-4!
src/HOL/Auth/Event.ML
src/HOL/Auth/Event.thy
     1.1 --- a/src/HOL/Auth/Event.ML	Tue Aug 20 17:46:24 1996 +0200
     1.2 +++ b/src/HOL/Auth/Event.ML	Tue Aug 20 18:53:17 1996 +0200
     1.3 @@ -384,14 +384,22 @@
     1.4  be traces.induct 1;
     1.5  bd NS3_msg_in_parts_sees_Enemy 5;
     1.6  by (ALLGOALS Asm_simp_tac);
     1.7 -by (ALLGOALS
     1.8 -    (best_tac 
     1.9 +(*NS1 and NS2*)
    1.10 +map (by o fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [3,2];
    1.11 +(*Fake and NS3*)
    1.12 +map (by o best_tac
    1.13       (!claset addSDs [newK_invKey]
    1.14  	      addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
    1.15  		     impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    1.16  		     Suc_leD]
    1.17  	      addEs [new_keys_not_seen RS not_parts_not_analz RSN (2,rev_notE)]
    1.18 -	      addss (!simpset))));
    1.19 +	      addss (!simpset)))
    1.20 +    [2,1];
    1.21 +(*NS4*)
    1.22 +by (step_tac (!claset addSDs [Suc_leD, newK_invKey]) 1);
    1.23 +by (deepen_tac (!claset addIs [impOfSubs keysFor_mono]) 0 2);
    1.24 +by (fast_tac (!claset addDs [Says_imp_old_keys]
    1.25 +	              addss (!simpset addsimps [le_def])) 1);
    1.26  val lemma = result();
    1.27  
    1.28  goal thy 
    1.29 @@ -526,6 +534,7 @@
    1.30  by (auto_tac (!claset addIs [Says_imp_old_keys], !simpset));
    1.31  qed "Says_S_message_form";
    1.32  
    1.33 +(*Currently unused.  Needed only to reason about the VERY LAST message.*)
    1.34  goal thy 
    1.35   "!!evs. [| evs = Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}   \
    1.36  \                           (serverKey A)) # evs';                  \
    1.37 @@ -540,7 +549,6 @@
    1.38  
    1.39  
    1.40  
    1.41 -
    1.42  (****
    1.43   The following is to prove theorems of the form
    1.44  
    1.45 @@ -568,6 +576,7 @@
    1.46  		      addDs [impOfSubs analz_subset_parts,
    1.47                               impOfSubs parts_insert_subset_Un]
    1.48                        addss (!simpset)) 1);
    1.49 +by (fast_tac (!claset addss (!simpset)) 1);
    1.50  result();
    1.51  
    1.52  
     2.1 --- a/src/HOL/Auth/Event.thy	Tue Aug 20 17:46:24 1996 +0200
     2.2 +++ b/src/HOL/Auth/Event.thy	Tue Aug 20 18:53:17 1996 +0200
     2.3 @@ -85,24 +85,27 @@
     2.4  (*NS3 DOESN'T ALLOW INTERLEAVING -- that is, it only responds to the
     2.5    MOST RECENT message.*)
     2.6  
     2.7 +(*Needham-Schroeder Shared-Key protocol (from BAN paper, page 247)*)
     2.8  consts  traces   :: "event list set"
     2.9  inductive traces
    2.10    intrs 
    2.11 +         (*Initial trace is empty*)
    2.12      Nil  "[]: traces"
    2.13  
    2.14 -    (*The enemy MAY say anything he CAN say.  We do not expect him to
    2.15 -      invent new nonces here, but he can also use NS1.*)
    2.16 -    Fake "[| evs: traces;  B ~= Enemy;  
    2.17 -             X: synth(analz(sees Enemy evs))
    2.18 +         (*The enemy MAY say anything he CAN say.  We do not expect him to
    2.19 +           invent new nonces here, but he can also use NS1.  Common to
    2.20 +           all similar protocols.*)
    2.21 +    Fake "[| evs: traces;  B ~= Enemy;  X: synth (analz (sees Enemy evs))
    2.22            |] ==> (Says Enemy B X) # evs : traces"
    2.23  
    2.24 +         (*Alice initiates a protocol run*)
    2.25      NS1  "[| evs: traces;  A ~= Server
    2.26            |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) 
    2.27                   # evs : traces"
    2.28  
    2.29 -          (*We can't trust the sender field, hence the A' in it.
    2.30 -            This allows the Server to respond more than once to A's
    2.31 -            request...*)
    2.32 +         (*Server's response to Alice's message.
    2.33 +           !! It may respond more than once to A's request !!
    2.34 +	   We can't trust the sender field, hence the A' in it.*)
    2.35      NS2  "[| evs: traces;  A ~= B;  A ~= Server;
    2.36               (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    2.37            |] ==> (Says Server A 
    2.38 @@ -110,9 +113,9 @@
    2.39                             (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
    2.40                     (serverKey A))) # evs : traces"
    2.41  
    2.42 -           (*We can't assume S=Server.  Agent A "remembers" her nonce.
    2.43 -             May assume WLOG that she is NOT the Enemy: the Fake rule
    2.44 -             covers this case.  Can inductively show A ~= Server*)
    2.45 +          (*We can't assume S=Server.  Agent A "remembers" her nonce.
    2.46 +            May assume WLOG that she is NOT the Enemy: the Fake rule
    2.47 +            covers this case.  Can inductively show A ~= Server*)
    2.48      NS3  "[| evs: traces;  A ~= B;
    2.49               (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
    2.50                 : set_of_list evs;
    2.51 @@ -120,12 +123,8 @@
    2.52               (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    2.53            |] ==> (Says A B X) # evs : traces"
    2.54  
    2.55 -(*Initial version of NS2 had 
    2.56 -
    2.57 -        {|Agent A, Agent B, Key (newK evs), Nonce NA|}
    2.58 -
    2.59 -  for the encrypted part; the version above is LESS explicit, hence
    2.60 -  HARDER to prove.  Also it is precisely as in the BAN paper.
    2.61 -*)
    2.62 -
    2.63 +    NS4  "[| evs: traces;  A ~= B;  
    2.64 +             (Says A' B (Crypt {|Key K, Agent A|} (serverKey B))) 
    2.65 +               : set_of_list evs
    2.66 +          |] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : traces"
    2.67  end