src/HOL/Auth/Recur.thy
author paulson
Fri, 11 Jul 1997 13:26:15 +0200
changeset 3512 9dcb4daa15e8
parent 3466 30791e5a69c4
child 3519 ab0a9fbed4c0
permissions -rw-r--r--
Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".
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;
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2550
diff changeset
    78
             Says A' B PA : set 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;
3465
e85c24717cad set_of_list -> set
nipkow
parents: 2550
diff changeset
    85
             Says B' Server PB : set 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, 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    93
                         XA, Agent A, Agent B, Nonce NA, P|} : set evs;
2550
8d8344bcf98a Re-ordering of certificates so that session keys appear in decreasing order
paulson
parents: 2532
diff changeset
    94
             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
    95
                         Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    96
                         RA|} : set evs |]
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    97
          ==> Says B A RA # evs : recur lost"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    98
3466
30791e5a69c4 Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents: 3465
diff changeset
    99
(**No "oops" message can easily be expressed.  Each session key is
2449
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   100
   associated--in two separate messages--with two nonces.
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   101
***)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   102
end