src/HOL/Auth/Shared.thy
changeset 1967 0ff58b41c037
parent 1965 789c12ea0b30
child 2012 1b234f1fd9c7
     1.1 --- a/src/HOL/Auth/Shared.thy	Mon Sep 09 18:53:41 1996 +0200
     1.2 +++ b/src/HOL/Auth/Shared.thy	Mon Sep 09 18:58:02 1996 +0200
     1.3 @@ -16,6 +16,9 @@
     1.4    shrK    :: agent => key  (*symmetric keys*)
     1.5    leaked  :: nat set       (*Friendly agents whose keys have leaked to Enemy*)
     1.6  
     1.7 +constdefs     (*Enemy and compromised agents*)
     1.8 +  bad     :: agent set     "bad == insert Enemy (Friend``leaked)"
     1.9 +
    1.10  rules
    1.11    isSym_shrK "isSymKey (shrK A)"
    1.12  
    1.13 @@ -26,8 +29,7 @@
    1.14          (*Server knows all keys; other agents know only their own*)
    1.15    initState_Server  "initState Server     = Key `` range shrK"
    1.16    initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
    1.17 -  initState_Enemy
    1.18 -    "initState Enemy = insert (Key (shrK Enemy)) (Key``shrK``Friend``leaked)"
    1.19 +  initState_Enemy   "initState Enemy      = Key``shrK``bad"
    1.20  
    1.21  datatype  (*Messages, and components of agent stores*)
    1.22    event = Says agent agent msg