src/HOL/Auth/NS_Shared.thy
changeset 1965 789c12ea0b30
parent 1943 20574dca5a3e
child 1976 1cff1f4fdb8a
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Mon Sep 09 17:34:24 1996 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Mon Sep 09 17:44:20 1996 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4      Fake "[| evs: ns_shared;  B ~= Enemy;  X: synth (analz (sees Enemy evs))
     1.5            |] ==> Says Enemy B X # evs : ns_shared"
     1.6  
     1.7 -         (*Alice initiates a protocol run*)
     1.8 +         (*Alice initiates a protocol run, requesting to talk to any B*)
     1.9      NS1  "[| evs: ns_shared;  A ~= Server
    1.10            |] ==> Says A Server {|Agent A, Agent B, Nonce (newN evs)|} # evs
    1.11                   : ns_shared"