src/HOL/Auth/Recur.thy
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 5434 9b4bed3f394c
child 11185 1b737b4c2108
permissions -rw-r--r--
tidied; added lemma restrict_to_left
paulson@2449
     1
(*  Title:      HOL/Auth/Recur
paulson@2449
     2
    ID:         $Id$
paulson@2449
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2449
     4
    Copyright   1996  University of Cambridge
paulson@2449
     5
paulson@2449
     6
Inductive relation "recur" for the Recursive Authentication protocol.
paulson@2449
     7
*)
paulson@2449
     8
paulson@2485
     9
Recur = Shared +
paulson@2449
    10
paulson@5434
    11
(*End marker for message bundles*)
paulson@5434
    12
syntax        END :: msg
paulson@5434
    13
translations "END" == "Number 0"
paulson@5434
    14
paulson@2449
    15
(*Two session keys are distributed to each agent except for the initiator,
paulson@2516
    16
        who receives one.
paulson@2449
    17
  Perhaps the two session keys could be bundled into a single message.
paulson@2449
    18
*)
paulson@2516
    19
consts     respond :: "event list => (msg*msg*key)set"
paulson@2516
    20
inductive "respond evs" (*Server's response to the nested message*)
paulson@2449
    21
  intrs
paulson@5434
    22
    One  "[| Key KAB ~: used evs |]
paulson@5434
    23
          ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|}, 
paulson@5434
    24
               {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, END|},
paulson@2516
    25
               KAB)   : respond evs"
paulson@2449
    26
paulson@2532
    27
    (*The most recent session key is passed up to the caller*)
paulson@2516
    28
    Cons "[| (PA, RA, KAB) : respond evs;  
paulson@2516
    29
             Key KBC ~: used evs;  Key KBC ~: parts {RA};
paulson@5434
    30
             PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} |]
paulson@2516
    31
          ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, 
paulson@2550
    32
               {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
paulson@2550
    33
                 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
paulson@2516
    34
                 RA|},
paulson@2516
    35
               KBC)
paulson@2516
    36
              : respond evs"
paulson@2449
    37
paulson@2449
    38
paulson@2481
    39
(*Induction over "respond" can be difficult due to the complexity of the
paulson@2532
    40
  subgoals.  Set "responses" captures the general form of certificates.
paulson@2449
    41
*)
paulson@2516
    42
consts     responses :: event list => msg set
paulson@2516
    43
inductive "responses evs"       
paulson@2449
    44
  intrs
paulson@2449
    45
    (*Server terminates lists*)
paulson@5434
    46
    Nil  "END : responses evs"
paulson@2449
    47
paulson@2516
    48
    Cons "[| RA : responses evs;  Key KAB ~: used evs |]
paulson@2516
    49
          ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
paulson@2516
    50
                RA|}  : responses evs"
paulson@2449
    51
paulson@2449
    52
paulson@3519
    53
consts     recur   :: event list set
paulson@3519
    54
inductive "recur"
paulson@2449
    55
  intrs 
paulson@2449
    56
         (*Initial trace is empty*)
paulson@3519
    57
    Nil  "[]: recur"
paulson@2449
    58
paulson@2532
    59
         (*The spy MAY say anything he CAN say.  Common to
paulson@2449
    60
           all similar protocols.*)
paulson@5434
    61
    Fake "[| evs: recur;  X: synth (analz (spies evs)) |]
paulson@3519
    62
          ==> Says Spy B X  # evs : recur"
paulson@2449
    63
paulson@2449
    64
         (*Alice initiates a protocol run.
paulson@5434
    65
           END is a placeholder to terminate the nesting.*)
paulson@5434
    66
    RA1  "[| evs1: recur;  Nonce NA ~: used evs1 |]
paulson@5434
    67
          ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|})
paulson@3659
    68
              # evs1 : recur"
paulson@2449
    69
paulson@2449
    70
         (*Bob's response to Alice's message.  C might be the Server.
paulson@4552
    71
           We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because
paulson@4552
    72
           it complicates proofs, so B may respond to any message at all!*)
paulson@5434
    73
    RA2  "[| evs2: recur;  Nonce NB ~: used evs2;
paulson@4552
    74
             Says A' B PA : set evs2 |]
paulson@2516
    75
          ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
paulson@3659
    76
              # evs2 : recur"
paulson@2449
    77
paulson@2550
    78
         (*The Server receives Bob's message and prepares a response.*)
paulson@5434
    79
    RA3  "[| evs3: recur;  Says B' Server PB : set evs3;
paulson@3659
    80
             (PB,RB,K) : respond evs3 |]
paulson@3659
    81
          ==> Says Server B RB # evs3 : recur"
paulson@2449
    82
paulson@2449
    83
         (*Bob receives the returned message and compares the Nonces with
paulson@2516
    84
           those in the message he previously sent the Server.*)
paulson@5434
    85
    RA4  "[| evs4: recur;  
paulson@2449
    86
             Says B  C {|XH, Agent B, Agent C, Nonce NB, 
paulson@3659
    87
                         XA, Agent A, Agent B, Nonce NA, P|} : set evs4;
paulson@2550
    88
             Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
paulson@2550
    89
                         Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
paulson@3659
    90
                         RA|} : set evs4 |]
paulson@3659
    91
          ==> Says B A RA # evs4 : recur"
paulson@2449
    92
paulson@2449
    93
end
paulson@5359
    94
paulson@5359
    95
   (*No "oops" message can easily be expressed.  Each session key is
paulson@5359
    96
     associated--in two separate messages--with two nonces.  This is 
paulson@5359
    97
     one try, but it isn't that useful.  Re domino attack, note that
paulson@5359
    98
     Recur.ML proves that each session key is secure provided the two
paulson@5359
    99
     peers are, even if there are compromised agents elsewhere in
paulson@5359
   100
     the chain.  Oops cases proved using parts_cut, Key_in_keysFor_parts,
paulson@5359
   101
     etc.
paulson@5359
   102
paulson@5359
   103
    Oops  "[| evso: recur;  Says Server B RB : set evso;
paulson@5359
   104
	      RB : responses evs';  Key K : parts {RB} |]
paulson@5359
   105
           ==> Notes Spy {|Key K, RB|} # evso : recur"
paulson@5359
   106
  *)