--- 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"