src/HOL/Auth/Recur.thy

Now with Andy Gordon's treatment of freshness to replace newN/K

(*  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 +

(*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 :: "event list => (msg*msg*key)set"
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|}, 
               {|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*)
    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|};
             B ~= Server |]
          ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, 
               {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
                 Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
                 RA|},
               KBC)
              : respond evs"


(*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 :: event list => msg set
inductive "responses evs"       
  intrs
    (*Server terminates lists*)
    Nil  "Agent Server : responses evs"

    Cons "[| RA : responses evs;  Key KAB ~: used evs |]
          ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
                RA|}  : responses evs"


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.*)
    RA1  "[| evs: recur lost;  A ~= B;  A ~= Server;  Nonce NA ~: used evs |]
          ==> Says A B 
                (Hash[Key(shrK A)] 
                 {|Agent A, Agent B, Nonce NA, Agent Server|})
              # 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.
           NOTE: existing proofs don't need PA and are complicated by its
                presence!  See parts_Fake_tac.*)
    RA2  "[| evs: recur lost;  B ~= C;  B ~= Server;  Nonce NB ~: used evs;
             Says A' B PA : set_of_list evs;  
             PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
          ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
              # evs : recur lost"

         (*The Server receives and decodes Bob's message.  Then he generates
           a new session key and a response.*)
    RA3  "[| evs: recur lost;  B ~= Server;
             Says B' Server PB : set_of_list evs;
             (PB,RB,K) : respond 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.*)
    RA4  "[| evs: recur lost;  A ~= B;  
             Says C' B {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
                         Crypt (shrK B) {|Key KBC, 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