src/HOL/Auth/Event.thy
changeset 1929 f0839bab4b00
parent 1913 2809adb15eb0
child 1930 cdf9bcd53749
     1.1 --- a/src/HOL/Auth/Event.thy	Tue Aug 20 12:40:17 1996 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Tue Aug 20 17:46:24 1996 +0200
     1.3 @@ -82,10 +82,8 @@
     1.4    isSym_newK "isSymKey (newK evs)"
     1.5  
     1.6  
     1.7 -(*NS1 AND NS2 DON'T ALLOW INTERLEAVING -- that is, they only respond to the
     1.8 -  MOST RECENT message.  Does this mean we can't model middleperson attacks?
     1.9 -  We don't need the most recent restriction in order to handle interception
    1.10 -  by the Enemy, as agents are not forced to respond anyway.*)
    1.11 +(*NS3 DOESN'T ALLOW INTERLEAVING -- that is, it only responds to the
    1.12 +  MOST RECENT message.*)
    1.13  
    1.14  consts  traces   :: "event list set"
    1.15  inductive traces
    1.16 @@ -102,9 +100,11 @@
    1.17            |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) 
    1.18                   # evs : traces"
    1.19  
    1.20 -          (*We can't trust the sender field, hence the A' in it  *)
    1.21 +          (*We can't trust the sender field, hence the A' in it.
    1.22 +            This allows the Server to respond more than once to A's
    1.23 +            request...*)
    1.24      NS2  "[| evs: traces;  A ~= B;  A ~= Server;
    1.25 -             evs = (Says A' Server {|Agent A, Agent B, Nonce NA|}) # evs'
    1.26 +             (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    1.27            |] ==> (Says Server A 
    1.28                    (Crypt {|Nonce NA, Agent B, Key (newK evs),   
    1.29                             (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
    1.30 @@ -114,11 +114,10 @@
    1.31               May assume WLOG that she is NOT the Enemy: the Fake rule
    1.32               covers this case.  Can inductively show A ~= Server*)
    1.33      NS3  "[| evs: traces;  A ~= B;
    1.34 -             evs = (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}
    1.35 -                              (serverKey A))) 
    1.36 -                   # evs';
    1.37 +             (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
    1.38 +               : set_of_list evs;
    1.39               A = Friend i;
    1.40 -             (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs'
    1.41 +             (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    1.42            |] ==> (Says A B X) # evs : traces"
    1.43  
    1.44  (*Initial version of NS2 had