src/HOL/Auth/Recur.thy
changeset 2449 d30ad12b1397
child 2451 ce85a2aafc7a
--- /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