src/HOL/Auth/Shared.thy
changeset 1965 789c12ea0b30
parent 1943 20574dca5a3e
child 1967 0ff58b41c037
     1.1 --- a/src/HOL/Auth/Shared.thy	Mon Sep 09 17:34:24 1996 +0200
     1.2 +++ b/src/HOL/Auth/Shared.thy	Mon Sep 09 17:44:20 1996 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4  
     1.5  consts
     1.6    shrK    :: agent => key  (*symmetric keys*)
     1.7 +  leaked  :: nat set       (*Friendly agents whose keys have leaked to Enemy*)
     1.8  
     1.9  rules
    1.10    isSym_shrK "isSymKey (shrK A)"
    1.11 @@ -25,7 +26,8 @@
    1.12          (*Server knows all keys; other agents know only their own*)
    1.13    initState_Server  "initState Server     = Key `` range shrK"
    1.14    initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
    1.15 -  initState_Enemy   "initState Enemy  = {Key (shrK Enemy)}"
    1.16 +  initState_Enemy
    1.17 +    "initState Enemy = insert (Key (shrK Enemy)) (Key``shrK``Friend``leaked)"
    1.18  
    1.19  datatype  (*Messages, and components of agent stores*)
    1.20    event = Says agent agent msg