src/HOL/Auth/KerberosIV.thy
author wenzelm
Sat Oct 06 00:02:46 2001 +0200 (2001-10-06)
changeset 11704 3c50a2cd6f00
parent 11701 3d51fbf81c17
child 13507 febb8e5d2a9d
permissions -rw-r--r--
* sane numerals (stage 2): plain "num" syntax (removed "#");
paulson@6452
     1
(*  Title:      HOL/Auth/KerberosIV
paulson@6452
     2
    ID:         $Id$
paulson@6452
     3
    Author:     Giampaolo Bella, Cambridge University Computer Laboratory
paulson@6452
     4
    Copyright   1998  University of Cambridge
paulson@6452
     5
paulson@6452
     6
The Kerberos protocol, version IV.
paulson@6452
     7
*)
paulson@6452
     8
paulson@6452
     9
KerberosIV = Shared +
paulson@6452
    10
paulson@6452
    11
syntax
paulson@6452
    12
  Kas, Tgs :: agent    (*the two servers are translations...*)
paulson@6452
    13
paulson@6452
    14
paulson@6452
    15
translations
paulson@6452
    16
  "Kas"       == "Server"
paulson@6452
    17
  "Tgs"       == "Friend 0"   
paulson@6452
    18
paulson@6452
    19
paulson@6452
    20
rules
paulson@6452
    21
  (*Tgs is secure --- we already know that Kas is secure*)
paulson@11185
    22
  Tgs_not_bad "Tgs \\<notin> bad"
paulson@6452
    23
  
paulson@6452
    24
(*The current time is just the length of the trace!*)
paulson@6452
    25
syntax
paulson@6452
    26
    CT :: event list=>nat
paulson@6452
    27
paulson@6452
    28
    ExpirAuth :: [nat, event list] => bool
paulson@6452
    29
paulson@6452
    30
    ExpirServ :: [nat, event list] => bool 
paulson@6452
    31
paulson@6452
    32
    ExpirAutc :: [nat, event list] => bool 
paulson@6452
    33
paulson@6452
    34
    RecentResp :: [nat, nat] => bool
paulson@6452
    35
paulson@6452
    36
paulson@6452
    37
constdefs
paulson@6452
    38
 (* AuthKeys are those contained in an AuthTicket *)
paulson@6452
    39
    AuthKeys :: event list => key set
paulson@11185
    40
    "AuthKeys evs == {AuthKey. \\<exists>A Peer Tk. Says Kas A
paulson@6452
    41
                        (Crypt (shrK A) {|Key AuthKey, Agent Peer, Tk, 
paulson@6452
    42
                   (Crypt (shrK Peer) {|Agent A, Agent Peer, Key AuthKey, Tk|})
paulson@11185
    43
                  |}) \\<in> set evs}"
paulson@6452
    44
                      
paulson@6452
    45
 (* A is the true creator of X if she has sent X and X never appeared on
paulson@6452
    46
    the trace before this event. Recall that traces grow from head. *)
paulson@6452
    47
  Issues :: [agent , agent, msg, event list] => bool ("_ Issues _ with _ on _")
paulson@6452
    48
   "A Issues B with X on evs == 
paulson@11185
    49
      \\<exists>Y. Says A B Y \\<in> set evs & X \\<in> parts {Y} &
paulson@11185
    50
      X \\<notin> parts (spies (takeWhile (% z. z  \\<noteq> Says A B Y) (rev evs)))"
paulson@6452
    51
paulson@6452
    52
paulson@6452
    53
consts
paulson@6452
    54
paulson@6452
    55
    (*Duration of the authentication key*)
paulson@6452
    56
    AuthLife   :: nat
paulson@6452
    57
paulson@6452
    58
    (*Duration of the service key*)
paulson@6452
    59
    ServLife   :: nat
paulson@6452
    60
paulson@6452
    61
    (*Duration of an authenticator*)
paulson@6452
    62
    AutcLife   :: nat
paulson@6452
    63
paulson@6452
    64
    (*Upper bound on the time of reaction of a server*)
paulson@6452
    65
    RespLife   :: nat 
paulson@6452
    66
paulson@6452
    67
rules
wenzelm@11704
    68
     AuthLife_LB    "2 <= AuthLife"
wenzelm@11704
    69
     ServLife_LB    "2 <= ServLife"
wenzelm@11701
    70
     AutcLife_LB    "Suc 0 <= AutcLife" 
wenzelm@11701
    71
     RespLife_LB    "Suc 0 <= RespLife"
paulson@6452
    72
paulson@6452
    73
translations
paulson@6452
    74
   "CT" == "length"
paulson@6452
    75
paulson@6452
    76
   "ExpirAuth T evs" == "AuthLife + T < CT evs"
paulson@6452
    77
paulson@6452
    78
   "ExpirServ T evs" == "ServLife + T < CT evs"
paulson@6452
    79
paulson@6452
    80
   "ExpirAutc T evs" == "AutcLife + T < CT evs"
paulson@6452
    81
