src/HOL/Auth/Recur.thy
author paulson
Fri Jul 04 17:34:55 1997 +0200 (1997-07-04)
changeset 3500 0d8ad2f192d8
parent 3466 30791e5a69c4
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
New constant "certificate"--just an abbreviation
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@2449
    11
(*Two session keys are distributed to each agent except for the initiator,
paulson@2516
    12
        who receives one.
paulson@2449
    13
  Perhaps the two session keys could be bundled into a single message.
paulson@2449
    14
*)
paulson@2516
    15
consts     respond :: "event list => (msg*msg*key)set"
paulson@2516
    16
inductive "respond evs" (*Server's response to the nested message*)
paulson@2449
    17
  intrs
paulson@2449
    18
    (*The message "Agent Server" marks the end of a list.*)
paulson@2516
    19
    One  "[| A ~= Server;  Key KAB ~: used evs |]
paulson@2532
    20
          ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, Agent Server|}, 
paulson@2516
    21
               {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, Agent Server|},
paulson@2516
    22
               KAB)   : respond evs"
paulson@2449
    23
paulson@2532
    24
    (*The most recent session key is passed up to the caller*)
paulson@2516
    25
    Cons "[| (PA, RA, KAB) : respond evs;  
paulson@2516
    26
             Key KBC ~: used evs;  Key KBC ~: parts {RA};
paulson@2516
    27
             PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|};
paulson@2481
    28
             B ~= Server |]
paulson@2516
    29
          ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, 
paulson@2550
    30
               {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
paulson@2550
    31
                 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
paulson@2516
    32
                 RA|},
paulson@2516
    33
               KBC)
paulson@2516
    34
              : respond evs"
paulson@2449
    35
paulson@2449
    36
paulson@2481
    37
(*Induction over "respond" can be difficult due to the complexity of the
paulson@2532
    38
  subgoals.  Set "responses" captures the general form of certificates.
paulson@2449
    39
*)
paulson@2516
    40
consts     responses :: event list => msg set
paulson@2516
    41
inductive "responses evs"       
paulson@2449
    42
  intrs
paulson@2449
    43
    (*Server terminates lists*)
paulson@2516
    44
    Nil  "Agent Server : responses evs"
paulson@2449
    45
paulson@2516
    46
    Cons "[| RA : responses evs;  Key KAB ~: used evs |]
paulson@2516
    47
          ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
paulson@2516
    48
                RA|}  : responses evs"
paulson@2449
    49
paulson@2449
    50
paulson@2449
    51
consts     recur   :: agent set => event list set
paulson@2449
    52
inductive "recur lost"
paulson@2449
    53
  intrs 
paulson@2449
    54
         (*Initial trace is empty*)
paulson@2449
    55
    Nil  "[]: recur lost"
paulson@2449
    56
paulson@2532
    57
         (*The spy MAY say anything he CAN say.  Common to
paulson@2449
    58
           all similar protocols.*)
paulson@2449
    59
    Fake "[| evs: recur lost;  B ~= Spy;  
paulson@2449
    60
             X: synth (analz (sees lost Spy evs)) |]
paulson@2449
    61
          ==> Says Spy B X  # evs : recur lost"
paulson@2449
    62
paulson@2449
    63
         (*Alice initiates a protocol run.
paulson@2449
    64
           "Agent Server" is just a placeholder, to terminate the nesting.*)
paulson@2516
    65
    RA1  "[| evs: recur lost;  A ~= B;  A ~= Server;  Nonce NA ~: used evs |]
paulson@2481
    66
          ==> Says A B 
paulson@2516
    67
                (Hash[Key(shrK A)] 
paulson@2516
    68
                 {|Agent A, Agent B, Nonce NA, Agent Server|})
paulson@2481
    69
              # evs : recur lost"
paulson@2449
    70
paulson@2449
    71
         (*Bob's response to Alice's message.  C might be the Server.
paulson@2449
    72
           XA should be the Hash of the remaining components with KA, but
paulson@2516
    73
                Bob cannot check that.
paulson@2485
    74
           P is the previous recur message from Alice's caller.
paulson@2485
    75
           NOTE: existing proofs don't need PA and are complicated by its
paulson@2516
    76
                presence!  See parts_Fake_tac.*)
paulson@2516
    77
    RA2  "[| evs: recur lost;  B ~= C;  B ~= Server;  Nonce NB ~: used evs;
nipkow@3465
    78
             Says A' B PA : set evs;  
paulson@2481
    79
             PA = {|XA, Agent A, Agent B, Nonce NA, P|} |]
paulson@2516
    80
          ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
paulson@2481
    81
              # evs : recur lost"
paulson@2449
    82
paulson@2550
    83
         (*The Server receives Bob's message and prepares a response.*)
paulson@2451
    84
    RA3  "[| evs: recur lost;  B ~= Server;
nipkow@3465
    85
             Says B' Server PB : set evs;
paulson@2516
    86
             (PB,RB,K) : respond evs |]
paulson@2449
    87
          ==> Says Server B RB # evs : recur lost"
paulson@2449
    88
paulson@2449
    89
         (*Bob receives the returned message and compares the Nonces with
paulson@2516
    90
           those in the message he previously sent the Server.*)
paulson@2451
    91
    RA4  "[| evs: recur lost;  A ~= B;  
paulson@2449
    92
             Says B  C {|XH, Agent B, Agent C, Nonce NB, 
paulson@3466
    93
                         XA, Agent A, Agent B, Nonce NA, P|} : set evs;
paulson@2550
    94
             Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, 
paulson@2550
    95
                         Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
paulson@3466
    96
                         RA|} : set evs |]
paulson@2449
    97
          ==> Says B A RA # evs : recur lost"
paulson@2449
    98
paulson@3466
    99
(**No "oops" message can easily be expressed.  Each session key is
paulson@2449
   100
   associated--in two separate messages--with two nonces.
paulson@2449
   101
***)
paulson@2449
   102
end