src/HOL/Auth/Event.thy

--- a/src/HOL/Auth/Event.thy	Tue Sep 03 16:43:31 1996 +0200
+++ b/src/HOL/Auth/Event.thy	Tue Sep 03 17:54:39 1996 +0200
@@ -16,19 +16,19 @@
 
 consts
   publicKey    :: agent => key
-  serverKey    :: agent => key  (*symmetric keys*)
+  shrK    :: agent => key  (*symmetric keys*)
 
 rules
-  isSym_serverKey "isSymKey (serverKey A)"
+  isSym_shrK "isSymKey (shrK A)"
 
 consts  (*Initial states of agents -- parameter of the construction*)
   initState :: agent => msg set
 
 primrec initState agent
         (*Server knows all keys; other agents know only their own*)
-  initState_Server  "initState Server     = Key `` range serverKey"
-  initState_Friend  "initState (Friend i) = {Key (serverKey (Friend i))}"
-  initState_Enemy   "initState Enemy  = {Key (serverKey Enemy)}"
+  initState_Server  "initState Server     = Key `` range shrK"
+  initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
+  initState_Enemy   "initState Enemy  = {Key (shrK Enemy)}"
 
 (**
 For asymmetric keys: server knows all public and private keys,
@@ -72,7 +72,7 @@
   newK :: "event list => key"
 
 rules
-  inj_serverKey "inj serverKey"
+  inj_shrK "inj shrK"
 
   inj_newN   "inj(newN)"
   fresh_newN "Nonce (newN evs) ~: parts (initState B)" 
@@ -108,14 +108,14 @@
              (Says A' Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
           |] ==> (Says Server A 
                   (Crypt {|Nonce NA, Agent B, Key (newK evs),   
-                           (Crypt {|Key (newK evs), Agent A|} (serverKey B))|}
-                   (serverKey A))) # evs : traces"
+                           (Crypt {|Key (newK evs), Agent A|} (shrK B))|}
+                   (shrK A))) # evs : traces"
 
           (*We can't assume S=Server.  Agent A "remembers" her nonce.
             May assume WLOG that she is NOT the Enemy: the Fake rule
             covers this case.  Can inductively show A ~= Server*)
     NS3  "[| evs: traces;  A ~= B;
-             (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
+             (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))) 
                : set_of_list evs;
              A = Friend i;
              (Says A Server {|Agent A, Agent B, Nonce NA|}) : set_of_list evs
@@ -124,14 +124,14 @@
          (*Bob's nonce exchange.  He does not know who the message came
            from, but responds to A because she is mentioned inside.*)
     NS4  "[| evs: traces;  A ~= B;  
-             (Says A' B (Crypt {|Key K, Agent A|} (serverKey B))) 
+             (Says A' B (Crypt {|Key K, Agent A|} (shrK B))) 
                : set_of_list evs
           |] ==> (Says B A (Crypt (Nonce (newN evs)) K)) # evs : traces"
 
          (*Alice responds with (Suc N), if she has seen the key before.*)
     NS5  "[| evs: traces;  A ~= B;  
              (Says B' A (Crypt (Nonce N) K)) : set_of_list evs;
-             (Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A))) 
+             (Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))) 
                : set_of_list evs
           |] ==> (Says A B (Crypt (Nonce (Suc N)) K)) # evs : traces"