src/HOL/Auth/Event.thy
changeset 2032 1bbf1bdcaf56
parent 1942 6c9c1a42a869
     1.1 --- a/src/HOL/Auth/Event.thy	Thu Sep 26 12:47:47 1996 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Thu Sep 26 12:50:48 1996 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4          (*Server knows all keys; other agents know only their own*)
     1.5    initState_Server  "initState Server     = Key `` range shrK"
     1.6    initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
     1.7 -  initState_Enemy   "initState Enemy  = {Key (shrK Enemy)}"
     1.8 +  initState_Spy   "initState Spy  = {Key (shrK Spy)}"
     1.9  
    1.10  (**
    1.11  For asymmetric keys: server knows all public and private keys,
    1.12 @@ -45,7 +45,7 @@
    1.13  primrec sees1 event
    1.14             (*First agent recalls all that it says, but NOT everything
    1.15               that is sent to it; it must note such things if/when received*)
    1.16 -  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Enemy} then {X} else {})"
    1.17 +  sees1_Says  "sees1 A (Says A' B X)  = (if A:{A',Spy} then {X} else {})"
    1.18            (*part of A's internal state*)
    1.19    sees1_Notes "sees1 A (Notes A' X)   = (if A=A' then {X} else {})"
    1.20  
    1.21 @@ -89,11 +89,11 @@
    1.22           (*Initial trace is empty*)
    1.23      Nil  "[]: traces"
    1.24  
    1.25 -         (*The enemy MAY say anything he CAN say.  We do not expect him to
    1.26 +         (*The spy MAY say anything he CAN say.  We do not expect him to
    1.27             invent new nonces here, but he can also use NS1.  Common to
    1.28             all similar protocols.*)
    1.29 -    Fake "[| evs: traces;  B ~= Enemy;  X: synth (analz (sees Enemy evs))
    1.30 -          |] ==> (Says Enemy B X) # evs : traces"
    1.31 +    Fake "[| evs: traces;  B ~= Spy;  X: synth (analz (sees Spy evs))
    1.32 +          |] ==> (Says Spy B X) # evs : traces"
    1.33  
    1.34           (*Alice initiates a protocol run*)
    1.35      NS1  "[| evs: traces;  A ~= Server
    1.36 @@ -112,7 +112,7 @@
    1.37                     (shrK A))) # evs : traces"
    1.38  
    1.39            (*We can't assume S=Server.  Agent A "remembers" her nonce.
    1.40 -            May assume WLOG that she is NOT the Enemy: the Fake rule
    1.41 +            May assume WLOG that she is NOT the Spy: the Fake rule
    1.42              covers this case.  Can inductively show A ~= Server*)
    1.43      NS3  "[| evs: traces;  A ~= B;
    1.44               (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)))