src/HOL/Auth/Event.thy
author paulson
Thu, 18 Sep 1997 13:24:04 +0200
changeset 3683 aafe719dff14
parent 3678 414e04d7c2d6
child 5183 89f162de39cf
permissions -rw-r--r--
Global change: lost->bad and sees Spy->spies First change just gives a more sensible name. Second change eliminates the agent parameter of "sees" to simplify definitions and theorems
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
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
     8
Datatype of events; function "spies"; freshness
3678
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3519
diff changeset
     9
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    10
"bad" agents have been broken by the Spy; their private keys and internal
3678
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3519
diff changeset
    11
    stores are visible to him
3512
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
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    14
Event = Message + List + 
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
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
    17
  initState :: agent => msg set
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    18
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    19
datatype  (*Messages--could add another constructor for agent knowledge*)
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    20
  event = Says  agent agent msg
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    21
        | Notes agent       msg
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
consts  
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    24
  bad    :: agent set        (*compromised agents*)
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    25
  spies  :: event list => msg set
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    26
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    27
rules
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    28
  (*Spy has access to his own key for spoof messages, but Server is secure*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    29
  Spy_in_bad     "Spy: bad"
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    30
  Server_not_bad "Server ~: bad"
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    31
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    32
primrec spies list
3678
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3519
diff changeset
    33
           (*Spy reads all traffic whether addressed to him or not*)
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    34
  spies_Nil   "spies []       = initState Spy"
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    35
  spies_Cons  "spies (ev # evs) =
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    36
	         (case ev of
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    37
		    Says A B X => insert X (spies evs)
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    38
		  | Notes A X  => 
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    39
	              if A:bad then insert X (spies evs) else spies evs)"
3678
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3519
diff changeset
    40
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    41
consts
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    42
  (*Set of items that might be visible to somebody:
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    43
    complement of the set of fresh items*)
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    44
  used :: event list => msg set
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    45
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    46
primrec used list
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    47
  used_Nil   "used []         = (UN B. parts (initState B))"
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    48
  used_Cons  "used (ev # evs) =
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    49
	         (case ev of
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    50
		    Says A B X => parts {X} Un (used evs)
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    51
		  | Notes A X  => parts {X} Un (used evs))"
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    52
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    53
end