author nipkow
Thu, 26 Jun 1997 13:20:50 +0200
changeset 3465 e85c24717cad
parent 2550 8d8344bcf98a
child 3466 30791e5a69c4
permissions -rw-r--r--
set_of_list -> set

(*  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*)
    (*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"

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

(*Induction over "respond" can be difficult due to the complexity of the
  subgoals.  Set "responses" captures the general form of certificates.
consts     responses :: event list => msg set
inductive "responses evs"       
    (*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"
         (*Initial trace is empty*)
    Nil  "[]: recur lost"

         (*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)) |]
          ==> 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 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 Bob's message and prepares a response.*)
    RA3  "[| evs: recur lost;  B ~= Server;
             Says B' Server PB : set 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 B  C {|XH, Agent B, Agent C, Nonce NB, 
                         XA, Agent A, Agent B, Nonce NA, P|} 
               : set evs;
             Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
                         Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
               : set 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.