1.1 --- a/src/HOL/Auth/Event.thy	Tue Sep 03 16:43:31 1996 +0200
     1.2 +++ b/src/HOL/Auth/Event.thy	Tue Sep 03 17:54:39 1996 +0200
     1.3 @@ -16,19 +16,19 @@
     1.4  
     1.5  consts
     1.6    publicKey    :: agent => key
     1.7 -  serverKey    :: agent => key  (*symmetric keys*)
     1.8 +  shrK    :: agent => key  (*symmetric keys*)
     1.9  
    1.10  rules
    1.11 -  isSym_serverKey "isSymKey (serverKey A)"
    1.12 +  isSym_shrK "isSymKey (shrK A)"
    1.13  
    1.14  consts  (*Initial states of agents -- parameter of the construction*)
    1.15    initState :: agent => msg set
    1.16  
    1.17  primrec initState agent
    1.18          (*Server knows all keys; other agents know only their own*)
    1.19 -  initState_Server  "initState Server     = Key `` range serverKey"
    1.20 -  initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
    1.21 -  initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
    1.22 +  initState_Server  "initState Server     = Key `` range shrK"
    1.23 +  initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
    1.24 +  initState_Enemy   "initState Enemy  = {Key (shrK Enemy)}"
    1.25  
    1.26  (**
    1.27  For asymmetric keys: server knows all public and private keys,
    1.28 @@ -72,7 +72,7 @@
    1.29    newK :: "event list => key"
    1.30  
    1.31  rules
    1.32 -  inj_serverKey "inj serverKey"
    1.33 +  inj_shrK "inj shrK"
    1.34  
    1.35    inj_newN   "inj(newN)"
    1.36    fresh_newN "Nonce (newN evs) ~: parts (initState B)" 
    1.37 @@ -108,14 +108,14 @@
    1.38               (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    1.39            |] ==> (Says Server A 
    1.40                    (Crypt {|Nonce NA, Agent B, Key (newK evs),   
    1.41 -                           (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
    1.42 -                   (serverKey A))) # evs : traces"
    1.43 +                           (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
    1.44 +                   (shrK A))) # evs : traces"
    1.45  
    1.46            (*We can't assume S=Server.  Agent A "remembers" her nonce.
    1.47              May assume WLOG that she is NOT the Enemy: the Fake rule
    1.48              covers this case.  Can inductively show A ~= Server*)
    1.49      NS3  "[| evs: traces;  A ~= B;
    1.50 -             (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
    1.51 +             (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))) 
    1.52                 : set_of_list evs;
    1.53               A = Friend i;
    1.54               (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
    1.55 @@ -124,14 +124,14 @@
    1.56           (*Bob's nonce exchange.  He does not know who the message came
    1.57             from, but responds to A because she is mentioned inside.*)
    1.58      NS4  "[| evs: traces;  A ~= B;  
    1.59 -             (Says A' B (Crypt {|Key K, Agent A|} (serverKey B))) 
    1.60 +             (Says A' B (Crypt {|Key K, Agent A|} (shrK B))) 
    1.61                 : set_of_list evs
    1.62            |] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : traces"
    1.63  
    1.64           (*Alice responds with (Suc N), if she has seen the key before.*)
    1.65      NS5  "[| evs: traces;  A ~= B;  
    1.66               (Says B' A (Crypt (Nonce N) K)) : set_of_list evs;
    1.67 -             (Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
    1.68 +             (Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))) 
    1.69                 : set_of_list evs
    1.70            |] ==> (Says A B (Crypt (Nonce (Suc N)) K)) # evs : traces"
    1.71