src/HOL/Auth/Event.thy

Works up to main theorem, then XXX...X

(*  Title:      HOL/Auth/Message
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1996  University of Cambridge

Datatype of events;
inductive relation "traces" for Needham-Schroeder (shared keys)

INTERLEAVING?  See defn of "traces"

WHAT ABOUT ASYMMETRIC KEYS?  NOBODY'S PRIVATE KEY CAN EQUAL SOMEBODY ELSE'S
  PUBLIC KEY...
*)

Event = Message + List + 

consts
  publicKey    :: agent => key
  serverKey    :: agent => key  (*symmetric keys*)

rules
  isSym_serverKey "isSymKey (serverKey A)"

consts  (*Initial states of agents -- parameter of the construction*)
  initState :: agent => msg set

primrec initState agent
        (*Server knows all keys; other agents know only their own*)
  initState_Server  "initState Server     = Key `` range serverKey"
  initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
  initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"

(**
For asymmetric keys: server knows all public and private keys,
  others know their private key and perhaps all public keys  
**)

datatype  (*Messages, and components of agent stores*)
  event = Says agent agent msg
        | Notes agent msg

consts  
  sees1 :: [agent, event] => msg set

primrec sees1 event
           (*First agent recalls all that it says, but NOT everything
             that is sent to it; it must note such things if/when received*)
  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
          (*part of A's internal state*)
  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' then {X} else {})"

consts  
  sees :: [agent, event list] => msg set

primrec sees list
        (*Initial knowledge includes all public keys and own private key*)
  sees_Nil  "sees A []       = initState A"
  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"


constdefs
  knownBy :: [event list, msg] => agent set
  "knownBy evs X == {A. X: analyze (sees A evs)}"


(*Agents generate "random" nonces.  Different traces always yield
  different nonces.  Same applies for keys.*)
(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS.
  NEED AXIOM SAYING THAT NEW KEYS CANNOT EQUAL THE INVERSE OF A PREVIOUS KEY*)
consts
  newN :: "event list => nat"
  newK :: "event list => key"

rules
  inj_serverKey "inj serverKey"

  inj_newN   "inj(newN)"
  fresh_newN "Nonce (newN evs) ~: parts (initState B)" 

  inj_newK   "inj(newK)"
  fresh_newK "Key (newK evs) ~: parts (initState B)" 
  isSym_newK "isSymKey (newK evs)"


(*NS1 AND NS2 DON'T ALLOW INTERLEAVING -- that is, they only respond to the
  MOST RECENT message.  Does this mean we can't model middleperson attacks?
  We don't need the most recent restriction in order to handle interception
  by the Enemy, as agents are not forced to respond anyway.*)

consts  traces   :: "event list set"
inductive traces
  intrs 
    Nil  "[]: traces"

    (*The enemy MAY say anything he CAN say.  We do not expect him to
      invent new nonces here, but he can also use NS1.*)
    Fake "[| evs: traces;  B ~= Enemy;  
             X: synthesize(analyze(sees Enemy evs))
          |] ==> (Says Enemy B X) # evs : traces"

    NS1  "[| evs: traces;  A ~= Server
          |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) 
                 # evs : traces"

          (*We can't trust the sender field, hence the A' in it  *)
    NS2  "[| evs: traces;  A ~= B;  A ~= Server;
             evs = (Says A' Server {|Agent A, Agent B, Nonce NA|}) # evs'
          |] ==> (Says Server A 
                  (Crypt {|Nonce NA, Agent B, Key (newK evs),   
                           (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
                   (serverKey A))) # evs : traces"

           (*We can't assume S=Server.  Agent A "remembers" her nonce.
             May assume WLOG that she is NOT the Enemy: the Fake rule
             covers this case.  Can inductively show A ~= Server*)
    NS3  "[| evs: traces;  A ~= B;
             evs = (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}
                              (serverKey A))) 
                   # evs';
             A = Friend i;
             (Says A Server {|Agent A, Agent B, Nonce NA|}) : setOfList evs'
          |] ==> (Says A B X) # evs : traces"

(*Initial version of NS2 had 

        {|Agent A, Agent B, Key (newK evs), Nonce NA|}

  for the encrypted part; the version above is LESS transparent, hence
  maybe HARDER to prove.  Also it is precisely as in the BAN paper.
*)

end