src/HOL/Auth/Recur.thy
author paulson
Fri Jan 17 12:49:31 1997 +0100 (1997-01-17)
changeset 2516 4d68fbe6378b
parent 2485 c4368c967c56
child 2532 cde25bf71cc1
permissions -rw-r--r--
Now with Andy Gordon's treatment of freshness to replace newN/K
     1 (*  Title:      HOL/Auth/Recur
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Inductive relation "recur" for the Recursive Authentication protocol.
     7 *)
     8 
     9 Recur = Shared +
    10 
    11 (*Two session keys are distributed to each agent except for the initiator,
    12         who receives one.
    13   Perhaps the two session keys could be bundled into a single message.
    14 *)
    15 consts     respond :: "event list => (msg*msg*key)set"
    16 inductive "respond evs" (*Server's response to the nested message*)
    17   intrs
    18     (*The message "Agent Server" marks the end of a list.*)
    19 
    20     One  "[| A ~= Server;  Key KAB ~: used evs |]
    21           ==> (Hash[Key(shrK A)] 
    22                         {|Agent A, Agent B, Nonce NA, Agent Server|}, 
    23                {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, Agent Server|},
    24                KAB)   : respond evs"
    25 
    26     (*newK2(i,Suc j) is the key for A & B; newK2(i,j) is the key for B & C*)
    27     Cons "[| (PA, RA, KAB) : respond evs;  
    28              Key KBC ~: used evs;  Key KBC ~: parts {RA};
    29              PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|};
    30              B ~= Server |]
    31           ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, 
    32                {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
    33                  Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
    34                  RA|},
    35                KBC)
    36               : respond evs"
    37 
    38 
    39 (*Induction over "respond" can be difficult due to the complexity of the
    40   subgoals.  The "responses" relation formalizes the general form of its
    41   third component.
    42 *)
    43 consts     responses :: event list => msg set
    44 inductive "responses evs"       
    45   intrs
    46     (*Server terminates lists*)
    47     Nil  "Agent Server : responses evs"
    48 
    49     Cons "[| RA : responses evs;  Key KAB ~: used evs |]
    50           ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
    51                 RA|}  : responses evs"
    52 
    53 
    54 consts     recur   :: agent set => event list set
    55 inductive "recur lost"
    56   intrs 
    57          (*Initial trace is empty*)
    58     Nil  "[]: recur lost"
    59 
    60          (*The spy MAY say anything he CAN say.  We do not expect him to
    61            invent new nonces here, but he can also use NS1.  Common to
    62            all similar protocols.*)
    63     Fake "[| evs: recur lost;  B ~= Spy;  
    64              X: synth (analz (sees lost Spy evs)) |]
    65           ==> Says Spy B X  # evs : recur lost"
    66 
    67          (*Alice initiates a protocol run.
    68            "Agent Server" is just a placeholder, to terminate the nesting.*)
    69     RA1  "[| evs: recur lost;  A ~= B;  A ~= Server;  Nonce NA ~: used evs |]
    70           ==> Says A B 
    71                 (Hash[Key(shrK A)] 
    72                  {|Agent A, Agent B, Nonce NA, Agent Server|})
    73               # evs : recur lost"
    74 
    75          (*Bob's response to Alice's message.  C might be the Server.
    76            XA should be the Hash of the remaining components with KA, but
    77                 Bob cannot check that.
    78            P is the previous recur message from Alice's caller.
    79            NOTE: existing proofs don't need PA and are complicated by its
    80                 presence!  See parts_Fake_tac.*)
    81     RA2  "[| evs: recur lost;  B ~= C;  B ~= Server;  Nonce NB ~: used evs;
    82              Says A' B PA : set_of_list evs;  
    83              PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
    84           ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
    85               # evs : recur lost"
    86 
    87          (*The Server receives and decodes Bob's message.  Then he generates
    88            a new session key and a response.*)
    89     RA3  "[| evs: recur lost;  B ~= Server;
    90              Says B' Server PB : set_of_list evs;
    91              (PB,RB,K) : respond evs |]
    92           ==> Says Server B RB # evs : recur lost"
    93 
    94          (*Bob receives the returned message and compares the Nonces with
    95            those in the message he previously sent the Server.*)
    96     RA4  "[| evs: recur lost;  A ~= B;  
    97              Says C' B {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
    98                          Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, RA|}
    99                : set_of_list evs;
   100              Says B  C {|XH, Agent B, Agent C, Nonce NB, 
   101                          XA, Agent A, Agent B, Nonce NA, P|} 
   102                : set_of_list evs |]
   103           ==> Says B A RA # evs : recur lost"
   104 
   105 (**No "oops" message can readily be expressed, since each session key is
   106    associated--in two separate messages--with two nonces.
   107 ***)
   108 end