src/HOL/Auth/Event.thy
changeset 1839 199243afac2b
child 1852 289ce6cb5c84
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Auth/Event.thy	Fri Jun 28 15:26:39 1996 +0200
     1.3 @@ -0,0 +1,104 @@
     1.4 +(*  Title:      HOL/Auth/Message
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Datatype of events;
    1.10 +inductive relation "traces" for Needham-Schroeder (shared keys)
    1.11 +
    1.12 +WHAT ABOUT ASYMMETRIC KEYS?  NOBODY'S PRIVATE KEY CAN EQUAL SOMEBODY ELSE'S
    1.13 +  PUBLIC KEY...
    1.14 +*)
    1.15 +
    1.16 +Event = Message + List + 
    1.17 +
    1.18 +consts
    1.19 +  publicKey    :: agent => key
    1.20 +  serverKey    :: agent => key	(*symmetric keys*)
    1.21 +
    1.22 +rules
    1.23 +  isSym_serverKey "isSymKey (serverKey A)"
    1.24 +
    1.25 +consts	(*Initial states of agents -- parameter of the construction*)
    1.26 +  initState :: agent => msg set
    1.27 +
    1.28 +primrec initState agent
    1.29 +	(*Server knows all keys; other agents know only their own*)
    1.30 +  initState_Server  "initState Server     = range (Key o serverKey)"
    1.31 +  initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
    1.32 +  initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
    1.33 +
    1.34 +(**
    1.35 +For asymmetric keys: server knows all public and private keys,
    1.36 +  others know their private key and perhaps all public keys  
    1.37 +**)
    1.38 +
    1.39 +datatype  (*Messages, and components of agent stores*)
    1.40 +  event = Says agent agent msg
    1.41 +        | Notes agent msg
    1.42 +
    1.43 +consts  
    1.44 +  sees1 :: [agent, event] => msg set
    1.45 +
    1.46 +primrec sees1 event
    1.47 +           (*First agent recalls all that it says, but NOT everything
    1.48 +             that is sent to it; it must note such things if/when received*)
    1.49 +  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
    1.50 +          (*part of A's internal state*)
    1.51 +  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' then {X} else {})"
    1.52 +
    1.53 +consts  
    1.54 +  sees :: [agent, event list] => msg set
    1.55 +
    1.56 +primrec sees list
    1.57 +	(*Initial knowledge includes all public keys and own private key*)
    1.58 +  sees_Nil  "sees A []       = initState A"
    1.59 +  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
    1.60 +
    1.61 +
    1.62 +constdefs
    1.63 +  knownBy :: [event list, msg] => agent set
    1.64 +  "knownBy evs X == {A. X: analyze (sees A evs)}"
    1.65 +
    1.66 +
    1.67 +(*Agents generate "random" nonces.  Different agents always generate
    1.68 +  different nonces.  Different traces also yield different nonces.  Same
    1.69 +  applies for keys.*)
    1.70 +(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS.  REMOVE AGENT ARGUMENT?
    1.71 +  NEED AXIOM SAYING THAT NEW KEYS CANNOT EQUAL THE INVERSE OF A PREVIOUS KEY*)
    1.72 +consts
    1.73 +  newN :: "agent * event list => nat"
    1.74 +  newK :: "agent * event list => key"
    1.75 +
    1.76 +rules
    1.77 +  inj_serverKey "inj serverKey"
    1.78 +
    1.79 +  inj_newN   "inj(newN)"
    1.80 +  fresh_newN "Nonce (newN(A,evs)) ~: parts (initState B)" 
    1.81 +
    1.82 +  inj_newK   "inj(newK)"
    1.83 +  fresh_newK "Key (newK(A,evs)) ~: parts (initState B)" 
    1.84 +  isSym_newK "isSymKey (newK(A,evs))"
    1.85 +
    1.86 +
    1.87 +consts  traces   :: "event list set"
    1.88 +inductive traces
    1.89 +  intrs 
    1.90 +    Nil  "[]: traces"
    1.91 +
    1.92 +    (*The enemy MAY say anything he CAN say.  We do not expect him to
    1.93 +      invent new nonces here, but he can also use NS1.*)
    1.94 +    Fake "[| evs: traces;  X: synthesize(analyze(sees Enemy evs))
    1.95 +          |] ==> (Says Enemy B X) # evs : traces"
    1.96 +
    1.97 +    NS1  "[| evs: traces;  A ~= Server
    1.98 +          |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN(A,evs))|}) 
    1.99 +                 # evs : traces"
   1.100 +
   1.101 +    NS2  "[| evs: traces;  
   1.102 +             evs = (Says A Server {|Agent A, Agent B, Nonce NA|}) # evs'
   1.103 +          |] ==> (Says Server A 
   1.104 +                       (Crypt {|Agent A, Agent B, 
   1.105 +                                Key (newK(Server,evs)), Nonce NA|}
   1.106 +                              (serverKey A))) # evs : traces"
   1.107 +end