src/HOL/Auth/Event.thy
changeset 1852 289ce6cb5c84
parent 1839 199243afac2b
child 1885 a18a6dc14f76
     1.1 --- a/src/HOL/Auth/Event.thy	Thu Jul 11 15:28:10 1996 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Thu Jul 11 15:30:22 1996 +0200
     1.3 @@ -6,6 +6,8 @@
     1.4  Datatype of events;
     1.5  inductive relation "traces" for Needham-Schroeder (shared keys)
     1.6  
     1.7 +INTERLEAVING?  See defn of "traces"
     1.8 +
     1.9  WHAT ABOUT ASYMMETRIC KEYS?  NOBODY'S PRIVATE KEY CAN EQUAL SOMEBODY ELSE'S
    1.10    PUBLIC KEY...
    1.11  *)
    1.12 @@ -14,16 +16,16 @@
    1.13  
    1.14  consts
    1.15    publicKey    :: agent => key
    1.16 -  serverKey    :: agent => key	(*symmetric keys*)
    1.17 +  serverKey    :: agent => key  (*symmetric keys*)
    1.18  
    1.19  rules
    1.20    isSym_serverKey "isSymKey (serverKey A)"
    1.21  
    1.22 -consts	(*Initial states of agents -- parameter of the construction*)
    1.23 +consts  (*Initial states of agents -- parameter of the construction*)
    1.24    initState :: agent => msg set
    1.25  
    1.26  primrec initState agent
    1.27 -	(*Server knows all keys; other agents know only their own*)
    1.28 +        (*Server knows all keys; other agents know only their own*)
    1.29    initState_Server  "initState Server     = range (Key o serverKey)"
    1.30    initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
    1.31    initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
    1.32 @@ -51,7 +53,7 @@
    1.33    sees :: [agent, event list] => msg set
    1.34  
    1.35  primrec sees list
    1.36 -	(*Initial knowledge includes all public keys and own private key*)
    1.37 +        (*Initial knowledge includes all public keys and own private key*)
    1.38    sees_Nil  "sees A []       = initState A"
    1.39    sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
    1.40  
    1.41 @@ -61,25 +63,29 @@
    1.42    "knownBy evs X == {A. X: analyze (sees A evs)}"
    1.43  
    1.44  
    1.45 -(*Agents generate "random" nonces.  Different agents always generate
    1.46 -  different nonces.  Different traces also yield different nonces.  Same
    1.47 -  applies for keys.*)
    1.48 -(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS.  REMOVE AGENT ARGUMENT?
    1.49 +(*Agents generate "random" nonces.  Different traces always yield
    1.50 +  different nonces.  Same applies for keys.*)
    1.51 +(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS.
    1.52    NEED AXIOM SAYING THAT NEW KEYS CANNOT EQUAL THE INVERSE OF A PREVIOUS KEY*)
    1.53  consts
    1.54 -  newN :: "agent * event list => nat"
    1.55 -  newK :: "agent * event list => key"
    1.56 +  newN :: "event list => nat"
    1.57 +  newK :: "event list => key"
    1.58  
    1.59  rules
    1.60    inj_serverKey "inj serverKey"
    1.61  
    1.62    inj_newN   "inj(newN)"
    1.63 -  fresh_newN "Nonce (newN(A,evs)) ~: parts (initState B)" 
    1.64 +  fresh_newN "Nonce (newN evs) ~: parts (initState B)" 
    1.65  
    1.66    inj_newK   "inj(newK)"
    1.67 -  fresh_newK "Key (newK(A,evs)) ~: parts (initState B)" 
    1.68 -  isSym_newK "isSymKey (newK(A,evs))"
    1.69 +  fresh_newK "Key (newK evs) ~: parts (initState B)" 
    1.70 +  isSym_newK "isSymKey (newK evs)"
    1.71 +
    1.72  
    1.73 +(*NS1 AND NS2 DON'T ALLOW INTERLEAVING -- that is, they only respond to the
    1.74 +  MOST RECENT message.  Does this mean we can't model middleperson attacks?
    1.75 +  We don't need the most recent restriction in order to handle interception
    1.76 +  by the Enemy, as agents are not forced to respond anyway.*)
    1.77  
    1.78  consts  traces   :: "event list set"
    1.79  inductive traces
    1.80 @@ -88,17 +94,39 @@
    1.81  
    1.82      (*The enemy MAY say anything he CAN say.  We do not expect him to
    1.83        invent new nonces here, but he can also use NS1.*)
    1.84 -    Fake "[| evs: traces;  X: synthesize(analyze(sees Enemy evs))
    1.85 +    Fake "[| evs: traces;  B ~= Enemy;  
    1.86 +             X: synthesize(analyze(sees Enemy evs))
    1.87            |] ==> (Says Enemy B X) # evs : traces"
    1.88  
    1.89      NS1  "[| evs: traces;  A ~= Server
    1.90 -          |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN(A,evs))|}) 
    1.91 +          |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) 
    1.92                   # evs : traces"
    1.93  
    1.94 -    NS2  "[| evs: traces;  
    1.95 +          (*We can't trust the sender field: change that A to A'?  *)
    1.96 +    NS2  "[| evs: traces;  A ~= B;
    1.97               evs = (Says A Server {|Agent A, Agent B, Nonce NA|}) # evs'
    1.98            |] ==> (Says Server A 
    1.99 -                       (Crypt {|Agent A, Agent B, 
   1.100 -                                Key (newK(Server,evs)), Nonce NA|}
   1.101 -                              (serverKey A))) # evs : traces"
   1.102 +                  (Crypt {|Nonce NA, Agent B, Key (newK evs),   
   1.103 +                           (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
   1.104 +                   (serverKey A))) # evs : traces"
   1.105 +
   1.106 +           (*We can't assume S=Server.  Agent A "remembers" her nonce.
   1.107 +             May assume WLOG that she is NOT the Enemy, as the Fake rule.
   1.108 +             covers this case.  Can inductively show A ~= Server*)
   1.109 +    NS3  "[| evs: traces;  A ~= B;
   1.110 +             evs = (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}
   1.111 +                              (serverKey A))) 
   1.112 +                   # evs';
   1.113 +             A = Friend i;
   1.114 +             (Says A Server {|Agent A, Agent B, Nonce NA|}) : setOfList evs'
   1.115 +          |] ==> (Says A B X) # evs : traces"
   1.116 +
   1.117 +(*Initial version of NS2 had 
   1.118 +
   1.119 +        {|Agent A, Agent B, Key (newK evs), Nonce NA|}
   1.120 +
   1.121 +  for the encrypted part; the version above is LESS transparent, hence
   1.122 +  maybe HARDER to prove.  Also it is precisely as in the BAN paper.
   1.123 +*)
   1.124 +
   1.125  end