src/HOL/Auth/Event.thy
changeset 3678 414e04d7c2d6
parent 3519 ab0a9fbed4c0
child 3683 aafe719dff14
     1.1 --- a/src/HOL/Auth/Event.thy	Wed Sep 17 16:37:21 1997 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Wed Sep 17 16:37:27 1997 +0200
     1.3 @@ -6,6 +6,9 @@
     1.4  Theory of events for security protocols
     1.5  
     1.6  Datatype of events; function "sees"; freshness
     1.7 +
     1.8 +"lost" agents have been broken by the Spy; their private keys and internal
     1.9 +    stores are visible to him
    1.10  *)
    1.11  
    1.12  Event = Message + List + 
    1.13 @@ -18,15 +21,7 @@
    1.14          | Notes agent       msg
    1.15  
    1.16  consts  
    1.17 -  sees1 :: [agent, event] => msg set
    1.18 -
    1.19 -primrec sees1 event
    1.20 -           (*Spy reads all traffic whether addressed to him or not*)
    1.21 -  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
    1.22 -  sees1_Notes "sees1 A (Notes A' X)   = (if A = A'    then {X} else {})"
    1.23 -
    1.24 -consts  
    1.25 -  lost :: agent set        (*agents whose private keys have been compromised*)
    1.26 +  lost :: agent set        (*compromised agents*)
    1.27    sees :: [agent, event list] => msg set
    1.28  
    1.29  rules
    1.30 @@ -34,6 +29,15 @@
    1.31    Spy_in_lost     "Spy: lost"
    1.32    Server_not_lost "Server ~: lost"
    1.33  
    1.34 +consts  
    1.35 +  sees1 :: [agent, event] => msg set
    1.36 +
    1.37 +primrec sees1 event
    1.38 +           (*Spy reads all traffic whether addressed to him or not*)
    1.39 +  sees1_Says  "sees1 A (Says A' B X)  = (if A:{B,Spy} then {X} else {})"
    1.40 +  sees1_Notes "sees1 A (Notes A' X)   = (if A=A' | A=Spy & A':lost then {X}
    1.41 +					 else {})"
    1.42 +
    1.43  primrec sees list
    1.44    sees_Nil  "sees A []       = initState A"
    1.45    sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs"