src/HOL/Auth/Event.thy
author paulson
Fri Jun 28 15:26:39 1996 +0200 (1996-06-28)
changeset 1839 199243afac2b
child 1852 289ce6cb5c84
permissions -rw-r--r--
Proving safety properties of authentication protocols
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@1839
     9
WHAT ABOUT ASYMMETRIC KEYS?  NOBODY'S PRIVATE KEY CAN EQUAL SOMEBODY ELSE'S
paulson@1839
    10
  PUBLIC KEY...
paulson@1839
    11
*)
paulson@1839
    12
paulson@1839
    13
Event = Message + List + 
paulson@1839
    14
paulson@1839
    15
consts
paulson@1839
    16
  publicKey    :: agent => key
paulson@1839
    17
  serverKey    :: agent => key	(*symmetric keys*)
paulson@1839
    18
paulson@1839
    19
rules
paulson@1839
    20
  isSym_serverKey "isSymKey (serverKey A)"
paulson@1839
    21
paulson@1839
    22
consts	(*Initial states of agents -- parameter of the construction*)
paulson@1839
    23
  initState :: agent => msg set
paulson@1839
    24
paulson@1839
    25
primrec initState agent
paulson@1839
    26
	(*Server knows all keys; other agents know only their own*)
paulson@1839
    27
  initState_Server  "initState Server     = range (Key o serverKey)"
paulson@1839
    28
  initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
paulson@1839
    29
  initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
paulson@1839
    30
paulson@1839
    31
(**
paulson@1839
    32
For asymmetric keys: server knows all public and private keys,
paulson@1839
    33
  others know their private key and perhaps all public keys  
paulson@1839
    34
**)
paulson@1839
    35
paulson@1839
    36
datatype  (*Messages, and components of agent stores*)
paulson@1839
    37
  event = Says agent agent msg
paulson@1839
    38
        | Notes agent msg
paulson@1839
    39
paulson@1839
    40
consts  
paulson@1839
    41
  sees1 :: [agent, event] => msg set
paulson@1839
    42
paulson@1839
    43
primrec sees1 event
paulson@1839
    44
           (*First agent recalls all that it says, but NOT everything
paulson@1839
    45
             that is sent to it; it must note such things if/when received*)
paulson@1839
    46
  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
paulson@1839
    47
          (*part of A's internal state*)
paulson@1839
    48
  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' then {X} else {})"
paulson@1839
    49
paulson@1839
    50
consts  
paulson@1839
    51
  sees :: [agent, event list] => msg set
paulson@1839
    52
paulson@1839
    53
primrec sees list
paulson@1839
    54
	(*Initial knowledge includes all public keys and own private key*)
paulson@1839
    55
  sees_Nil  "sees A []       = initState A"
paulson@1839
    56
  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
paulson@1839
    57
paulson@1839
    58
paulson@1839
    59
constdefs
paulson@1839
    60
  knownBy :: [event list, msg] => agent set
paulson@1839
    61
  "knownBy evs X == {A. X: analyze (sees A evs)}"
paulson@1839
    62
paulson@1839
    63
paulson@1839
    64
(*Agents generate "random" nonces.  Different agents always generate
paulson@1839
    65
  different nonces.  Different traces also yield different nonces.  Same
paulson@1839
    66
  applies for keys.*)
paulson@1839
    67
(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS.  REMOVE AGENT ARGUMENT?
paulson@1839
    68
  NEED AXIOM SAYING THAT NEW KEYS CANNOT EQUAL THE INVERSE OF A PREVIOUS KEY*)
paulson@1839
    69
consts
paulson@1839
    70
  newN :: "agent * event list => nat"
paulson@1839
    71
  newK :: "agent * event list => key"
paulson@1839
    72
paulson@1839
    73
rules
paulson@1839
    74
  inj_serverKey "inj serverKey"
paulson@1839
    75
paulson@1839
    76
  inj_newN   "inj(newN)"
paulson@1839
    77
  fresh_newN "Nonce (newN(A,evs)) ~: parts (initState B)" 
paulson@1839
    78
paulson@1839
    79
  inj_newK   "inj(newK)"
paulson@1839
    80
  fresh_newK "Key (newK(A,evs)) ~: parts (initState B)" 
paulson@1839
    81
  isSym_newK "isSymKey (newK(A,evs))"
paulson@1839
    82
paulson@1839
    83
paulson@1839
    84
consts  traces   :: "event list set"
paulson@1839
    85
inductive traces
paulson@1839
    86
  intrs 
paulson@1839
    87
    Nil  "[]: traces"
paulson@1839
    88
paulson@1839
    89
    (*The enemy MAY say anything he CAN say.  We do not expect him to
paulson@1839
    90
      invent new nonces here, but he can also use NS1.*)
paulson@1839
    91
    Fake "[| evs: traces;  X: synthesize(analyze(sees Enemy evs))
paulson@1839
    92
          |] ==> (Says Enemy B X) # evs : traces"
paulson@1839
    93
paulson@1839
    94
    NS1  "[| evs: traces;  A ~= Server
paulson@1839
    95
          |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN(A,evs))|}) 
paulson@1839
    96
                 # evs : traces"
paulson@1839
    97
paulson@1839
    98
    NS2  "[| evs: traces;  
paulson@1839
    99
             evs = (Says A Server {|Agent A, Agent B, Nonce NA|}) # evs'
paulson@1839
   100
          |] ==> (Says Server A 
paulson@1839
   101
                       (Crypt {|Agent A, Agent B, 
paulson@1839
   102
                                Key (newK(Server,evs)), Nonce NA|}
paulson@1839
   103
                              (serverKey A))) # evs : traces"
paulson@1839
   104
end