src/HOL/Auth/Event.thy
author paulson
Mon, 14 Jul 1997 12:47:21 +0200
changeset 3519 ab0a9fbed4c0
parent 3512 9dcb4daa15e8
child 3678 414e04d7c2d6
permissions -rw-r--r--
Changing "lost" from a parameter of protocol definitions to a constant. Advantages: no "lost" argument everywhere; fewer Vars in subgoals; less need for specially instantiated rules Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this theorem was never used, and its original proof was also broken the introduction of the "Notes" constructor.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/Event
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     2
    ID:         $Id$
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     5
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     6
Theory of events for security protocols
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     7
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     8
Datatype of events; function "sees"; freshness
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
     9
*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    10
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    11
Event = Message + List + 
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    12
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    13
consts  (*Initial states of agents -- parameter of the construction*)
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    14
  initState :: agent => msg set
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    15
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    16
datatype  (*Messages--could add another constructor for agent knowledge*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    17
  event = Says  agent agent msg
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    18
        | Notes agent       msg
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    19
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    20
consts  
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    21
  sees1 :: [agent, event] => msg set
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    22
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    23
primrec sees1 event
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    24
           (*Spy reads all traffic whether addressed to him or not*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    25
  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    26
  sees1_Notes "sees1 A (Notes A' X)   = (if A = A'    then {X} else {})"
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    27
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    28
consts  
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    29
  lost :: agent set        (*agents whose private keys have been compromised*)
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    30
  sees :: [agent, event list] => msg set
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    31
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    32
rules
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    33
  (*Spy has access to his own key for spoof messages, but Server is secure*)
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    34
  Spy_in_lost     "Spy: lost"
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    35
  Server_not_lost "Server ~: lost"
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    36
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    37
primrec sees list
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    38
  sees_Nil  "sees A []       = initState A"
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    39
  sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    40
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    41
constdefs
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    42
  (*Set of items that might be visible to somebody: complement of the set
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    43
        of fresh items*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    44
  used :: event list => msg set
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    45
    "used evs == parts (UN B. sees B evs)"
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    46
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    47
end