paulson@6452
    82
   "RecentResp T1 T2" == "T1 <= RespLife + T2"
paulson@6452
    83
paulson@6452
    84
(*---------------------------------------------------------------------*)
paulson@6452
    85
paulson@6452
    86
paulson@6452
    87
(* Predicate formalising the association between AuthKeys and ServKeys *)
paulson@6452
    88
constdefs 
paulson@6452
    89
  KeyCryptKey :: [key, key, event list] => bool
paulson@6452
    90
  "KeyCryptKey AuthKey ServKey evs ==
paulson@11185
    91
     \\<exists>A B tt. 
paulson@6452
    92
       Says Tgs A (Crypt AuthKey
paulson@6452
    93
                     {|Key ServKey, Agent B, tt,
paulson@6452
    94
                       Crypt (shrK B) {|Agent A, Agent B, Key ServKey, tt|} |})
paulson@11185
    95
         \\<in> set evs"
paulson@6452
    96
paulson@6452
    97
consts
paulson@6452
    98
paulson@6452
    99
kerberos   :: event list set
paulson@6452
   100
inductive "kerberos"
paulson@6452
   101
  intrs 
paulson@6452
   102
        
paulson@11185
   103
    Nil  "[] \\<in> kerberos"
paulson@6452
   104
paulson@11185
   105
    Fake "[| evsf \\<in> kerberos;  X \\<in> synth (analz (spies evsf)) |]
paulson@11185
   106
          ==> Says Spy B X  # evsf \\<in> kerberos"
paulson@6452
   107
paulson@6452
   108
(* FROM the initiator *)
paulson@11185
   109
    K1   "[| evs1 \\<in> kerberos |]
paulson@6452
   110
          ==> Says A Kas {|Agent A, Agent Tgs, Number (CT evs1)|} # evs1 
paulson@11185
   111
          \\<in> kerberos"
paulson@6452
   112
paulson@6452
   113
(* Adding the timestamp serves to A in K3 to check that
paulson@6452
   114
   she doesn't get a reply too late. This kind of timeouts are ordinary. 
paulson@6452
   115
   If a server's reply is late, then it is likely to be fake. *)
paulson@6452
   116
paulson@6452
   117
(*---------------------------------------------------------------------*)
paulson@6452
   118
paulson@6452
   119
(*FROM Kas *)
paulson@11185
   120
    K2  "[| evs2 \\<in> kerberos; Key AuthKey \\<notin> used evs2;
paulson@11185
   121
            Says A' Kas {|Agent A, Agent Tgs, Number Ta|} \\<in> set evs2 |]
paulson@6452
   122
          ==> Says Kas A
paulson@6452
   123
                (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number (CT evs2), 
paulson@6452
   124
                      (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey, 
paulson@11185
   125
                          Number (CT evs2)|})|}) # evs2 \\<in> kerberos"
paulson@6452
   126
(* 
paulson@6452
   127
  The internal encryption builds the AuthTicket.
paulson@6452
   128
  The timestamp doesn't change inside the two encryptions: the external copy
paulson@6452
   129
  will be used by the initiator in K3; the one inside the 
paulson@6452
   130
  AuthTicket by Tgs in K4.
paulson@6452
   131
*)
paulson@6452
   132
paulson@6452
   133
(*---------------------------------------------------------------------*)
paulson@6452
   134
paulson@6452
   135
(* FROM the initiator *)
paulson@11185
   136
    K3  "[| evs3 \\<in> kerberos; 
paulson@11185
   137
            Says A Kas {|Agent A, Agent Tgs, Number Ta|} \\<in> set evs3;
paulson@6452
   138
            Says Kas' A (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, 
paulson@11185
   139
              AuthTicket|}) \\<in> set evs3; 
paulson@6452
   140
            RecentResp Tk Ta
paulson@6452
   141
         |]
paulson@6452
   142
          ==> Says A Tgs {|AuthTicket, 
paulson@6452
   143
                           (Crypt AuthKey {|Agent A, Number (CT evs3)|}), 
paulson@11185
   144
                           Agent B|} # evs3 \\<in> kerberos"
paulson@6452
   145
(*The two events amongst the premises allow A to accept only those AuthKeys 
paulson@6452
   146
  that are not issued late. *)
paulson@6452
   147
paulson@6452
   148
(*---------------------------------------------------------------------*)
paulson@6452
   149
paulson@6452
   150
(* FROM Tgs *)
paulson@6452
   151
