src/HOL/Auth/Event.thy
changeset 3678 414e04d7c2d6
parent 3519 ab0a9fbed4c0
child 3683 aafe719dff14
equal deleted inserted replaced
3677:f2569416d18b 3678:414e04d7c2d6
     4     Copyright   1996  University of Cambridge
     4     Copyright   1996  University of Cambridge
     5 
     5 
     6 Theory of events for security protocols
     6 Theory of events for security protocols
     7 
     7 
     8 Datatype of events; function "sees"; freshness
     8 Datatype of events; function "sees"; freshness
       
     9 
       
    10 "lost" agents have been broken by the Spy; their private keys and internal
       
    11     stores are visible to him
     9 *)
    12 *)
    10 
    13 
    11 Event = Message + List + 
    14 Event = Message + List + 
    12 
    15 
    13 consts  (*Initial states of agents -- parameter of the construction*)
    16 consts  (*Initial states of agents -- parameter of the construction*)
    16 datatype  (*Messages--could add another constructor for agent knowledge*)
    19 datatype  (*Messages--could add another constructor for agent knowledge*)
    17   event = Says  agent agent msg
    20   event = Says  agent agent msg
    18         | Notes agent       msg
    21         | Notes agent       msg
    19 
    22 
    20 consts  
    23 consts  
    21   sees1 :: [agent, event] => msg set
    24   lost :: agent set        (*compromised agents*)
    22 
       
    23 primrec sees1 event
       
    24            (*Spy reads all traffic whether addressed to him or not*)
       
    25   sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
       
    26   sees1_Notes "sees1 A (Notes A' X)   = (if A = A'    then {X} else {})"
       
    27 
       
    28 consts  
       
    29   lost :: agent set        (*agents whose private keys have been compromised*)
       
    30   sees :: [agent, event list] => msg set
    25   sees :: [agent, event list] => msg set
    31 
    26 
    32 rules
    27 rules
    33   (*Spy has access to his own key for spoof messages, but Server is secure*)
    28   (*Spy has access to his own key for spoof messages, but Server is secure*)
    34   Spy_in_lost     "Spy: lost"
    29   Spy_in_lost     "Spy: lost"
    35   Server_not_lost "Server ~: lost"
    30   Server_not_lost "Server ~: lost"
       
    31 
       
    32 consts  
       
    33   sees1 :: [agent, event] => msg set
       
    34 
       
    35 primrec sees1 event
       
    36            (*Spy reads all traffic whether addressed to him or not*)
       
    37   sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
       
    38   sees1_Notes "sees1 A (Notes A' X)   = (if A=A' | A=Spy & A':lost then {X}
       
    39 					 else {})"
    36 
    40 
    37 primrec sees list
    41 primrec sees list
    38   sees_Nil  "sees A []       = initState A"
    42   sees_Nil  "sees A []       = initState A"
    39   sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
    43   sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"
    40 
    44