--- a/src/HOL/Auth/Recur.thy Mon Jan 20 18:29:26 1997 +0100
+++ b/src/HOL/Auth/Recur.thy Tue Jan 21 10:54:05 1997 +0100
@@ -16,14 +16,12 @@
inductive "respond evs" (*Server's response to the nested message*)
intrs
(*The message "Agent Server" marks the end of a list.*)
-
One "[| A ~= Server; Key KAB ~: used evs |]
- ==> (Hash[Key(shrK A)]
- {|Agent A, Agent B, Nonce NA, Agent Server|},
+ ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, Agent Server|},
{|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, Agent Server|},
KAB) : respond evs"
- (*newK2(i,Suc j) is the key for A & B; newK2(i,j) is the key for B & C*)
+ (*The most recent session key is passed up to the caller*)
Cons "[| (PA, RA, KAB) : respond evs;
Key KBC ~: used evs; Key KBC ~: parts {RA};
PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|};
@@ -37,8 +35,7 @@
(*Induction over "respond" can be difficult due to the complexity of the
- subgoals. The "responses" relation formalizes the general form of its
- third component.
+ subgoals. Set "responses" captures the general form of certificates.
*)
consts responses :: event list => msg set
inductive "responses evs"
@@ -57,8 +54,7 @@
(*Initial trace is empty*)
Nil "[]: recur lost"
- (*The spy MAY say anything he CAN say. We do not expect him to
- invent new nonces here, but he can also use NS1. Common to
+ (*The spy MAY say anything he CAN say. Common to
all similar protocols.*)
Fake "[| evs: recur lost; B ~= Spy;
X: synth (analz (sees lost Spy evs)) |]