src/HOL/Auth/Event.thy
author paulson
Mon Aug 19 11:19:55 1996 +0200 (1996-08-19)
changeset 1913 2809adb15eb0
parent 1893 fa58f4a06f21
child 1929 f0839bab4b00
permissions -rw-r--r--
Renaming of functions, and tidying
     1 (*  Title:      HOL/Auth/Message
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Datatype of events;
     7 inductive relation "traces" for Needham-Schroeder (shared keys)
     8 
     9 INTERLEAVING?  See defn of "traces"
    10 
    11 WHAT ABOUT ASYMMETRIC KEYS?  NOBODY'S PRIVATE KEY CAN EQUAL SOMEBODY ELSE'S
    12   PUBLIC KEY...
    13 *)
    14 
    15 Event = Message + List + 
    16 
    17 consts
    18   publicKey    :: agent => key
    19   serverKey    :: agent => key  (*symmetric keys*)
    20 
    21 rules
    22   isSym_serverKey "isSymKey (serverKey A)"
    23 
    24 consts  (*Initial states of agents -- parameter of the construction*)
    25   initState :: agent => msg set
    26 
    27 primrec initState agent
    28         (*Server knows all keys; other agents know only their own*)
    29   initState_Server  "initState Server     = Key `` range serverKey"
    30   initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
    31   initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
    32 
    33 (**
    34 For asymmetric keys: server knows all public and private keys,
    35   others know their private key and perhaps all public keys  
    36 **)
    37 
    38 datatype  (*Messages, and components of agent stores*)
    39   event = Says agent agent msg
    40         | Notes agent msg
    41 
    42 consts  
    43   sees1 :: [agent, event] => msg set
    44 
    45 primrec sees1 event
    46            (*First agent recalls all that it says, but NOT everything
    47              that is sent to it; it must note such things if/when received*)
    48   sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
    49           (*part of A's internal state*)
    50   sees1_Notes "sees1 A (Notes A' X)   = (if A=A' then {X} else {})"
    51 
    52 consts  
    53   sees :: [agent, event list] => msg set
    54 
    55 primrec sees list
    56         (*Initial knowledge includes all public keys and own private key*)
    57   sees_Nil  "sees A []       = initState A"
    58   sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
    59 
    60 
    61 constdefs
    62   knownBy :: [event list, msg] => agent set
    63   "knownBy evs X == {A. X: analz (sees A evs)}"
    64 
    65 
    66 (*Agents generate "random" nonces.  Different traces always yield
    67   different nonces.  Same applies for keys.*)
    68 (*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS.
    69   NEED AXIOM SAYING THAT NEW KEYS CANNOT EQUAL THE INVERSE OF A PREVIOUS KEY*)
    70 consts
    71   newN :: "event list => nat"
    72   newK :: "event list => key"
    73 
    74 rules
    75   inj_serverKey "inj serverKey"
    76 
    77   inj_newN   "inj(newN)"
    78   fresh_newN "Nonce (newN evs) ~: parts (initState B)" 
    79 
    80   inj_newK   "inj(newK)"
    81   fresh_newK "Key (newK evs) ~: parts (initState B)" 
    82   isSym_newK "isSymKey (newK evs)"
    83 
    84 
    85 (*NS1 AND NS2 DON'T ALLOW INTERLEAVING -- that is, they only respond to the
    86   MOST RECENT message.  Does this mean we can't model middleperson attacks?
    87   We don't need the most recent restriction in order to handle interception
    88   by the Enemy, as agents are not forced to respond anyway.*)
    89 
    90 consts  traces   :: "event list set"
    91 inductive traces
    92   intrs 
    93     Nil  "[]: traces"
    94 
    95     (*The enemy MAY say anything he CAN say.  We do not expect him to
    96       invent new nonces here, but he can also use NS1.*)
    97     Fake "[| evs: traces;  B ~= Enemy;  
    98              X: synth(analz(sees Enemy evs))
    99           |] ==> (Says Enemy B X) # evs : traces"
   100 
   101     NS1  "[| evs: traces;  A ~= Server
   102           |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) 
   103                  # evs : traces"
   104 
   105           (*We can't trust the sender field, hence the A' in it  *)
   106     NS2  "[| evs: traces;  A ~= B;  A ~= Server;
   107              evs = (Says A' Server {|Agent A, Agent B, Nonce NA|}) # evs'
   108           |] ==> (Says Server A 
   109                   (Crypt {|Nonce NA, Agent B, Key (newK evs),   
   110                            (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
   111                    (serverKey A))) # evs : traces"
   112 
   113            (*We can't assume S=Server.  Agent A "remembers" her nonce.
   114              May assume WLOG that she is NOT the Enemy: the Fake rule
   115              covers this case.  Can inductively show A ~= Server*)
   116     NS3  "[| evs: traces;  A ~= B;
   117              evs = (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|}
   118                               (serverKey A))) 
   119                    # evs';
   120              A = Friend i;
   121              (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs'
   122           |] ==> (Says A B X) # evs : traces"
   123 
   124 (*Initial version of NS2 had 
   125 
   126         {|Agent A, Agent B, Key (newK evs), Nonce NA|}
   127 
   128   for the encrypted part; the version above is LESS explicit, hence
   129   HARDER to prove.  Also it is precisely as in the BAN paper.
   130 *)
   131 
   132 end