src/HOL/Auth/Recur.thy
author paulson
Tue Nov 11 11:16:18 1997 +0100 (1997-11-11)
changeset 4198 c63639beeff1
parent 3683 aafe719dff14
child 4552 bb8ff763c93d
permissions -rw-r--r--
Fixed spelling error
     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     One  "[| A ~= Server;  Key KAB ~: used evs |]
    20           ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, Agent Server|}, 
    21                {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, Agent Server|},
    22                KAB)   : respond evs"
    23 
    24     (*The most recent session key is passed up to the caller*)
    25     Cons "[| (PA, RA, KAB) : respond evs;  
    26              Key KBC ~: used evs;  Key KBC ~: parts {RA};
    27              PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|};
    28              B ~= Server |]
    29           ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, 
    30                {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
    31                  Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
    32                  RA|},
    33                KBC)
    34               : respond evs"
    35 
    36 
    37 (*Induction over "respond" can be difficult due to the complexity of the
    38   subgoals.  Set "responses" captures the general form of certificates.
    39 *)
    40 consts     responses :: event list => msg set
    41 inductive "responses evs"       
    42   intrs
    43     (*Server terminates lists*)
    44     Nil  "Agent Server : responses evs"
    45 
    46     Cons "[| RA : responses evs;  Key KAB ~: used evs |]
    47           ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
    48                 RA|}  : responses evs"
    49 
    50 
    51 consts     recur   :: event list set
    52 inductive "recur"
    53   intrs 
    54          (*Initial trace is empty*)
    55     Nil  "[]: recur"
    56 
    57          (*The spy MAY say anything he CAN say.  Common to
    58            all similar protocols.*)
    59     Fake "[| evs: recur;  B ~= Spy;  
    60              X: synth (analz (spies evs)) |]
    61           ==> Says Spy B X  # evs : recur"
    62 
    63          (*Alice initiates a protocol run.
    64            "Agent Server" is just a placeholder, to terminate the nesting.*)
    65     RA1  "[| evs1: recur;  A ~= B;  A ~= Server;  Nonce NA ~: used evs1 |]
    66           ==> Says A B 
    67                 (Hash[Key(shrK A)] 
    68                  {|Agent A, Agent B, Nonce NA, Agent Server|})
    69               # evs1 : recur"
    70 
    71          (*Bob's response to Alice's message.  C might be the Server.
    72            XA should be the Hash of the remaining components with KA, but
    73                 Bob cannot check that.
    74            P is the previous recur message from Alice's caller.
    75            NOTE: existing proofs don't need PA and are complicated by its
    76                 presence!  See parts_Fake_tac.*)
    77     RA2  "[| evs2: recur;  B ~= C;  B ~= Server;  Nonce NB ~: used evs2;
    78              Says A' B PA : set evs2;  
    79              PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
    80           ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
    81               # evs2 : recur"
    82 
    83          (*The Server receives Bob's message and prepares a response.*)
    84     RA3  "[| evs3: recur;  B ~= Server;
    85              Says B' Server PB : set evs3;
    86              (PB,RB,K) : respond evs3 |]
    87           ==> Says Server B RB # evs3 : recur"
    88 
    89          (*Bob receives the returned message and compares the Nonces with
    90            those in the message he previously sent the Server.*)
    91     RA4  "[| evs4: recur;  A ~= B;  
    92              Says B  C {|XH, Agent B, Agent C, Nonce NB, 
    93                          XA, Agent A, Agent B, Nonce NA, P|} : set evs4;
    94              Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
    95                          Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
    96                          RA|} : set evs4 |]
    97           ==> Says B A RA # evs4 : recur"
    98 
    99 (**No "oops" message can easily be expressed.  Each session key is
   100    associated--in two separate messages--with two nonces.
   101 ***)
   102 end