--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/Recur.thy Wed Dec 18 17:46:38 1996 +0100
@@ -0,0 +1,117 @@
+(* Title: HOL/Auth/Recur
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+
+Inductive relation "recur" for the Recursive Authentication protocol.
+*)
+
+Recur = Shared +
+
+syntax
+ newK2 :: "nat*nat => key"
+
+translations
+ "newK2 x" == "newK(nPair x)"
+
+(*Two session keys are distributed to each agent except for the initiator,
+ who receives one.
+ Perhaps the two session keys could be bundled into a single message.
+*)
+consts respond :: "nat => (nat*msg*msg)set"
+inductive "respond i" (*Server's response to the nested message*)
+ intrs
+ (*The message "Agent Server" marks the end of a list.*)
+
+ One "[| A ~= Server;
+ MA = {|Agent A, Agent B, Nonce NA, Agent Server|} |]
+ ==> (j, {|Hash{|Key(shrK A), MA|}, MA|},
+ {|Agent A,
+ Crypt (shrK A) {|Key(newK2(i,j)), Agent B, Nonce NA|},
+ Agent Server|})
+ : respond i"
+
+ (*newK2(i,Suc j) is the key for A & B; newK2(i,j) is the key for B & C*)
+ Cons "[| (Suc j, PA, RA) : respond i;
+ B ~= Server;
+ MB = {|Agent B, Agent C, Nonce NB, PA|};
+ PA = {|Hash{|Key(shrK A), MA|}, MA|};
+ MA = {|Agent A, Agent B, Nonce NA, P|} |]
+ ==> (j, {|Hash{|Key(shrK B), MB|}, MB|},
+ {|Agent B,
+ Crypt (shrK B) {|Key(newK2(i,Suc j)), Agent A, Nonce NB|},
+ Agent B,
+ Crypt (shrK B) {|Key(newK2(i,j)), Agent C, Nonce NB|},
+ RA|})
+ : respond i"
+
+
+(*Induction over "respond" can be difficult, due to the complexity of the
+ subgoals. The "responses" relation formalizes the general form of its
+ third component.
+*)
+consts responses :: nat => msg set
+inductive "responses i"
+ intrs
+ (*Server terminates lists*)
+ Nil "Agent Server : responses i"
+
+ Cons "RA : responses i
+ ==> {|Agent B,
+ Crypt (shrK B) {|Key(newK2(i,k)), Agent A, Nonce NB|},
+ RA|} : responses i"
+
+
+consts recur :: agent set => event list set
+inductive "recur lost"
+ intrs
+ (*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
+ all similar protocols.*)
+ Fake "[| evs: recur lost; B ~= Spy;
+ X: synth (analz (sees lost Spy evs)) |]
+ ==> Says Spy B X # evs : recur lost"
+
+ (*Alice initiates a protocol run.
+ "Agent Server" is just a placeholder, to terminate the nesting.*)
+ NA1 "[| evs: recur lost; A ~= B; A ~= Server;
+ MA = {|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|}|]
+ ==> Says A B {|Hash{|Key(shrK A),MA|}, MA|} # evs : recur lost"
+
+ (*Bob's response to Alice's message. C might be the Server.
+ XA should be the Hash of the remaining components with KA, but
+ Bob cannot check that.
+ P is the previous recur message from Alice's caller.*)
+ NA2 "[| evs: recur lost; B ~= C; B ~= Server;
+ Says A' B PA : set_of_list evs;
+ PA = {|XA, Agent A, Agent B, Nonce NA, P|};
+ MB = {|Agent B, Agent C, Nonce (newN(length evs)), PA|} |]
+ ==> Says B C {|Hash{|Key(shrK B),MB|}, MB|} # evs : recur lost"
+
+ (*The Server receives and decodes Bob's message. Then he generates
+ a new session key and a response.*)
+ NA3 "[| evs: recur lost; B ~= Server;
+ Says B' Server PB : set_of_list evs;
+ (0,PB,RB) : respond (length evs) |]
+ ==> Says Server B RB # evs : recur lost"
+
+ (*Bob receives the returned message and compares the Nonces with
+ those in the message he previously sent the Server.*)
+ NA4 "[| evs: recur lost; A ~= B;
+ Says C' B {|Agent B,
+ Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
+ Agent B,
+ Crypt (shrK B) {|Key KAC, Agent C, Nonce NB|}, RA|}
+ : set_of_list evs;
+ Says B C {|XH, Agent B, Agent C, Nonce NB,
+ XA, Agent A, Agent B, Nonce NA, P|}
+ : set_of_list evs |]
+ ==> Says B A RA # evs : recur lost"
+
+(**No "oops" message can readily be expressed, since each session key is
+ associated--in two separate messages--with two nonces.
+***)
+end