A Logic of Authentication - Coursework Example

This report is submitted as part requirement for the module COMPGA11 Research in Information Security at College London. It is substantially the result of my own work except where explicitly indicated in the text. The report may be freely copied and distributed provided the source is explicitly acknowledged. March 11, 2011 Conclusion 16 1 Chapter 1 Abstract In various distributed systems, authentication protocols constitute the very foundation of network security. It is in this regard that proper operation of these protocols is necessary. However, majority of these protocol designs were extremely prone to error, due to the inability of protocol designers to understand its features and apply the techniques of existing protocols appropriately. As a result, Borrows, Abadi and Needham formulated a logic of belief and action, to address these errors. The logic allows people to formally describe the beliefs of trustworthy parties involved in these authentication protocols, thus uncovering subtleties, redundancies and flaws through an analysis of the protocols’ syntax and semantics. Borrows, Abadi and Needham take four published protocols into account, in order to show how they illustrate the appropriateness of this logical method of analysis. But how sound is the logic that they are proposing? How far can a vague and ambiguous logic take us? This paper aims to introduce the famous BAN (Borrows, Abadi and Needham) logic and it’s use on one of the published protocols (i.e. Kerberos), to discuss the logic’s success, its successors, and to review the critiques made on the logic. This paper is based on the article ”A Logic of Authentication” published in 1989 by the authors Michael Burrows, Martin Abadi and Roger Needham, University of Cambridge. The paper was nominated for publication in TOCS by the Program Committee for the ACM SIGOPS Symposium on Operating Systems Principles, December 1989. The three authors completed part of this work at Digital Equipment Corporation and part at the University of Cambridge. 2 Chapter 2 Introduction In this chapter a brief introduction to the basic principles of the BAN logic is discussed as well as a short section about security protocols. 2.1 An Introduction to Borrows, Abadi, Need- ham (BAN) Logic The BAN Logic is named after Borrows, Abadi and Needham. The logic is, as they stated, a logic of belief and action. It contains no logical inversions; therefore it cannot be used to prove that a protocol is flawed. But when proof, that a protocol is correct, cannot be obtained, that protocol deserves to be treated with suspicion [?]. In other words BAN logic does not aim to prove the security of a protocol; it can only catch certain kinds of subtle errors, help us to reason about the protocol, and help us identify and formalize our assumptions and analysis. Details of the BAN logic such as the idealization of protocol transactions, along with the various inference rules, will be discussed on the later sections. The authors of ”A Logic of Authentication” introduce the BAN logic to protocol designers whom they believe are inappropriately copying available techniques; thus coming up with protocols containing many security flows. The authors explain the basic notation of the logic and five rules that are applied to analyze protocols. Afterwards, they move on to actually idealize different existing protocols to conclude that such a simple logic can capture subtle differences between protocols. If there is one thing that the authors forgot to mention, that would be the basic definitions of frequently used terms. So in this paper I will try my best to define those terms. 3 CHAPTER 2. INTRODUCTION 4 2.1.1 Security Protocols A security protocol usually uses cryptography to distribute messages, authenticate the communicating parties and protects data over an insecure network. It can be defined as a set of transactions or traces. Each transaction consists of a series of communication events, some of which are perhaps interleaved protocol runs. Every desirable security protocol should provide a comprehensive introduction of the details with respect to authentication, message delivery, encryption, decryption, etc. Therefore, security protocols are very suitable for rigorous analytical techniques, such as inductive definitions. Theorem proving is good at defining properties of security protocols and model checking is an effective means of detecting attacks. Why are security protocols used? • Distributing secret keys over an insecure network. • Authenticating the involved principals. • Assuring secrecy of message content. (Confidentiality) • Assuring integrity of messages. • Non-repudiation methods. If you search for the keyword ”security protocol” on the Internet, it could be understood that many protocols are designed for different purposes. They can apply different cryptographic algorithms and varied and complex authentication and authorization to set up a secure channel of communication. Regardless of these discrepancies from the details of security protocols, they end up becoming consistent and turn out to be analogous. Thus, perhaps the relatively easy and well-known Needham and Schroeder protocol provides a good example to help us understand the fundamentals of security protocols. Nevertheless, it is not this paper’s goal to discuss the details with respect to the fundamentals of cryptographic protocols. Though further research can always be done. Chapter 3 Main Body In this chapter the BAN logic will be discussed in a more detailed manner. Why has it been a success? And is it perfectly flawless? 3.1 The Logic of BAN - Part I BAN logic is a set of rules for defining and analyzing information exchange protocols. Specifically, BAN logic helps its users determine whether exchanged information is trustworthy, and if it is secured against eavesdropping. BAN logic starts with the assumption that all the information exchanges that happen in the media is vulnerable to tampering and public monitoring. This has evolved into the popular security mantra, ”Don’t trust the network”[?]. BAN Logic is an epistemic logic, whose formal proof of validity aims to analyze cryptographic protocols. There have been a lot of works involving the application of BAN since it was published in 1989. Nevertheless, BAN’s central language or syntax, ”epistemic modality,” has no standard semantics yet, thus creating confusion with regards to certain terms and notions. As a result of this confusion, the evaluation of various settings for the proof is very difficult. So before digging deeper into the BAN logic, lets make sure that we are familiar with the semantics involved.1 CHAPTER 3. MAIN BODY 6 3.1.1 Basic Notation The logic is best told in its creators’ words: Our formalism is built on a many-sorted model logic. In the logic we distinguish several sorts of objects: principals, encryption keys, and formulas (also called statements). We identify messages with statements in the logic. Typically, the symbols A, B, and S denote specific principals; K-1ab, K-1as and K-1bs denote specific shared keys; Ka, Kb, and Ks denote specific public keys, and Ka , Kb , and Ks denote the corresponding secret keys; and Na, Nb, and Nc denote specific statements. The symbols P, Q, and R range over principals; X and Y range over statements; and K ranges over encryption keys [4]. Moreover, the authors specify that the only connective that will be used is conjunction, which will be represented by a comma. Also, conjunctions will be treated as sets all throughout. Aside from conjunction, the following shall be used: • P believes X: “P believes X.” It may also be understood as: agent P is entitled to believe X, whatever X may be. In addition, agent P may possibly believe that X is true. • P sees X: “P sees X.” Someone has sent a message to agent P containing X. Here, P can thus read and repeat X, given that P has done some sort of prior decryption. • P said X: “P once said X.” The agent P at some time sent a message, which included the statement X. The time frame by which the message was sent is unknown. What is known is that at that time when the message was sent, P believed X. • P controls X: “P has jurisdiction over X.” The principal P is an expert on X and should therefore be trusted on matters that pertain to X. • fresh(X): “X is fresh.” X has not been sent in a previous message before the current run of the protocol. This is usually true for nonces, that is, expressions invented for the purpose of being fresh. Nonces commonly include a timestamp or a number that is used only once [4]. • P ↔K Q: P and Q may use the shared key K to communicate. K is good, insofar that it will never be discovered by any principal except for either P or Q, or a principal trusted by either P or Q [4]. CHAPTER 3. MAIN BODY 7 • →K P: P has K as a public key. The matching secret key (denoted as K-l) will never be discovered by any principal except for P, or a principal trusted by P [4]. • P ⇔X Q: The formula X is a secret known only to P and Q, and possibly to principals trusted by them. Only P and Q may use X to prove their identities to one another. An example of a secret is a password [4]. • {X}K,: This represents the formula X encrypted under the key K. Formally, {X}K is a convenient abbreviation for an expression of the form {X}K from P. We make the realistic assumption that each principal is able to recognize and ignore his own messages; the originator of each message is mentioned for this purpose [4]. • < X >y: This represents X combined with the formula Y; it is intended that Y be a secret and that its presence prove the identity of whoever utters < X >y. In implementations, X is simply concatenated with the password Y. Our notation highlights that Y plays a special role, as proof of origin for X, in much the same way as an encryption key [4]. 3.1.2 BAN Inference Rules Here are the following rules of inference used by Borrows, Abadi and Needham: [4] 1. Message-meaning rules: P bel Q ⇔K P, P sees {X}K |- P bel said X P bel →K , P sees {X}K-1 |-P bel Q said X P bl Q ⇔Y P, P sees < X > Y |- P bel Q said X 2. Nonce-verification: P bel fresh(X, P bel Q said X |- P bel Q bel X 3. Jurisdiction: P bel Q controls X, P bel Q bel X |- P bel X 4. See’s rules: P sees (X,Y) |- P sees X, P sees Y P sees < X >Y |- P sees X P bel Q ↔K P, P ses {X}K |- P sees X P bel K → P, P sees {X}K |- P sees X P bel K → Q, P sees {X}K-1 |- P sees X CHAPTER 3. MAIN BODY 8 5. Freshness: P bel fresh(X) |- P bel fresh(X,Y) 3.2 The BAN Logic - Part II In the BAN logic, three main stages are indicated to analyze a protocol. The first step involves expressing its goals and assumptions in a symbolic manner, that is to say, in a way that the logic can be used in the assurance of whether the goals are in fact achieved or not. In the second step, the protocol traces/transactions/ steps are also transformed using semantics. The combined effort of BAN and their logic eventually turned out to be a success. From here on, people were able to find flaws and inconsistencies from protocols such as the Needham-Schroeder public key protocol and the CCITT X.509 protocol [?]. In addition, protocol designers and publishers gradually used the logic to make claims about their protocol’s security. In addition to discovering the flaws in particular protocols, redundancies in many protocols, including the Needham-Schroeder, Kerberos, Otway-Rees, and the CCITT X.509, have been found [?]. Nevertheless, despite the success of the logic, a lot of critiques towards it have also been published. The most notable of them would be Nesset’s 1990 critique. Criticisms against the logic will be discussed in the latter sections of the paper. 3.3 Application of the BAN Logic on the Ker- beros Protocol In this section an introduction to the application of the logic will be made, as well a brief overview on how the Kerberos Protocol works. 3.3.1 The Kerberos Protocol The Internet is a place where security is always questionable. Many of the protocols used in the Internet do not provide any form of security. Tools to ”sniff” passwords off of the network are commonly used by malicious hackers. Thus, applications, which send an unencrypted password over the network, are extremely vulnerable. Worse yet, other clients / server applications rely on the client program to be ”honest” about the identity of the user who is using it. Other applications rely on the client to restrict its activities to those, which it is only allowed to do, with no other mode of enforcement by the server [?]. Moreover, firewalls are often chosen by various websites to occupy their network security slots. In fact, insiders carry out most of the infamous attacks rampant in computers. Unfortunately, firewalls assume that the outsiders cause all the threats, which is often CHAPTER 3. MAIN BODY 9 a very bad assumption. A major disadvantage of these firewalls would be the way they restrict the users using the Internet. These restrictions are often considered unacceptable and slightly extreme. Thus, as a solution to these network security problems, Kerberos was created by the MIT as a part of Project Athena and is now used everywhere. The Needham-Schroeder protocol makes use of a shared key between two agents, with help from an authentication server. It also makes use of timestamps as nonces, both to remove security problems and to reduce the total number of messages required. The protocol, having the goal of authentication, establishes a shared key between two principals with the help from a server. Lets have a look at an example from BAN’s paper [?]: Kerberos is available as a product by many vendors. In the protocol below, A and B are the two principals, Kas and Kbs as their private keys, and S as the authentication server. S and A generate the time stamps Ts and Ta, respectively, and S generates the lifetime L. The fourth message is used only if mutual authentication is required. The messages are as follows: Message 1. A → S : A, B. Message 2. S → A : {Ts, L, Kab, B, {Ts, L, Kab, A}Kbs}Kas. Message 3.A → B : {Ts, L, Kab, A}Kbs, {A, Ta}Kab. Message 4. B → A : {Ta + 1}Kab. The messages in actual words would be: • A sends a clear text message to S stating his desire to communicate with B • The server responds with an encrypted message containing a timestamp, a lifetime, a session key for A and B, and a ticket that only B can read. • A forwards the ticket to B together with an authenticator, which is a times- tamp encrypted with the session key. CHAPTER 3. MAIN BODY 10 • B decrypts the ticket and checks the timestamp and lifetime. If the ticket was created recently, he uses the enclosed key to decrypt the authenticator. • B then checks the authenticator’s timestamp and if it is recent, he uses the session key to return the timestamp that is checked by A. Afterwards, the principals proceed to use the session key once they are satisfied. The graphical representation of the messages of principals A and B [?] 3.3.2 Idealization of Kerberos We have seen the messages generated in the actual protocol. In the idealization process, the lifetime L is combined with the time stamp Ts, which is treated just like a nonce. Since the first step does not posses the logical properties of the protocol, it is left out: • Message 2. S → A : {Ts, A ↔Kab B, {Ts, A ↔Kab B}Kbs}Kas. • Message 3. A → B : {Ts, A ↔Kab B}Kbs, {Ta, A ↔Kab B}Kab from A. • Message 4. B → A : {Ta, A ↔Kab B}Kab from B. The following analysis results and assumptions are taken from the paper ”A Logic of Authentication” [4]. CHAPTER 3. MAIN BODY 11 Applying the rules mentioned earlier in the paper to the idealized Kerberos protocol does the analysis of the protocol. The main steps of the analysis are as follows: Using the jurisdiction rule, we finally get: A believes A ↔Kab B which concludes the analysis of message 2. By having the knowledge of the new key, B can decrypt the rest of message 3 and we deduce: CHAPTER 3. MAIN BODY 12 B believes A believes A ↔Kab B Finally by analyzing the fourth message we deduce the final results: • A believes A ↔Kab B • A believes X B believes A ↔Kab B • B believes A ↔Kab B • B believes A believes A ↔Kab B To summarize, if only the first three messages are used, we do not get: A believes B believes A ↔KabB, which shows that the three-message protocol does not convince A of B’s presence.2 3.4 Critiques of the BAN Logic 3.4.1 Nessett’s Critique As mentioned in the previous sections, various critiques have been published on the logic despite its success. Nessett, in 1990, criticizes BAN logic about its claimed goals of authentication [?]. By using a specific example with the use of the logic, he showed that the BAN logic could cause basic security flaws. Now consider a protocol step: A → B: {T, Kab}Ka-1 ⇒ B sees {T, A ↔Kab B}Ka-1 Using the assumptions: • B believes →Ka A • A believes A ↔Kab B • B believes fresh(T) CHAPTER 3. MAIN BODY 13 • B believes A controls A ↔Kab B The goal is to deduce: A ↔Kab B • (Using Assumption 1 and rule 1) B believes A said (T, A ↔Kab B) • (Using Assumption 3 and rule 5) B believes fresh(T, A ↔Kab B) • (Using rule 2) B believes A believes (T, A ↔Kab B) • (Using Assumption 4 and rule 3) B believes (T, A ↔Kab B) Outcome: Ka is a public key therefore Kab is exposed. Nessett believes that idealization provides no handling of unauthorized release of secrets so the protocol may be inconsistent with beliefs about the confidentiality of keys and other secrets. 3.4.2 Other Critiques In 1991, Snekkenes examined the limitations of the BAN logic, and examined the logic’s disability to provide partial correctness proofs. I agree with Liebl’s critique that logic fails to clarify terms like “completeness.” Also, the logic does not take into account message confidentiality and the interaction of the protocol runs at different times of the same protocol [?]. In 1991,Syverson revealed confusions about the logic’s goals, and the problem of using the logic’s functional semantics. “Nevertheless, BAN’s central language construct, that is, ”epistemic modality”, has no agreed-upon semantics” - Chapter 1;Logic of BAN part I One of the major problems caused by the BAN logic would be found in the idealization step. This is due to the ambiguity and vagueness of its semantics. Further logical systems have been proposed and published, which took BAN logic as its starting point. Other Logic System Approaches GNY GNY logic is a successful but rather complicated approach, which takes the BAN logic into account but improves much of its scope. It is a logic, which aims to analyze a protocol step-by-step and explicitly make assumptions. This logic has several important advantages over the BAN logic. Unlike in BAN, The GNY logic clearly demarcates between the content and the meaning of messages; thus increasing consistency in the analysis. CHAPTER 3. MAIN BODY 14 In this way, various modes of reasoning are born in the process of analyzing. In GNY, principals have the right to include data, whose messages are those that they do not believe in. Message authentication is possible in GNY as a protection against replays. If we were to compare GNY and BAN logic, on the one hand, GNY only addresses authentication issues and is much more complicated and elaborate. At each stage, considerable amounts of rules have to be considered. It also had some drawbacks and shortcomings as revealed by Anderson in 1992. [?] BGNY logic is an extended version of GNY, proposed by Bracing. The belief logic is based on a software that automatically proves the authentication properties of cryptographic protocols. BGNY also operates at an intermediate level to specify protocol properties. Kailar also introduced a logic for the analysis of secure e-commerce protocols such as electronic transactions. This logic is more useful for the analysis of accountability rather than the belief of logics. In 1994, SvO logic was published, which served as the extension and a sort of variants of four different logics, namely, BAN, GNY, AT and vO, in a single unified framework. It should also be noted that SvO is simpler to use than any of these four, yet is much more expensive. Chapter 4 Conclusion After having discussed the BAN logic of authentication, it seems that idealization provides no sufficient handling of unauthorized release of secrets. As a result, the protocol may turn out to be inconsistent with beliefs about the confidentiality of keys and other secrets. Thus, we can jump to the conclusion that idealization does not address confidentiality. It is in my contention that the authors should have mentioned such an important fact in the entirety of the paper. Nevertheless, it is indeed inspiring to see that a subtype of modal logic can capture such subtle differences between protocols. It is in light that the logic of BAN, as shown herein, was a sound and justified method of analysis. The use of formal logic and its emphasis on syntax and semantics, paved the way towards an evolutionary epistemic logic across disciplines. While epistemology and logic has a long tradition and history, epistemic logic is considered to be a relatively new development with its application seen manifested in disciplines such as philosophy, theoretical computer science, artificial intelligence, economics, linguistics, and now, with the principles of operating computer systems as well. Indeed, with the dawn of a logic of authentication such as the BAN logic of authentication, the rate of subtleties, errors and flaws decrease, and as a result, a more efficient and effective system is thus formed. As shown in this paper, authentication protocols functioned correctly and more efficiently after the implementation of such logic. But nevertheless, I would highly recommend that the protocols should still be re-analyzed after idealization for reliability purposes. Also, when new rules are formulated or implemented, it should be made in such a way that it guarantees confidentiality and consistency. Note: Sometimes the technical will not sound logical to our ears. Ex: A believes a Nonce. Bibliography [1] Sape J. Mullender, Universiteit Twente. BAN Logic; A Logic of Authentication, [2] Wikipedia, BurrowsAbadiNeedham logic. [3] Hans van Ditmarsch, Wiebe van der Hoek, Barteld Kooi, Dynamic Epistemic Logic [4] Burrows, M., Abadi, M., Needham, R., “A logic of authentication”, ACM Transactions on Computer Systems, 8(1) : 18-36, February 1989. [5] Qinqfeng Chen, Chengqi Zhang, Shichao Zhang, Secure Transaction Protocol Analysis. [6] Sokratis Katsikas, Communications and Multimedia Security. [7] MIT web glossary; http://web.mit.edu/ 16 Read More