src/HOL/Auth/Event.thy
author paulson
Tue, 03 Sep 1996 17:54:39 +0200
changeset 1942 6c9c1a42a869
parent 1933 8b24773de6db
child 2032 1bbf1bdcaf56
permissions -rw-r--r--
Renaming and simplification
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/Message
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     2
    ID:         $Id$
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     5
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     6
Datatype of events;
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     7
inductive relation "traces" for Needham-Schroeder (shared keys)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
     8
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
     9
INTERLEAVING?  See defn of "traces"
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    10
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    11
WHAT ABOUT ASYMMETRIC KEYS?  NOBODY'S PRIVATE KEY CAN EQUAL SOMEBODY ELSE'S
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    12
  PUBLIC KEY...
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    13
*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    14
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    15
Event = Message + List + 
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    16
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    17
consts
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    18
  publicKey    :: agent => key
1942
6c9c1a42a869 Renaming and simplification
paulson
parents: 1933
diff changeset
    19
  shrK    :: agent => key  (*symmetric keys*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    20
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    21
rules
1942
6c9c1a42a869 Renaming and simplification
paulson
parents: 1933
diff changeset
    22
  isSym_shrK "isSymKey (shrK A)"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    23
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    24
consts  (*Initial states of agents -- parameter of the construction*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    25
  initState :: agent => msg set
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    26
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    27
primrec initState agent
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    28
        (*Server knows all keys; other agents know only their own*)
1942
6c9c1a42a869 Renaming and simplification
paulson
parents: 1933
diff changeset
    29
  initState_Server  "initState Server     = Key `` range shrK"
6c9c1a42a869 Renaming and simplification
paulson
parents: 1933
diff changeset
    30
  initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
6c9c1a42a869 Renaming and simplification
paulson
parents: 1933
diff changeset
    31
  initState_Enemy   "initState Enemy  = {Key (shrK Enemy)}"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    32
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    33
(**
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    34
For asymmetric keys: server knows all public and private keys,
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    35
  others know their private key and perhaps all public keys  
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    36
**)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    37
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    38
datatype  (*Messages, and components of agent stores*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    39
  event = Says agent agent msg
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    40
        | Notes agent msg
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    41
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    42
consts  
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    43
  sees1 :: [agent, event] => msg set
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    44
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    45
primrec sees1 event
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    46
           (*First agent recalls all that it says, but NOT everything
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    47
             that is sent to it; it must note such things if/when received*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    48
  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    49
          (*part of A's internal state*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    50
  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' then {X} else {})"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    51
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    52
consts  
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    53
  sees :: [agent, event list] => msg set
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    54
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    55
primrec sees list
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    56
        (*Initial knowledge includes all public keys and own private key*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    57
  sees_Nil  "sees A []       = initState A"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    58
  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    59
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    60
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    61
constdefs
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    62
  knownBy :: [event list, msg] => agent set
1913
2809adb15eb0 Renaming of functions, and tidying
paulson
parents: 1893
diff changeset
    63
  "knownBy evs X == {A. X: analz (sees A evs)}"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    64
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    65
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    66
(*Agents generate "random" nonces.  Different traces always yield
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    67
  different nonces.  Same applies for keys.*)
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    68
(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS.
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    69
  NEED AXIOM SAYING THAT NEW KEYS CANNOT EQUAL THE INVERSE OF A PREVIOUS KEY*)
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    70
consts
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    71
  newN :: "event list => nat"
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    72
  newK :: "event list => key"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    73
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    74
rules
1942
6c9c1a42a869 Renaming and simplification
paulson
parents: 1933
diff changeset
    75
  inj_shrK "inj shrK"
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    76
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    77
  inj_newN   "inj(newN)"
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    78
  fresh_newN "Nonce (newN evs) ~: parts (initState B)" 
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    79
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    80
  inj_newK   "inj(newK)"
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    81
  fresh_newK "Key (newK evs) ~: parts (initState B)" 
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    82
  isSym_newK "isSymKey (newK evs)"
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
    83
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    84
1930
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
    85
(*Needham-Schroeder Shared-Key protocol (from BAN paper, page 247)*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    86
consts  traces   :: "event list set"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    87
inductive traces
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    88
  intrs 
1930
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
    89
         (*Initial trace is empty*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    90
    Nil  "[]: traces"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    91
1930
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
    92
         (*The enemy MAY say anything he CAN say.  We do not expect him to
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
    93
           invent new nonces here, but he can also use NS1.  Common to
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
    94
           all similar protocols.*)
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
    95
    Fake "[| evs: traces;  B ~= Enemy;  X: synth (analz (sees Enemy evs))
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    96
          |] ==> (Says Enemy B X) # evs : traces"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    97
1930
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
    98
         (*Alice initiates a protocol run*)
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
    99
    NS1  "[| evs: traces;  A ~= Server
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   100
          |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) 
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   101
                 # evs : traces"
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   102
1930
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
   103
         (*Server's response to Alice's message.
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
   104
           !! It may respond more than once to A's request !!
1933
8b24773de6db Addition of message NS5
paulson
parents: 1930
diff changeset
   105
	   Server doesn't know who the true sender is, hence the A' in
8b24773de6db Addition of message NS5
paulson
parents: 1930
diff changeset
   106
               the sender field.*)
1893
fa58f4a06f21 Works up to main theorem, then XXX...X
paulson
parents: 1885
diff changeset
   107
    NS2  "[| evs: traces;  A ~= B;  A ~= Server;
1929
f0839bab4b00 Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents: 1913
diff changeset
   108
             (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   109
          |] ==> (Says Server A 
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   110
                  (Crypt {|Nonce NA, Agent B, Key (newK evs),   
1942
6c9c1a42a869 Renaming and simplification
paulson
parents: 1933
diff changeset
   111
                           (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
6c9c1a42a869 Renaming and simplification
paulson
parents: 1933
diff changeset
   112
                   (shrK A))) # evs : traces"
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   113
1930
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
   114
          (*We can't assume S=Server.  Agent A "remembers" her nonce.
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
   115
            May assume WLOG that she is NOT the Enemy: the Fake rule
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
   116
            covers this case.  Can inductively show A ~= Server*)
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   117
    NS3  "[| evs: traces;  A ~= B;
1942
6c9c1a42a869 Renaming and simplification
paulson
parents: 1933
diff changeset
   118
             (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))) 
1929
f0839bab4b00 Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents: 1913
diff changeset
   119
               : set_of_list evs;
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   120
             A = Friend i;
1929
f0839bab4b00 Working version of NS, messages 1-3, WITH INTERLEAVING
paulson
parents: 1913
diff changeset
   121
             (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
1852
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   122
          |] ==> (Says A B X) # evs : traces"
289ce6cb5c84 Added Msg 3; works up to Says_Server_imp_Key_newK
paulson
parents: 1839
diff changeset
   123
1933
8b24773de6db Addition of message NS5
paulson
parents: 1930
diff changeset
   124
         (*Bob's nonce exchange.  He does not know who the message came
8b24773de6db Addition of message NS5
paulson
parents: 1930
diff changeset
   125
           from, but responds to A because she is mentioned inside.*)
1930
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
   126
    NS4  "[| evs: traces;  A ~= B;  
1942
6c9c1a42a869 Renaming and simplification
paulson
parents: 1933
diff changeset
   127
             (Says A' B (Crypt {|Key K, Agent A|} (shrK B))) 
1930
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
   128
               : set_of_list evs
cdf9bcd53749 Working version of NS, messages 1-4!
paulson
parents: 1929
diff changeset
   129
          |] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : traces"
1933
8b24773de6db Addition of message NS5
paulson
parents: 1930
diff changeset
   130
8b24773de6db Addition of message NS5
paulson
parents: 1930
diff changeset
   131
         (*Alice responds with (Suc N), if she has seen the key before.*)
8b24773de6db Addition of message NS5
paulson
parents: 1930
diff changeset
   132
    NS5  "[| evs: traces;  A ~= B;  
8b24773de6db Addition of message NS5
paulson
parents: 1930
diff changeset
   133
             (Says B' A (Crypt (Nonce N) K)) : set_of_list evs;
1942
6c9c1a42a869 Renaming and simplification
paulson
parents: 1933
diff changeset
   134
             (Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))) 
1933
8b24773de6db Addition of message NS5
paulson
parents: 1930
diff changeset
   135
               : set_of_list evs
8b24773de6db Addition of message NS5
paulson
parents: 1930
diff changeset
   136
          |] ==> (Says A B (Crypt (Nonce (Suc N)) K)) # evs : traces"
8b24773de6db Addition of message NS5
paulson
parents: 1930
diff changeset
   137
1839
199243afac2b Proving safety properties of authentication protocols
paulson
parents:
diff changeset
   138
end