src/HOL/Auth/Event.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 6399 4a9040b85e2e
child 11104 f2024fed9f0c
permissions -rw-r--r--
hide many names from Datatype_Universe.
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
6399
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    19
datatype
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    20
  event = Says  agent agent msg
6399
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    21
        | Gets  agent       msg
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    22
        | Notes agent       msg
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    23
       
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    24
consts 
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    25
  bad    :: agent set        (*compromised agents*)
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    26
  knows  :: agent => event list => msg set
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    27
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    28
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    29
(*"spies" is retained for compability's sake*)
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    30
syntax
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    31
  spies  :: event list => msg set
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    32
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    33
translations
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    34
  "spies"   => "knows Spy"
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    35
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    36
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    37
rules
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3512
diff changeset
    38
  (*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
    39
  Spy_in_bad     "Spy: bad"
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    40
  Server_not_bad "Server ~: bad"
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    41
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 3683
diff changeset
    42
primrec
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    43
  knows_Nil   "knows A []         = initState A"
6399
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    44
  knows_Cons
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    45
    "knows A (ev # evs) =
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    46
       (if A = Spy then 
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    47
	(case ev of
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    48
	   Says A' B X => insert X (knows Spy evs)
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    49
	 | Gets A' X => knows Spy evs
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    50
	 | Notes A' X  => 
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    51
	     if A' : bad then insert X (knows Spy evs) else knows Spy evs)
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    52
	else
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    53
	(case ev of
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    54
	   Says A' B X => 
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    55
	     if A'=A then insert X (knows A evs) else knows A evs
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    56
	 | Gets A' X    => 
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    57
	     if A'=A then insert X (knows A evs) else knows A evs
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    58
	 | Notes A' X    => 
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    59
	     if A'=A then insert X (knows A evs) else knows A evs))"
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    60
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    61
(*
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    62
  Case A=Spy on the Gets event
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    63
  enforces the fact that if a message is received then it must have been sent,
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    64
  therefore the oops case must use Notes
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    65
*)
3678
414e04d7c2d6 Spy can see Notes of the compromised agents
paulson
parents: 3519
diff changeset
    66
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    67
consts
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    68
  (*Set of items that might be visible to somebody:
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    69
    complement of the set of fresh items*)
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    70
  used :: event list => msg set
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    71
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 3683
diff changeset
    72
primrec
3683
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    73
  used_Nil   "used []         = (UN B. parts (initState B))"
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    74
  used_Cons  "used (ev # evs) =
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    75
	         (case ev of
aafe719dff14 Global change: lost->bad and sees Spy->spies
paulson
parents: 3678
diff changeset
    76
		    Says A B X => parts {X} Un (used evs)
6399
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    77
		  | Gets A X   => used evs
4a9040b85e2e exchanged the order of Gets and Notes in datatype event
paulson
parents: 6308
diff changeset
    78
		  | Notes A X  => parts {X} Un (used evs))"
6308
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    79
76f3865a2b1d Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents: 5183
diff changeset
    80
3512
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    81
9dcb4daa15e8 Moving common declarations and proofs from theories "Shared"
paulson
parents:
diff changeset
    82
end