(*  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