src/HOL/Auth/Event.thy
author paulson
Thu Sep 26 12:50:48 1996 +0200 (1996-09-26)
changeset 2032 1bbf1bdcaf56
parent 1942 6c9c1a42a869
permissions -rw-r--r--
Introduction of "lost" argument
Changed Enemy -> Spy
Ran expandshort
     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   shrK    :: agent => key  (*symmetric keys*)
    20 
    21 rules
    22   isSym_shrK "isSymKey (shrK 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 shrK"
    30   initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
    31   initState_Spy   "initState Spy  = {Key (shrK Spy)}"
    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',Spy} 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_shrK "inj shrK"
    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 (*Needham-Schroeder Shared-Key protocol (from BAN paper, page 247)*)
    86 consts  traces   :: "event list set"
    87 inductive traces
    88   intrs 
    89          (*Initial trace is empty*)
    90     Nil  "[]: traces"
    91 
    92          (*The spy MAY say anything he CAN say.  We do not expect him to
    93            invent new nonces here, but he can also use NS1.  Common to
    94            all similar protocols.*)
    95     Fake "[| evs: traces;  B ~= Spy;  X: synth (analz (sees Spy evs))
    96           |] ==> (Says Spy B X) # evs : traces"
    97 
    98          (*Alice initiates a protocol run*)
    99     NS1  "[| evs: traces;  A ~= Server
   100           |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) 
   101                  # evs : traces"
   102 
   103          (*Server's response to Alice's message.
   104            !! It may respond more than once to A's request !!
   105 	   Server doesn't know who the true sender is, hence the A' in
   106                the sender field.*)
   107     NS2  "[| evs: traces;  A ~= B;  A ~= Server;
   108              (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
   109           |] ==> (Says Server A 
   110                   (Crypt {|Nonce NA, Agent B, Key (newK evs),   
   111                            (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
   112                    (shrK A))) # evs : traces"
   113 
   114           (*We can't assume S=Server.  Agent A "remembers" her nonce.
   115             May assume WLOG that she is NOT the Spy: the Fake rule
   116             covers this case.  Can inductively show A ~= Server*)
   117     NS3  "[| evs: traces;  A ~= B;
   118              (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))) 
   119                : set_of_list 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          (*Bob's nonce exchange.  He does not know who the message came
   125            from, but responds to A because she is mentioned inside.*)
   126     NS4  "[| evs: traces;  A ~= B;  
   127              (Says A' B (Crypt {|Key K, Agent A|} (shrK B))) 
   128                : set_of_list evs
   129           |] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : traces"
   130 
   131          (*Alice responds with (Suc N), if she has seen the key before.*)
   132     NS5  "[| evs: traces;  A ~= B;  
   133              (Says B' A (Crypt (Nonce N) K)) : set_of_list evs;
   134              (Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))) 
   135                : set_of_list evs
   136           |] ==> (Says A B (Crypt (Nonce (Suc N)) K)) # evs : traces"
   137 
   138 end