### Paper Menu >>

### Journal Menu >>

Journal of Information Security, 2010, 1, 56-67 doi:10.4236/jis.2010.12007 Published Online October 2010 (http://www.SciRP.org/journal/jis) Copyright © 2010 SciRes. JIS Extending the Strand Space Method with Timestamps: Part II Application to Kerberos V* Yongjian Li 1,2 , Jun Pang 3 1Chinese Academy of Sciences, Institute of Software Laboratory of Computer Science, Beijing, China 2The State Key Laboratory of Information Security, Beijing, China 3University of Oldenburg Department of Computer Science Safety-critical Embedded Systems, Oldenburg, Germany E-mail: lyj238@ios.ac.cn, jun.pang@informatik.uni-oldenburg.de Received June 23, 2010; revised Sep tember 14, 2010; accepted July 12, 2010 Abstract In this paper, we show how to use the novel extended strand space method to verify Kerberos V. First, we formally model novel semantical features in Kerberos V such as timestamps and protocol mixture in this new framework. Second, we apply unsolicited authentication test to prove its secrecy and authentication goals of Kerberos V. Our formalization and proof in this case study have been mechanized using Isabelle/HOL. Keywords: Strand Space, Kerberos V, Theorem Proving, Verification, Isabelle/HOL 1. Introduction The first version of Kerberos protocol was developed in the mid eighties as part of project Athena at MIT [1]. Over twenty years, different versions of Kerberos protocols have evolved. Kerberos V (Figure 1 and Figure 2) is the latest version released by the Internet Engineering Task Force (IETF) [2]. It is a password- based system for authentication and authorization over local area networks. It is designed with the following aims: once a client authenticates himself to a network machine, the process of obtaining authorization to access another network service should be completely trans- parent to him. Namely, the client only needs enter his password once during the authentication phase. As we introduced in the previous paper [3], there are two novel semantic features in Kerberos V protocol. First, it uses timestamps to prevent replay attacks, so this deficiency of the strand space theory makes it difficult to analyze these protocols. Second, it is divided into three causally related multiple phases: authentication, authorization, and service protocol phases. One phase may be used to retrieve a ticket from a key distribution center, while a second phase is used to present the ticket to a security-aware server. To make matters more complex, Kerbeors uses timestamps to guarantee the recency of these tickets, that is, such tickets are only valid for an interval, and multiple sub-protocol sessions can start in parallel by the same agent using the same ticket if the ticket does not expire. Little work has been done to formalize both the timestamps and protocol mixture in a semantic framework. The aim of this paper is practical. We hope to apply the extended theory in [3] to the analysis of Kerberos V protocol. Kerberos V is appropriate as our case study because it covers both timestamps and protocol mixture semantical features. Structure of the Paper: Section 2 briefly introduces the overview of Kerberos V. Section 3 presents the formalization of Kerberos V. Sections 4 and 5 prove its secrecy and authentication goals. We discuss related work and conclude the paper in Section 6. 2. An Overview of Kerberos V The protocol’s layout and its message exchanging are presented in Figure 1 and Figure 2 separately. In the infrastructure of the Kerberos V protocol, there is a unique authentication server, and some (not necessarily only one) ticket granting servers. The latter assumption is different from that in [4], where only a unique ticket granting server exists. *This is a revised and extended version of the homonymous paper ap- pearing in the Proceedings the Eighth International Conference on Paral- lel and Distributed Computing, Applications and Technologies (PDCAT 2007, IEEE Computer Society). The main modifications have been made on the presentation of the technical material, with the purpose of having full details. The first author is supported by grants (No. 60833001, 60496321, 60421001) from National Natural Science Foundation of Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 57 Figure 1. The layout of Kerberos V. { } } { { } } } { { } } { { 2 1. :, 2. :,,,,,,, 3.:,,,, ,, 4.:, ,,, Tgs Tgs B K authTicket K authK SK seruTick AKasA Tgs KasAA Tgs authK TaA TgsauthK TaKA ATgsATgsauthKTaA tB TgsAA B seruK T → → → → Authentication phase Authorisation Phase 1444442444443 { } } {} {} } { } 3 3 , ,, 5. :,,,,, 6. : B SauthK et SK seruK seruK AB seruK T ABABseruKTA t BA t → → Service Phase 14444244443 Figure 2. Kerberos V: message exchanging. In order to access some network service, the client needs to communicate with two trusted servers Kas and Tgs. Kas is an authentication server (or the key distribution center) and it provides keys for communication between clients and ticket granting servers. Tgs is a ticket granting server and it provides keys for communication between clients and application servers. The full protocol has three phases each consisting of two messages between the client and one of the servers in turn. Messages 2 and 4 are different from those in Kerberos IV [1,4] in that nested encryption has been cancelled. Later we will show that this change does not affect goals of the protocol. Detailed explanation about Kerberos V is delayed to Section 2, where the protocol is formalized in strand space model with our extensions. Here we only give an overview of the general principles to guarantee recency, secrecy and authentication in the design of Kerberos V. For recency, • A regular sender should attach a timestamp to indicate the time when the message is issued; usually such a message is of the form { } , , K tK K, where t is the time, K may be either a session key or long-term key. • When a regular receiver the message { } , , K t K K first he need be ensured of K ’s secrecy to guarantee that the message is not froged by the penetrator. Second he check the recency of the message by comparing the timestamp t with the reception time. More formally, if the receiving node is n , then )( ntime should be no later than ( ) cracktime Kt + , meaning that this message cannot be cracked at ( ) time n , which in turn indicates that the message { } , , K t K K is recent. For an encrypted message { } K h , the secrecy of a part of the plain message h also comes from both the secrecy of K and the recency of the message { } K h itself. That is to say, when a regular receives { } K h at time t , it must be ensured that the aforementioned two conditions must be guaranteed until t . From this, we can see that recency and secrecy are closely related with each other in a timed protocol framework. Unsolicited tests are the main mechanism to guarantee authentication. Because a guarantee of the existence of a regular node can be drawn from an unsolicited test, a regular agent uses unsolicited test to authenticate its regular protocol participant in Kerberos V. Now let us briefly review the main theoretical results in [3], which will be used in this work. For interesting readers, refer to [3] for preliminary definitions. If an agent is not a penetrator then his shared key cannot be penetrated, which is formalized as follows: Axiom 1 If A ∉ Bad , then P K∉ A K . Lemma 1 is the main technique used to reason about authentication guarantee of a node n which is an unsolicited test for an encrypted term of the form { } K h (e.g., the tickets { } , ,, A a K A TgsauthKT , { } , authK A t , and so on). That is to say, regular agents can use an unsolicited test with other properties of the protocol to guarantee that the agent who originates the term { } K h should be an intended regular agent. Lemma 1 (Unsolicited authentication test) B is a given bundle. Let n be an unsolicited test for { } K h . Then there exists a positive regular node m in B such that nm B and { } )( mtermh K ⊏ and { } ) ( ' K mtermh ⊏ / for any node ' m such that mm' B . Let a be an atomic message that uniquely originates at some node n , m be a positive penetrator node in a bundle B such that and ( ) . mterma ⊏ Suppose M is a test suite for a w.r.t. m in the bundle B . A strand’s Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 58 receiving nodes get messages which are all in ( ) , Msynth but a new message, which is not in ( ) Msynth , is sent in the strand, then the strand must be regular because a penetrator strand can not create such a term. Lemma 2 Let m be a positive node in a bundle , B a be an atomic message that uniquely originates at a regular node n , M be a message set such that ( ) ,,,,, B nmaMsuite and ( ) ( ) ' term msynth M ∈ for any node such that , ' m m + ⇒ and ( ) ( ) , term msynth M ∉ then m is regular . We will illustrate these general principles in detail in the next sections when we formalize the semantics and prove secrecy properties of Kerberos V. 3. Formalizing Kerberos V To model the time for a penetrator to break a message encrypted by a long-term shared key or a session key, we define two constants imeshrKcrackt and ktimesessionKcr . The crack time of any regular agent’s long-term shared key is the constant shrKcracktime, Axiom 2 () = shrKcracktime A cracktime K , for any regular agent A in Kerberos V. The crack time of any session key originated by an authentication server is the constant sessionKcrktime. Axiom 3 () =sessionKcrktime cracktime authK , for any session key authK originated by Kas . The trace tr specifications of the regular strands of Kerberos V (see Figure 2) are defined as predicates:1 1) Part I (Authentication Phase) • Ag-I ],,,,,,,[ 101 ttauthTicketTauthKTgsAi a iff { } { { } } 0 1 1 ( , ,,), () =(,,, , ,,) aKA tA Tgs tr itauthTicket A TgsauthKT + − where TGSs ∈ Tgs and imeshrKcrackt 1 ≤− a Tt . • AS ],,,,,[ 10 ttauthKTgsAas iff { } { } { { } + − ),,, ,,,,,,( ),,,,( =)( 1 11 0 A K Tgs K tauthKTgsA tauthKTgsAt TgsAt astr where TGSs ∈ Tgs . In the first phase, when Kas issues the second message { } { { } } ,,,,,, , A Tgs aa K K A TgsauthKTA TgsauthKT , authK is the session key that will be used for the client A to communicate with a ticket grant server Tgs , Kas attaches a T with the message to indicate when this message is sent; if A receives this message at time 1 t , A will check the condition 1 shrKcracktime a t T − ≤ to ensure the recency of this message. At the end of this phase, A obtains a ticket authTicket and the session key authK to communicate with Tgs. 2) Part II (Authorization Phase) • Ag-II ,,,,,,,[ 2S TservKBauthTicketauthKAi ],, 32 ttservTicket iff ∧∃ 21101 .,,,, iittTTgsi a a Ag-I ∧ ],,,,,,,[ 101 ttauthTicketTauthKTgsAi a ( ) { { } { { } 2 2 2 3 ( , ,, ,,), =( ,,, , ,,) authK SauthK t authTicket A tB tr it servTicket A BservKT + − where TGSs ∈ Tgs and imeshrKcrackt 3 ≤− a Tt and ktime.sessionKcr 3 ≤− S Tt • TGS a TBservKauthKTgsAtgs ,,,,,,[ , ],, 100 ttT iff { } { { } { } { { } } + − ),,, ,,,,,,( ),,, ,,,,,,( =)( 1 11 0 0 authK B K authK Tgs K a tservKBA tservKBAt BTA TauthKTgsAt tgstr where TGSs, ∈ Tgs TGSs, ∉ B 1 sessionKcrktime t + ≤ shrKcracktime a T+ . In the second phase, the situation is more complex. Both Tgs and A need to check whether their received messages are recent by the same mechanism. Furthermore, Tgs also need ensure a side condition that 1 sessionKcrktime shrKcracktime a t T+≤ + to guarantee that the application server B only receives a recent service ticket. Informally speaking, this condition means that Tgs can guarantee any authK that he receives can only be compromised later than servK which is associated with the authK . We will comment this side condition in analysis in the third phase. At the end of this phase, A obtains a ticket servTicket and the session key servK to communicate with B . 1 For simplicity, we assume any trace of a regular agent always re spects the time order in Kerberos V protocol, and we do not include this side condition in the trace specifications. Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 59 3) Part III (Service Phase) • Ag-III 34 5 [ ,,,,,] iA servKservTicket tt iff 10 1 223 ,,,,, ,,,,,, a S iTgsauthKTttiauthTicketB Ttt ∃ . ( ) 3 tr i = {{ } ( ) { } ( ) 4 4 5 4 , ,,,, , , servK servK tservTicketA t t t + ∧ − Ag-I 10 1 [ ,,,,,,,] a iA TgsauthKTauthTickettt ∧ Ag-II 2 [ ,,,,,, S iA authKauthTicketBservKT , 2 31223 , , ] servTicket ttiiii ∧ ∧ a a where T gs ∈ TGSs , 5 shrKcracktime a t T−≤ and 5 sessionKcrktime. S t T− ≤ • Apps 40 1 [, , ,,,,,] S appsA B servK TTtt iff ()= tr apps { } { { } } { } 0 4 1 1 ( , ,,,,,,), ( ,,) SservK KB servK tABservKTAT t t − + where 0 sessionKcrktime S t T− ≤ . In the last phase, it is subtle for the application server B to check the recency of the message { } { } { } 4 , ,,,, SservK KB ABservKTA T . From the ticket { } ,,, S K B A B servKT , B knows that Tgs must have issued {} {} { } 4 , ,,,, ,,, S S K authK B ABservKTAB TservKT at time S T . The potential compromise of 0 ls0 ws3b">T servTicket*,*] and 3 [ ,,,, iA servKservTicket Ag_III 4 ,*] T . The client strand in the service phase uses { } 4 servK T as an unsolicited test to authenticate the application server strand. This guarantee is also ensured from the secrecy of servK , which is in turn guaranteed by the ticket { } , ,, S authK A B servK T , and { } , ,, a K A A TgsauthKT . By the trace specification of an application server strand, we have that { } 4 servK T is received by A earlier than the time ktimesessionKcr + S T and imeshrKcrackt + a T . By Lemma 7, servK is safe at that time. Lemma 14 Let Bad ∉ BA, , TGSs ∉ B . If 3 i is a client strand in a service phase such that 3 [ , i Age nt_III ],,,,, 4∗ tservTicketservKA and B ∈ ,1)( 3 i , and 2 i is a client strand in the authorization phase such that 2 [, ,,, ,,,, S iA authKauthTicketBservKTservTicket Agent_II 2 3 , ] t t and 2 3 i i a , then there exists an application server strand b such that 4 ,,,,,[tTservKBAb S Apps , ],, ∗ ∗ and B ∈ ,1)(b . Proof. By analysis on the form of strand 3 i and , 2 i we have (1) ,1)( 3 iterm = { } 4 servK t and (2) { , , A B } , authK servKTs ⊏ ,1)( 2 iterm . By unfolding the definition of Agent_II, there exists a client strand 1 i such that 1 i a 2 i and Ag-I ,[ 1 i,A ,Tgs ,authK , a T ,authTicket , 0 t] 1 t and Tgs ∈ TGSs for some ,Tgs , a T, 0 t. 1 t Obviously, (3) { } , ,, a K A A TgsauthKT ⊏ ,1),( 1 iterm ,1)( 1 itime ≤ a T imeshrKcrackt +. From 1 i a 2 i and 2 i a , 3 i we can easily conclude that ,1)( 1 i + ⇒ ,1)( 3 i and ,1)( 2 i + ⇒ ,1).( 3 i With ,1)( 3 i ∈ B , we have ,1)( 2 i ∈ B and ,1)( 1 i ∈ B . With (2)(3), by Lemma 7, (4) ( ) mterm ≠ servK for any node m such that )(mtime ≤ S TktimesessionKcr +. By the definition of Agent_III, we have (5) ,1)( 3 itime ≤ S T ktime.sessionKcr + From (4)(5), we have ( ) mterm ≠ servK for any node m such that )(mtime ≤ ,1),( 3 itime therefore regular ( ) .,1),(, 3 B iservK So ,1)( 3 i is an unsolicited test for { } 4 servK T in . B By Lemma 1, (5) there is a regular positive node m such that m ,1)( 3 i B and { } 4 servK t ⊏ ( ) mterm and { } 4 authK t ⊏ / )( ' mterm for any node ' m such that ' m.m B Obviously B ∈ m . By simple case analysis, we have that m must be in an application server b such that ,[b Apps , ' A, ' B, ' servK , ' S T, 4 ' t , ∗ ], ∗ ,1).(= bm By the definition of Apps , ,1)(bterm = . 4 ' servK ' t With ,1)( 4 btermt servK ⊏ , we have (6) servKservK ' = and .= 44tt' Let { } { } { } .| ,,, ,,,, =tservKt TservKBA TservKBA M authK S B K S df ⊏ / ∪ Obviously ,0)(btime ,1)(btime B ,1)( 3 itime B ≤ S T + ktimesessionKcr , by the proof of Lemma 7, we have ,0)(bterm ∈ ),(Msynth i.e., { } { } { } 4 , ,,,( ) B ''' ' S'servK K ABservKTtsynth M ′ ′ ′∈. By the definition of synth , we have { } , ,, B ''' ' S ' K A B servKT ′ ∈ ),(Msynth then we have (7) { } , ,, B ' '' ' S ' K A BservKT ′ ∈ M or (8) { } , ,, ''' ' S A B servKT ∈ ).(Msynth If (7) holds, from (6) (7) and the definition of M , we have { } , ,, S A B servK T = { } , ,, ''' ' S A B servKT , then A = ' A and B = ' B and S T = . ' S T Therefore, the conclusion holds. If (8) holds, by the definition of synth, we have ' servK ∈ ),(Msynth with (6), we have servK ∈ ),(Msynth then by the definition of synth, we have servK ∈ ,M but this contradicts with the definition of M . Roughly speaking, we need two steps to prove an authentication goal that if there is a regular responder strand Resp ( r , x r ) and the k -th node of the strand is in a bundle B , then there is an initiator strand Init ( i , x r ) and some j-th node of the initiator strand is in B . First we prove that ),( kr is an unsolicited test for some encrypted term { } K h in B , which requires the secrecy of K . This is can be easily proved by the secrecy results on keys in section 3. Therefore, we have that there exists some regular node m in B by Lemma 2. Second, we need prove that m indeed is the intended node ),(ji . In order to prove this, we need do case analysis on the form of the strand which m possibly lies in. This proof needs unicity property of some session keys and the results of unsolicted tests, namely, the facts that { } K h ⊏ )(mterm and m is minimal. 6. Conclusions and Related Work Our main aim is to extend and mechanize the strand space theory to analyze Kerberos V, since mechanization in a theorem prover not only helps us model protocols rigorously and specify protocol goals without any ambiguity, it also guarantees a formal proof. Besides the Y. J. LI ET AL. Copyright © 2010 SciRes. JIS 67 essential inherence from the classic strand space method, our work is deeply inspired by Paulson and Bella’s work. We have directly used their formalization of message algebra, and have learned a lot about the semantics of timestamps and replay attacks from [4]. However, we model and analyze protocols in strand space theory rather than in Paulson's trace theory. In detail, we model behaviors of all the agents by strands, and mainly use the well-founded induction principle to prove properties. So in our Isabelle formalization, main efforts have been devoted to definitions and lemmas about strand space theory. e.g., we formalize strands, bundles, unique originality, the well-founded principle on bundles, and use this principle to prove important results such as unsolicited authentication test and regularity of keys. In [4], the ability of a penetrator to crack a stale en- crypted message is modelled by the Oops rule in the inductive definition of a trace, and the trace definition depends on the protocol under study. However, in the strand space theory, a penetrator’s abilities are modelled to be independent of the protocol, that is the main reason why we relate a key with a crack time, and model a penetrator’s ability of cracking a stale encrypted message by a new key cracking strand. The advantage of our method is that modelling a penetrator’s behavior remains independent and results such as the unsolicited authen- tication tests can be generalized. Regarding verification of the Kerberos protocols, Mitchell et al. [7] analyzed a simplified version of the protocol by model checking, and Butler et al. [8] analyzed the Kerberos V protocol using MSR [9]. But they did not include timestamps and replay attacks in their model, in fact the former work ignored both nonces and timestamps, and the latter only considered the implementation of the Kerberos protocol basing on nonce. 7. References [1] S. P. Miller, J. I. Neuman, J. I. Schiller and J. H. Saltzer, “Kerberos Authentication and Authorisation System,” Technical Report, Technical Plan Section E.2.1, MIT, Athena, 1989. [2] K. R. C. Neuman and S. Hartman, “The Kerberos Net- work Authentication Service (v5),” Technical report, In- ternet RFC 4120, July 2005. [3] Y. L. and J. Pang, “Extending the Strand Space Method with Timestamps: Part I the Theory,” Journal of Informa- tion Security, Vol. 1, No. 2, 2010, pp. 45-55. [4] G. Bella, “Inductive Verification of Cryptographic Pro- tocols,” PhD Thesis, Cambridge University Computer Laboratory, 2000. [5] F. Javier Thayer, J. C. Herzog and J. D. Guttman, “Strand Spaces: Proving Security Protocols Correct,” Journal of Computer Security, Vol. 7, No. 1, 1999, pp. 191-230. [6] Y. Li, “Strand Space and Security Protocols”. http://lcs. ios.ac.cn/˜lyj238/strand.html. [7] J. C. Mitchell, M. Mitchell and U. Stern, “Automated Analysis of Cryptographic Protocols Using Murphi,” Proceedings of 18th Symposium on Security and Privacy, 1997, pp. 141-153. [8] L. Bozga, C. Ene and Y. Lakhnech, “A Symbolic Deci- sion Procedure for Cryptographic Protocols with Time Stamps,” Journal of Logic and Algebraic Programming, Vol. 65, No. 1, 2005, pp. 1-35. [9] F. Butler, I. Cervesato, A. Jaggard and A. Scedrov, “A formal Analysis of Some Properties of Kerberos 5 Using MSR,” Proceedings of 15th IEEE Computer Security Foundations Workshop, 2002, pp. 175-190. |