(* Note that the last temporal check is not mentioned in the original MIT
paulson@6452
   152
   specification. Adding it strengthens the guarantees assessed by the 
paulson@6452
   153
   protocol. Theorems that exploit it have the suffix `_refined'
paulson@6452
   154
*) 
paulson@11185
   155
    K4  "[| evs4 \\<in> kerberos; Key ServKey \\<notin> used evs4; B \\<noteq> Tgs; 
paulson@6452
   156
            Says A' Tgs {|
paulson@6452
   157
             (Crypt (shrK Tgs) {|Agent A, Agent Tgs, Key AuthKey,
paulson@6452
   158
				 Number Tk|}),
paulson@6452
   159
             (Crypt AuthKey {|Agent A, Number Ta1|}), Agent B|}
paulson@11185
   160
	        \\<in> set evs4;
paulson@6452
   161
            ~ ExpirAuth Tk evs4;
paulson@6452
   162
            ~ ExpirAutc Ta1 evs4; 
paulson@6452
   163
            ServLife + (CT evs4) <= AuthLife + Tk
paulson@6452
   164
         |]
paulson@6452
   165
          ==> Says Tgs A 
paulson@6452
   166
                (Crypt AuthKey {|Key ServKey, Agent B, Number (CT evs4),  
paulson@6452
   167
			       Crypt (shrK B) {|Agent A, Agent B, Key ServKey,
paulson@6452
   168
		 			        Number (CT evs4)|} |})
paulson@11185
   169
	        # evs4 \\<in> kerberos"
paulson@6452
   170
(* Tgs creates a new session key per each request for a service, without 
paulson@6452
   171
   checking if there is still a fresh one for that service.
paulson@6452
   172
   The cipher under Tgs' key is the AuthTicket, the cipher under B's key
paulson@6452
   173
   is the ServTicket, which is built now.
paulson@6452
   174
   NOTE that the last temporal check is not present in the MIT specification.
paulson@6452
   175
  
paulson@6452
   176
*)
paulson@6452
   177
paulson@6452
   178
(*---------------------------------------------------------------------*)
paulson@6452
   179
paulson@6452
   180
(* FROM the initiator *)
paulson@11185
   181
    K5  "[| evs5 \\<in> kerberos;  
paulson@6452
   182
            Says A Tgs 
paulson@6452
   183
                {|AuthTicket, (Crypt AuthKey {|Agent A, Number Ta1|} ),
paulson@6452
   184
		  Agent B|}
paulson@11185
   185
              \\<in> set evs5;
paulson@6452
   186
            Says Tgs' A 
paulson@6452
   187
             (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|} ) 
paulson@11185
   188
                \\<in> set evs5;
paulson@6452
   189
            RecentResp Tt Ta1 |]
paulson@6452
   190
          ==> Says A B {|ServTicket,
paulson@6452
   191
			 Crypt ServKey {|Agent A, Number (CT evs5)|} |}
paulson@11185
   192
               # evs5 \\<in> kerberos"
paulson@6452
   193
(* Checks similar to those in K3. *)
paulson@6452
   194
paulson@6452
   195
(*---------------------------------------------------------------------*)
paulson@6452
   196
paulson@6452
   197
(* FROM the responder*)
paulson@11185
   198
     K6  "[| evs6 \\<in> kerberos;
paulson@6452
   199
            Says A' B {|           
paulson@6452
   200
              (Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|} ),
paulson@6452
   201
              (Crypt ServKey {|Agent A, Number Ta2|} )|}
paulson@11185
   202
            \\<in> set evs6;
paulson@6452
   203
            ~ ExpirServ Tt evs6;
paulson@6452
   204
            ~ ExpirAutc Ta2 evs6
paulson@6452
   205
         |]
paulson@6452
   206
          ==> Says B A (Crypt ServKey (Number Ta2) )
paulson@11185
   207
               # evs6 \\<in> kerberos"
paulson@6452
   208
(* Checks similar to those in K4. *)
paulson@6452
   209
paulson@6452
   210
(*---------------------------------------------------------------------*)
paulson@6452
   211
paulson@6452
   212
(* Leaking an AuthKey... *)
paulson@11185
   213
    Oops1 "[| evsO1 \\<in> kerberos;  A \\<noteq> Spy;
paulson@6452
   214
              Says Kas A
paulson@6452
   215
                (Crypt (shrK A) {|Key AuthKey, Agent Tgs, Number Tk, 
paulson@11185
   216
                                  AuthTicket|})  \\<in> set evsO1;
paulson@6452
   217
              ExpirAuth Tk evsO1 |]
paulson@6452
   218
          ==> Says A Spy {|Agent A, Agent Tgs, Number Tk, Key AuthKey|} 
paulson@11185
   219
               # evsO1 \\<in> kerberos"
paulson@6452
   220
paulson@6452
   221
(*---------------------------------------------------------------------*)
paulson@6452
   222
paulson@6452
   223
(*Leaking a ServKey... *)
paulson@11185
   224
    Oops2 "[| evsO2 \\<in> kerberos;  A \\<noteq> Spy;
paulson@6452
   225
              Says Tgs A 
paulson@6452
   226
                (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})
paulson@11185
   227
                   \\<in> set evsO2;
paulson@6452
   228
              ExpirServ Tt evsO2 |]
paulson@6452
   229
          ==> Says A Spy {|Agent A, Agent B, Number Tt, Key ServKey|} 
paulson@11185
   230
               # evsO2 \\<in> kerberos"
paulson@6452
   231
paulson@6452
   232
(*---------------------------------------------------------------------*)
paulson@6452
   233
paulson@6452
   234
paulson@6452
   235
end