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