src/HOL/Auth/Recur.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 5434 9b4bed3f394c
child 11185 1b737b4c2108
permissions -rw-r--r--
hide many names from Datatype_Universe.
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
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    11
(*End marker for message bundles*)
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    12
syntax        END :: msg
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    13
translations "END" == "Number 0"
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    14
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    15
(*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
    16
        who receives one.
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    17
  Perhaps the two session keys could be bundled into a single message.
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    18
*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    19
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
    20
inductive "respond evs" (*Server's response to the nested message*)
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    21
  intrs
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    22
    One  "[| Key KAB ~: used evs |]
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    23
          ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|}, 
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    24
               {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, END|},
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    25
               KAB)   : respond evs"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    26
2532
cde25bf71cc1 Improved layout and updated comments
paulson
parents: 2516
diff changeset
    27
    (*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
    28
    Cons "[| (PA, RA, KAB) : respond evs;  
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    29
             Key KBC ~: used evs;  Key KBC ~: parts {RA};
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    30
             PA = Hash[Key(shrK A)] {|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
    31
          ==> (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
    32
               {|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
    33
                 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
    34
                 RA|},
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    35
               KBC)
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    36
              : respond evs"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    37
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    38
2481
ee461c8bc9c3 Now uses HPair
paulson
parents: 2451
diff changeset
    39
(*Induction over "respond" can be difficult due to the complexity of the
2532
cde25bf71cc1 Improved layout and updated comments
paulson
parents: 2516
diff changeset
    40
  subgoals.  Set "responses" captures the general form of certificates.
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    41
*)
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    42
consts     responses :: event list => msg set
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    43
inductive "responses evs"       
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    44
  intrs
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    45
    (*Server terminates lists*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    46
    Nil  "END : responses evs"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    47
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    48
    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
    49
          ==> {|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
    50
                RA|}  : responses evs"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    51
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    52
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3466
diff changeset
    53
consts     recur   :: event list set
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3466
diff changeset
    54
inductive "recur"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    55
  intrs 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    56
         (*Initial trace is empty*)
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3466
diff changeset
    57
    Nil  "[]: recur"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    58
2532
cde25bf71cc1 Improved layout and updated comments
paulson
parents: 2516
diff changeset
    59
         (*The spy MAY say anything he CAN say.  Common to
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    60
           all similar protocols.*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    61
    Fake "[| evs: recur;  X: synth (analz (spies evs)) |]
3519
ab0a9fbed4c0 Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents: 3466
diff changeset
    62
          ==> Says Spy B X  # evs : recur"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    63
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    64
         (*Alice initiates a protocol run.
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    65
           END is a placeholder to terminate the nesting.*)
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    66
    RA1  "[| evs1: recur;  Nonce NA ~: used evs1 |]
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    67
          ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|})
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    68
              # evs1 : recur"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    69
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    70
         (*Bob's response to Alice's message.  C might be the Server.
4552
bb8ff763c93d Simplified proofs by omitting PA = {|XA, ...|} from RA2
paulson
parents: 3683
diff changeset
    71
           We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because
bb8ff763c93d Simplified proofs by omitting PA = {|XA, ...|} from RA2
paulson
parents: 3683
diff changeset
    72
           it complicates proofs, so B may respond to any message at all!*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    73
    RA2  "[| evs2: recur;  Nonce NB ~: used evs2;
4552
bb8ff763c93d Simplified proofs by omitting PA = {|XA, ...|} from RA2
paulson
parents: 3683
diff changeset
    74
             Says A' B PA : set evs2 |]
2516
4d68fbe6378b Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents: 2485
diff changeset
    75
          ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    76
              # evs2 : recur"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    77
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2532
diff changeset
    78
         (*The Server receives Bob's message and prepares a response.*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    79
    RA3  "[| evs3: recur;  Says B' Server PB : set evs3;
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    80
             (PB,RB,K) : respond evs3 |]
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    81
          ==> Says Server B RB # evs3 : recur"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    82
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    83
         (*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
    84
           those in the message he previously sent the Server.*)
5434
9b4bed3f394c Got rid of not_Says_to_self and most uses of ~= in definitions and theorems
paulson
parents: 5359
diff changeset
    85
    RA4  "[| evs4: recur;  
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    86
             Says B  C {|XH, Agent B, Agent C, Nonce NB, 
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    87
                         XA, Agent A, Agent B, Nonce NA, P|} : set evs4;
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2532
diff changeset
    88
             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
    89
                         Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
3659
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    90
                         RA|} : set evs4 |]
eddedfe2f3f8 Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents: 3519
diff changeset
    91
          ==> Says B A RA # evs4 : recur"
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    92
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    93
end
5359
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
    94
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
    95
   (*No "oops" message can easily be expressed.  Each session key is
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
    96
     associated--in two separate messages--with two nonces.  This is 
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
    97
     one try, but it isn't that useful.  Re domino attack, note that
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
    98
     Recur.ML proves that each session key is secure provided the two
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
    99
     peers are, even if there are compromised agents elsewhere in
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
   100
     the chain.  Oops cases proved using parts_cut, Key_in_keysFor_parts,
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
   101
     etc.
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
   102
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
   103
    Oops  "[| evso: recur;  Says Server B RB : set evso;
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
   104
	      RB : responses evs';  Key K : parts {RB} |]
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
   105
           ==> Notes Spy {|Key K, RB|} # evso : recur"
bd539b72d484 Tidying
paulson
parents: 4552
diff changeset
   106
  *)