src/HOL/Auth/Shared.thy
author paulson
Wed, 09 Oct 1996 13:43:51 +0200
changeset 2078 b198b3d46fb4
parent 2064 5a5e508e2a2b
child 2264 f298678bd54a
permissions -rw-r--r--
New version of axiom sees1_Says: Previously it only allowed the SENDER to see the content of messages... Now instead the RECIPIENT sees the messages. This change had no effect on subsequent proofs because protocol rules refer specifically to the relevant messages sent to an agent.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/Shared
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     2
    ID:         $Id$
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     5
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     6
Theory of Shared Keys (common to all symmetric-key protocols)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     7
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     8
Server keys; initial states of agents; new nonces and keys; function "sees" 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     9
*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    10
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    11
Shared = Message + List + 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    12
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    13
consts
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
    14
  shrK    :: agent => key  (*symmetric keys*)
1967
0ff58b41c037 "bad" set simplifies statements of many theorems
paulson
parents: 1965
diff changeset
    15
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    16
rules
1943
20574dca5a3e Renaming and simplification
paulson
parents: 1934
diff changeset
    17
  isSym_shrK "isSymKey (shrK A)"
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    18
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    19
consts  (*Initial states of agents -- parameter of the construction*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    20
  initState :: [agent set, agent] => msg set
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    21
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    22
primrec initState agent
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    23
        (*Server knows all keys; other agents know only their own*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    24
  initState_Server  "initState lost Server     = Key `` range shrK"
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    25
  initState_Friend  "initState lost (Friend i) = {Key (shrK (Friend i))}"
2064
5a5e508e2a2b Simple tidying
paulson
parents: 2032
diff changeset
    26
  initState_Spy     "initState lost Spy        = Key``shrK``lost"
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    27
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    28
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    29
datatype  (*Messages, and components of agent stores*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    30
  event = Says agent agent msg
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    31
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    32
consts  
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    33
  sees1 :: [agent, event] => msg set
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    34
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    35
primrec sees1 event
2078
b198b3d46fb4 New version of axiom sees1_Says:
paulson
parents: 2064
diff changeset
    36
           (*Spy reads all traffic whether addressed to him or not*)
b198b3d46fb4 New version of axiom sees1_Says:
paulson
parents: 2064
diff changeset
    37
  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    38
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    39
consts  
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    40
  sees :: [agent set, agent, event list] => msg set
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    41
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    42
primrec sees list
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    43
        (*Initial knowledge includes all public keys and own private key*)
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    44
  sees_Nil  "sees lost A []       = initState lost A"
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    45
  sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    46
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    47
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    48
(*Agents generate "random" nonces.  Different traces always yield
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    49
  different nonces.  Same applies for keys.*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    50
consts
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    51
  newN :: "event list => nat"
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    52
  newK :: "event list => key"
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    53
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    54
rules
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    55
  inj_shrK      "inj shrK"
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    56
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    57
  inj_newN      "inj newN"
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    58
2032
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    59
  inj_newK      "inj newK"
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    60
  newK_neq_shrK "newK evs ~= shrK A" 
1bbf1bdcaf56 Introduction of "lost" argument
paulson
parents: 2012
diff changeset
    61
  isSym_newK    "isSymKey (newK evs)"
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    62
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    63
end