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