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