src/HOL/Auth/Recur.thy
author paulson
Wed, 18 Dec 1996 17:46:38 +0100
changeset 2449 d30ad12b1397
child 2451 ce85a2aafc7a
permissions -rw-r--r--
Recursive Authentication Protocol
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
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
     9
Recur = Shared + 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    10
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    11
syntax
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    12
  newK2    :: "nat*nat => key"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    13
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    14
translations
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    15
  "newK2 x"  == "newK(nPair x)"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    16
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    17
(*Two session keys are distributed to each agent except for the initiator,
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    18
	who receives one.
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    19
  Perhaps the two session keys could be bundled into a single message.
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    20
*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    21
consts     respond :: "nat => (nat*msg*msg)set"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    22
inductive "respond i"	(*Server's response to the nested message*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    23
  intrs
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    24
    (*The message "Agent Server" marks the end of a list.*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    25
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    26
    One  "[| A ~= Server;
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    27
	     MA = {|Agent A, Agent B, Nonce NA, Agent Server|} |]
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    28
          ==> (j, {|Hash{|Key(shrK A), MA|}, MA|}, 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    29
                  {|Agent A, 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    30
                    Crypt (shrK A) {|Key(newK2(i,j)), Agent B, Nonce NA|}, 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    31
                    Agent Server|})
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    32
              : respond i"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    33
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    34
    (*newK2(i,Suc j) is the key for A & B; newK2(i,j) is the key for B & C*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    35
    Cons "[| (Suc j, PA, RA) : respond i;
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    36
             B ~= Server;
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    37
	     MB = {|Agent B, Agent C, Nonce NB, PA|};
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    38
             PA = {|Hash{|Key(shrK A), MA|}, MA|};
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    39
             MA = {|Agent A, Agent B, Nonce NA, P|} |]
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    40
          ==> (j, {|Hash{|Key(shrK B), MB|}, MB|}, 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    41
                  {|Agent B, 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    42
                    Crypt (shrK B) {|Key(newK2(i,Suc j)), Agent A, Nonce NB|},
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    43
                    Agent B, 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    44
                    Crypt (shrK B) {|Key(newK2(i,j)), Agent C, Nonce NB|}, 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    45
                    RA|})
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    46
              : respond i"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    47
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    48
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    49
(*Induction over "respond" can be difficult, due to the complexity of the
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    50
  subgoals.  The "responses" relation formalizes the general form of its
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    51
  third component.
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    52
*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    53
consts     responses :: nat => msg set
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    54
inductive "responses i" 	
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    55
  intrs
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    56
    (*Server terminates lists*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    57
    Nil  "Agent Server : responses i"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    58
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    59
    Cons "RA : responses i
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    60
          ==> {|Agent B, 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    61
                Crypt (shrK B) {|Key(newK2(i,k)), Agent A, Nonce NB|},
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    62
                RA|}  : responses i"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    63
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    64
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    65
consts     recur   :: agent set => event list set
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    66
inductive "recur lost"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    67
  intrs 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    68
         (*Initial trace is empty*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    69
    Nil  "[]: recur lost"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    70
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    71
         (*The spy MAY say anything he CAN say.  We do not expect him to
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    72
           invent new nonces here, but he can also use NS1.  Common to
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    73
           all similar protocols.*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    74
    Fake "[| evs: recur lost;  B ~= Spy;  
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    75
             X: synth (analz (sees lost Spy evs)) |]
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    76
          ==> Says Spy B X  # evs : recur lost"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    77
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    78
         (*Alice initiates a protocol run.
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    79
           "Agent Server" is just a placeholder, to terminate the nesting.*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    80
    NA1  "[| evs: recur lost;  A ~= B;  A ~= Server;
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    81
             MA = {|Agent A, Agent B, Nonce(newN(length evs)), Agent Server|}|]
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    82
          ==> Says A B {|Hash{|Key(shrK A),MA|}, MA|} # evs : recur lost"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    83
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    84
         (*Bob's response to Alice's message.  C might be the Server.
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    85
           XA should be the Hash of the remaining components with KA, but
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    86
		Bob cannot check that.
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    87
           P is the previous recur message from Alice's caller.*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    88
    NA2  "[| evs: recur lost;  B ~= C;  B ~= Server;
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    89
             Says A' B PA : set_of_list evs;  
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    90
             PA = {|XA, Agent A, Agent B, Nonce NA, P|};
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    91
             MB = {|Agent B, Agent C, Nonce (newN(length evs)), PA|} |]
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    92
          ==> Says B C {|Hash{|Key(shrK B),MB|}, MB|} # evs : recur lost"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    93
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    94
         (*The Server receives and decodes Bob's message.  Then he generates
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    95
           a new session key and a response.*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    96
    NA3  "[| evs: recur lost;  B ~= Server;
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    97
             Says B' Server PB : set_of_list evs;
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    98
             (0,PB,RB) : respond (length evs) |]
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
    99
          ==> Says Server B RB # evs : recur lost"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   100
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   101
         (*Bob receives the returned message and compares the Nonces with
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   102
	   those in the message he previously sent the Server.*)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   103
    NA4  "[| evs: recur lost;  A ~= B;  
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   104
             Says C' B {|Agent B, 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   105
                         Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   106
                         Agent B, 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   107
                         Crypt (shrK B) {|Key KAC, Agent C, Nonce NB|}, RA|}
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   108
               : set_of_list evs;
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   109
             Says B  C {|XH, Agent B, Agent C, Nonce NB, 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   110
                         XA, Agent A, Agent B, Nonce NA, P|} 
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   111
               : set_of_list evs |]
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   112
          ==> Says B A RA # evs : recur lost"
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   113
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   114
(**No "oops" message can readily be expressed, since each session key is
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   115
   associated--in two separate messages--with two nonces.
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   116
***)
d30ad12b1397 Recursive Authentication Protocol
paulson
parents:
diff changeset
   117
end