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