Analysis of Cryptographic Protocols (CRYPTO) Publications

There is also a master index of publications for our branch.

2003

"Towards a Hierarchy of Cryptographic Protocol Models", in Proceedings of FMSE 2003: Formal Methods in Security Engineering, ACM Press, October 30, 2003. PDF

Recently there has been an increasing amount of research in the introduction of cryptographic ideas into discrete methods for cryptographic protocol analysis. This is often done by developing a discrete model and a cryptographic model such that the discrete model can be shown sound with respect to the cryptographic model. In this position paper we talk about some of the other issues in cryptographic protocol analysis that could be addressed with this approach, and propose a hierarchy of models.

"A Fault Tree Representation of NPATRL Security Requirements", Workshop on Issues in Theory of Security 2003, April 2003. PDF

In this paper we show how we can increase the ease of reading and writing security requirements for cryptographic protocols by developing a visual language based on fault trees. We develop such a semantics for a subset of NPATRL, a temporal language used for expressing safety requirements for cryptographic protocols, and show that the subset is sound and complete with respect to the semantics. We also show how the fault trees can be used to improve the presentation of some specifications that we developed in our analysis of the Group Domain of Interpretation (GDOI) protocol.

"What Makes a Cryptographic Protocol Secure? The Evolution of Requirements Specification in Formal Cryptographic Protocol Analysis." Proceedings of ESOP 03, Springer-Verlag, April 2003. PostScript, PDF

Much attention has been paid to the design of languages for the specification of cryptographic protocols. However, the ability to specify their desired behavior correctly is also important; indeed many perceived protocol flaws arise out of a misunderstanding of the protocol's requirements. In this talk we give a brief survey of the history of requirements specification in formal analysis of cryptographic protocols. We outline the main approaches and describe some of the open issues.

"A Procedure for Verifying Security Against Type Confusion Attacks." Proceedings of the 16th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, June 2003. PostScript, PDF

A type confusion attack is one in which a principal accepts data of one type as data of another. Although it has been shown by Heather et al. that there are simple formatting conventions that will guarantee that protocols are free from simple type confusions in which fields of one type are substituted for fields of another, it is not clear how well they defend against more complex attacks, or against attacks arising from interaction with protocols that are formatted according to different conventions.

---

In this paper we show how type confusion attacks can arise in realistic situations even when the types are explicitly defined in at least some of the messages, using examples from our recent analysis of the Group Domain of Interpretation Protocol. We then develop a formal model of types that can capture potential ambiguity of type notation, and outline a procedure for determining whether or not the types of two messages can be confused. This work extends our earlier work on the subject in that it includes an explicit model of attacker and defender and extends the informal model of the type confusion attack in terms of a game between an intruder and a set of honest principals in or earlier work to a more formal model in which actions of intruder and honest principals are described explicitly. This gives us a simpler, more intuitive approach that allows us to calculate probabilities in a more systematic manner, and to compare different intruder strategies and different assumptions about the way in which the protocol is implemented in terms of their effects on type confusion.

"Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends", IEEE Journal on Selected Areas in Communication, Vol. 21, No. 1, pp. 44-54, January 2003. PostScript, PDF

The history of the application of formal methods to cryptographic protocol analysis spans over twenty years, and recently has been showing signs of new maturity and consolidation. Not only have a number of specialized tools been developed, and general-purpose ones been adapted, but people have begun applying these tools to realistic protocols, in many cases supplying feedback to designers that can be used to improve the protocol's security. In this paper we will describe some of the ongoing work in this area, as well as describe some of the new challenges and the ways in which they are being met.

"Formal Specification and Analysis of the Group Domain of Interpretation Protocol Using NPATRL and the NRL Protocol Analyzer", Journal of Computer Security, to appear. PostScript, PDF

Although research has been going on in the formal analysis of cryptographic protocols for a number of years, they are only slowly being integrated into the protocol design process. In this paper we describe how we furthered the integration of analysis and design by working closely with the Multicast Security Working Group in the Internet Engineering Task Force on the analysis of a proposed Internet Standard, the Group Domain Of Interpretation (GDOI) Protocol. We describe the challenges that had to be met before the analysis could be successfully completed, and some of the challenges that still remain. Perhaps not surprisingly, some of the most challenging work was in understanding the security requirements for group protocols in general. We give a detailed specification of the requirements for GDOI, describe our formal analysis of the protocol with respect to these requirements, and show how our analysis impacted the development of GDOI.

2002

"Environmental Requirements for Authentication Protocols", Proceedings of the International Symposium on Software Security. Springer-Verlag LNCS 2609, pp. 339-355, November 2002. PostScript, PDF

Most work on requirements in the area of authentication protocols has concentrated on identifying requirements for the protocol without much consideration of context. Little work has concentrated on assumptions about the environment, for example, the applications that make use of authenticated keys. We will show in this paper how the interaction between a protocol and its environment can have a major effect on a protocol. Specifically we will demonstrate a number of attacks on published and/or widely used protocols that are not feasible against the protocol running in isolation (even with multiple runs) but become feasible in some application environments. We will also discuss the tradeoff between putting constraints on a protocol and putting constraints on the environment in which it operates.

"Using a Declarative Language to Build an Experimental Analysis Tool", Proceedings of PADL '02, Springer Verlag LNCS 2257, pp. 1-2. PostScript

In this paper we give a brief summary of our experience in using a declarative language, Prolog, to develop an experimental formal analysis tool, the NRL Protocol Analyzer, which was updated and modified over the years to incorporate new theories and techniques. We discuss the benefits of using such an approach, and also some of the downsides.

"A Unification Algorithm for the Group Diffie-Hellman Protocol", Proceedings of WITS'02, January, 2002. PostScript

Equational unification can be an effective tool for the analysis of cryptographic protocols. This, for example, is the technique used by the NRL Protocol Analyzer, which uses narrowing to reason about cryptographic operations which can be described in terms of rewrite rules. However, the effectiveness of equational unification in cryptographic protocol analysis has been hampered by the lack of unification algorithms that can be used to reason about some of the more equationally rich algorithms used by many cryptographic systems, such as Diffie-Hellman, group Diffie-Hellman, and blinded signatures. In this paper we attempt to close this gap by providing an algorithm that can be used to reason about protocols that use the Diffie-Hellman and group Diffie-Hellman algorithm.

2001

"Formalizing GDOI Group Key Management Requirements in NPATRL", Proc. 8th ACM Computer and Communications Security Conference --- CCS'01, (P. Samarati ed.), pp. 235--244, ACM Press, November 2001. PostScript, PDF

Although there is a substantial amount of work on formal requirements for two and three-party key distribution protocols, very little has been done on requirements for group protocols. However, since the latter have security requirements that can differ in important but subtle ways, we believe that a rigorous expression of these requirements can be useful in determining whether a given protocol can satisfy an application's needs. In this paper we make a first step in providing a formal understanding of security requirements for group key distribution by using the NPATRL language, a temporal requirement specification language for use with the NRL Protocol Analyzer. We specify the requirements for GDOI, a protocol being proposed as an IETF standard, which we are formally specifying and verifying in cooperation with the MSec working group.

2000

"Interpreting Strands in Linear Logic," Proceedings of the 2000 Workshop on Formal Methods and Computer Security - FMCS'00 (H. Veith, N. Heintze, E. Clarke, editors), Chicago, IL, July 20 2000. PostScript, PDF

The adoption of the Dolev-Yao model, an abstraction of security protocols that supports symbolic reasoning, is responsible for many successes in protocol analysis. In particular, it has enabled using logic effectively to reason about protocols. One recent framework for expressing the basic assumptions of the Dolev-Yao model is given by strand spaces, certain directed graphs whose structure reflects causal interactions among protocol participants. We represent strand constructions as relatively simple formulas in first-order linear logic, a refinement of traditional logic known for an intrinsic and natural accounting of process states, events, and resources. The proposed encoding is shown to be sound and complete. Interestingly, this encoding differs from the multiset rewriting definition of the Dolev-Yao model, which is also based on linear logic. This raises the possibility that the multiset rewriting framework may differ from strand spaces in some subtle way, although the two settings are known to agree on the basic secrecy property.

"Relating Strands and Multiset Rewriting for Security Protocol Analysis," Proceedings of the Thirteenth IEEE Computer Security Foundations Workshop - CSFW'00 (P. Syverson, editor), pp. 35-51, IEEE Computer Society Press, Cambridge, UK, 3-5 July 2000. PostScript, PDF

Formal analysis of security protocols is largely based on a set of assumptions commonly referred to as the Dolev-Yao model. Two formalisms that state the basic assumptions of this model are related here: strand spaces and multiset rewriting with existential quantification. Although it is fairly intuitive that these two languages should be equivalent in some way, a number of modifications to each system are required to obtain a meaningful equivalence. We extend the strand formalism with a way of incrementally growing bundles in order to emulate an execution of a protocol with parametric strands. We omit the initialization part of the multiset rewriting setting, which formalizes the choice of initial data, such as shared public or private keys, and which has no counterpart in the strand space setting. The correspondence between the modified formalisms directly relates the intruder theory from the multiset rewriting formalism to the penetrator strands.

"A Cost-Based Framework for Analysis of Denial of Service in Networks," Journal of Computer Security, to appear. PostScript, PDF

Denial of service is becoming a growing concern. As computer systems communicate more and more with others that they know less and less, they become increasingly vulnerable to hostile intruders who may take advantage of the very protocols intended for the establishment and authentication of communication to tie up resources and disable servers. This paper shows how some principles that have already been used to make cryptographic protocols more resistant to denial of service by trading off the cost to defender against the cost to the attacker can be formalized based on a modification of the Gong-Syverson fail-stop model of cryptographic protocols, and indicates the ways in which existing cryptographic protocol analysis tools could be modified to operate within this formal framework. We also indicate how this framework could be extended to protocols that do not make use of strong authentication.

"Extending Formal Cryptographic Protocol Analysis Techniques for Group Protocols and Low-Level Cryptographic Primitives," Proceedings of the First Workshop on Issues in the Theory of Security - WITS'00, (P. Degano, editors), pp. 87-92, Geneva, Switzerland, July 8-9 2000. PostScript, PDF

In this paper we show how we have been using the NRL Protocol Analyzer to analyze the Cliques protocol, a group key distribution protocol based on Group Diffie-Hellman.

"Invariant Generation Techniques in Cryptographic Protocol Analysis", Proceedings of the 13th Computer Security Foundations Workshop, IEEE Computer Society Press, July, 2000. PostScript, PDF

The growing interest in the application of formal methods of cryptographic protocol analysis has led to the development of a number of different techniques for generating and describing invariants that are defined in terms of what messages an intruder can and cannot learn. These invariants, which can be used to prove authentication as well as secrecy results, appear to be central to many different tools and techniques. However, since they are usually developed independently for different systems, it is often not easy to see what they have in common with each other, or to tell whether or not they can be used in systems other than the ones for which they were developed. In this paper we attempt to remedy this situation by giving an overview of several of these techniques, discussing their relationships to each other, and developing a simple taxonomy. We also discuss some of the implications for future research.

"Open Issues in Formal Methods for Cryptographic Protocol Analysis," Proceedings of DISCEX 2000, IEEE Computer Society Press, pp. 237-250, January, 2000. PostScript, PDF

The history of the application of formal methods to cryptographic protocol analysis spans nearly twenty years, and recently has been showing signs of new maturity and consolidation. A number of specialized tools have been developed, and others have effectively demonstrated that existing general-purpose tools can also be applied to these problems with good results. However, with this better understanding of the field comes new problems that strain against the limits of the existing tools. In this paper we will outline some of these new problem areas, and describe what new research needs to be done to to meet the challenges posed.

"Towards an Analysis of Onion Routing Security," Workshop on Design Issues in Anonymity and Unobservability Berkeley, CA, July 2000. PostScript, PDF

This paper presents a security analysis of Onion Routing, an application independent infrastructure for traffic-analysis-resistant and anonymous Internet connections. It also includes an overview of the current system design, definitions of security goals and new adversary models.

"Dolev-Yao is no better than Machiavelli," Proceedings of the First Workshop on Issues in the Theory of Security - WITS'00, (P. Degano, editors), pp. 87-92, Geneva, Switzerland, July 8-9 2000. PostScript, PDF

We show that all attacks that can be mounted by a traditional Dolev-Yao intruder against common cryptographic protocols can be enacted by an apparently weaker `Machiavellian' adversary in which compromised principals will not share long-term secrets and will not send arbitrary messages. We also show that a Dolev-Yao adversary composed of multiple compromised principals is equivalent to an adversary consisting of a single dishonest principal who is only willing to produce messages in valid protocol form.

1999

"CAPSL Interface for the NRL Protocol Analyzer", Proceedings of ASSET 99, IEEE Computer Society Press, March 1999. PostScript, PDF

The Common Authentication Protocol Specification Language (CAPSL) is a high-level language for applying formal methods to the security analysis of cryptographic protocols. Its goal is to permit a protocol to be specified once in a form that is usable as an interface to any type of analysis tool or technique, given appropriate translation software. This paper describes the first operational CAPSL translator to the language used by the NRL Protocol Analyzer (NPA), a software tool developed specifically for the analysis of cryptographic protocols.

"Analysis of the Internet Key Exchange Protocol Using the NRL Protocol Analyzer," Proceedings of the 1999 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, May 1999. PostScript, PDF

In this paper we show how the NRL Protocol Analyzer, a special-purpose formal methods tool designed for the verification of cryptographic protocols, was used in the analysis of the Internet Key Exchange (IKE) protocol. We describe some of the challenges we faced in analyzing IKE, which specifies a set of closely related subprotocols, and we show how this led to a number of improvements to the Analyzer. We also describe the results of our analysis, which uncovered several ambiguities and omissions in the specification which would have made possible attacks on some implementations that conformed to the letter, if not necessarily the intentions, of the specifications.

"A Formal Framework and Evaluation Method for Network Denial of Service," Proceedings of the IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, June 1999. PostScript, PDF

Denial of service is becoming a growing concern. As our systems communicate more and more with others that we know less and less, they become increasingly vulnerable to hostile intruders who may take advantage of the very protocols intended for the establishment and authentication of communication to tie up our resources and disable our servers. Since these attacks occur before parties are authenticated to each other, we cannot rely upon enforcement of the appropriate access control policy to protect us. Instead we must build our defenses, as much as possible, into the protocols them selves.This paper shows how some principles that have already been used to make protocols more resistant to denial of service can be formalized, and indicates the ways in which existing cryptographic protocol analysis tools could be modified to operate within this formal framework.

"Fair On-Line Auctions without Special Trusted Parties," in Financial Cryptography, FC'99 Matthew Franklin, Ed. Springer-Verlag, LNCS 1648 February 1999 pp. 230--240 PostScript, PDF

Traditional face-to-face (English) auctions rely on the auctioneer to fairly interact with bidders to accept the highest bid on behalf of the seller. On-line auctions also require fair negotiation. However, unlike face-to-face auctions, on-line auctions are inherently subject to attacks because the bidders and auctioneer are not copresent. These attacks include selectively blocking bids based on the bidder and amount and selectively closing the auction after a particular bid is received. In this paper, we present an on-line English auction in which bids are processed fairly and the auction closes fairly without specialized trusted parties. In particular, there is no need to trust the auctioneer to obtain a fair outcome to the auction.

Group Principals and the Formalization of Anonymity FM'99 -- Formal Methods, Vol. I J.M. Wing and J. Woodcock and J. Davies, Eds. Springer-Verlag, LNCS 1708 September 1999 pp. 814--833 PostScript, PDF

We introduce the concept of a group principal and present a number of different classes of group principals, including threshold-group-principals. These appear to naturally useful concepts for looking at security. We provide an associated epistemic language and logic and use it to reason about anonymity protocols and anonymity services, where protection properties are formulated from the intruder's knowledge of group principals. Using our language, we give an epistemic characterization of anonymity properties. We also present a specification of a simple anonymizing system using our theory.

"Towards a Strand Semantics for Authentication Logic,", in Electronic Notes in Theoretical Computer Science, vol. 20, eds. Stephen Brookes, Achim Jung, Michael Mislove and Andre Scedrov, 2000. PostScript, PDF

The logic BAN was developed in the late eighties to reason about authenticated key establishment protocols. It uncovered many flaws and properties of protocols, thus generating lots of attention in protocol analysis. BAN itself was also subject of much attention, and work was done examining its properties and limitations, developing extensions and alternatives, and giving it a semantics.

More recently, the strand space approach was developed. This approach gave a graph theoretic characterization of the causally possible interactions between local histories (strands) along with a term algebra to express sent and received messages. This model was designed and has been used by its authors for direct application to authentication protocol analysis. However, it has also quickly attracted the attention of many other researchers in the field as useful in connection to related work, such as model checking approaches.

Here we discuss the idea of using strand spaces as the model of computation underlying a semantics for BAN-style expressions. This will help to integrate some of the approaches to security protocol analysis and to hopefully provide BAN logics with a clearer, more useful underlying model than they have had to date.

1998

"A Formal Specification of Requirements for Payment Transactions in the SET Protocol," DRAFT for Preproceedings of Financial Cryptography 98, Anguilla, BWI, Feb. 23-26, 1998. PostScript Body, PostScript Figures, PDF Body, PDF Figures

Payment transactions in the SET (Secure Electronic Transaction) protocol are described. Requirements for SET are discussed and formally represented in a version of NPATRL (the NRL Protocol Analyzer Temporal Requirements Language). NPATRL is language for expressing generic requirements, heretofore applied to key distribution or key agreement protocols. Transaction vectors and other new constructs added to NPATRL for reasoning about SET payment transactions are described along with properties of their representation.

1996

"Language Generation and Verification in the NRL Protocol Analyzer," Proceedings of the 9th Computer Security Foundations Workshop, IEEE Computer Society Press, 1996. PostScript

The NRL Protocol Analyzer is a tool for proving security properties of cryptographic protocols, and for finding flaws if they exist. It is used by having the user first prove a number of lemmas stating that infinite classes of states are unreachable, and then performing an exhaustive search on the remaining state space. One main source of difficulty in using the tool is in generating the lemmas that are to be proved. In this paper we show how we have made the task easier by automating the generation of lemmas involving the use of formal languages.

"Analyzing the Needham-Schroeder Public Key Protocol: A Comparison of Two Approaches," Proceedings of ESORICS, Springer Verlag, To appear. PostScript

In this paper we contrast the use of the NRL Protocol Analyzer and Gavin Lowe's use of the model checker to analyze the Needham-Schroeder public key protocol. This is used as a basis to compare and contrast the two systems and to point out possible future directions for research.

"Limitations on Design Principles for Public Key Protocols," Proceedings of the 1996 IEEE Symposium on Security and Privacy, Oakland, CA, 1996, IEEE CS Press, pp. 62-73. PostScript

Recent papers have taken a new look at cryptographic protocols from the perspective of proposing design principles. For years the main approach to cryptographic protocols has been logical, and a number of papers have examined the limitations of those logics. This paper takes a similar cautionary look at the design principal approach. Limitations and exceptions are offered on some of the previously given basic design principals. The focus is primarily on public key protocols, especially on the order of signature and encryption. But, other principles are discussed as well. Apparently secure protocols that fail to meet principles are presented. Also presented are new attacks on protocols as well as previously claimed attacks which are not.

"A Formal Language for Cryptographic Protocol Requirements," Designs, Codes, and Cryptography, vol. 7, no. 1/2, pp. 27-59, 1996. PostScript, PDF

In this paper we present a formal language for specifying and reasoning about cryptographic protocol requirements. We give sets of requirements for key distribution protocols and for key agreement protocols in that language. We look at a key agreement protocol due to Aziz and Diffie that might meet those requirements and show how to specify it in the language of the NRL Protocol Analyzer. We also show how to map our formal requirements to the language of the NRL Protocol Analyzer and use the Analyzer to show that the protocol meets those requirements. In other words, we use the Analyzer to assess the validity of the formulae that make up the requirements in models of the protocol. Our analysis reveals an implicit assumption about implementations of the protocol and reveals subtleties in the kinds of requirements one might specify for similar protocols.

"A Unified Cryptographic Protocol Logic," NRL CHACS Report 5540-227, 1996. PostScript, PDF

We present a logic for analyzing cryptographic protocols. This logic is based on a unification of four of its predecessors in the BAN family of logics, namely those given in [GNY90], [AT91], [vO93b], and BAN itself [BAN89]. The logic herein captures the desirable features of its predecessors and more; nonetheless, as a logic it is relatively simple and simple to use. We also present a model-theoretic semantics, and we prove soundness for the logic with respect to that semantics. We illustrate the logic by applying it to the Needham-Schroeder protocol, revealing that BAN analysis of it may lead to inappropriate conclusions in some settings. We also use the logic to analyze two key agreement protocols, examining an attack on one of them.

1995

"Applying the Dependability Paradigm to Computer Security," Proceedings of the 1995 New Security Paradigms Workshop, To appear. PostScript

Dependability is that property of a computer system such that reliance can justifiably be placed on the service it delivers. In this paper, we contrast the different ways faults are handled in the dependability paradigm with the way they are handled in the current paradigms for secure system design. We show how the current security paradigm is generally restricted to a subset of the types of approaches used in dependability, largely concentrating on fault prevention and removal while neglecting fault tolerance and forecast, and argue that this paradigm is fast becoming obsolete. We discuss the implications of extending the security paradigm to cover the full range of options covered by dependability. In particular, we develop a rough outline of a fault model for security and show how it could be applied to better our understanding of the place of both fault tolerance and fault forecast in computer security.

"The NRL Protocol Analyzer: An Overview," Journal of Logic Programming, To appear. PostScript

The NRL Protocol Analyzer is a prototype special-purpose verification tool, written in Prolog, that has been developed for the analysis of cryptographic protocols that are used to authenticate principals and services and distribute keys in a network. In this paper we give an overview of how the Analyzer works and describe its achievements so far. We also show how our use of Prolog language benefited us in the design and implementation of the Analyzer. This is a greatly expanded version of the paper "The NRL Protocol Analyzer: An Overview, " that appeared in the proceedings of the 2nd Conference on the Practical Applications of Logic Programming.

"Integrity in Multilevel Secure Database Management Systems," in Information Security: An Integrated Collection of Essays, Marshall Abrams, Sushil Jajodia, and Harold Podell, eds., IEEE Computer Society Press, 1995, pp. 530-541

Integrity is usually considered to be at odds with security in multilevel databases. Integrity constraints enforce conditions on relations between data, while security constraints enforce separation between data. If an integrity constraint is defined over data at different security levels, a direct conflict results. However, the solution is not to sacrifice the integrity constraint altogether. Compromise solutions can often be found that guaranteed some, although not all, of the desired results of the constraint. In this paper, we will show that, by dividing the desired goals of integrity into three areas, consistency, correctness, and availablity, one often find solutions to integrity problems that achieve some, if not all, of the goals without sacrificing security.

"Inference Problems in Multilevel Secure Database Management Systems", in Information Security: An Integrated Collection of Essays, Marshall Abrams, Sushil Jajodia, and Harold Podell, eds., IEEE Computer Society Press, 1995, pp. 570-584

Inference is the process of deriving new information from known information. In multilevel database systems, the INFERENCE PROBLEM refers to the fact that the derived information can have higher sensitivity than the lower sensitivity of the information provided to the user by the system. This essay provides a survey of the state-of-the-art in the study of INFERENCE PROBLEMS. It defines and characterizes the INFERENCE PROBLEM as it relates to multilevel database systems and describe methods that have been developed for dealing with it.

"The Role of Trust in Information Integrity Protocols," Journal of Computer Security, Vol. 3, No. 2, 1994. PostScript

Paradoxically, one of the most important -- and at the same time, probably one of the least understood -- functions performed by information integrity protocols is to transfer trust from where it exists to where it is needed. Initially in any protocol, there are at least two types of trust: trust that designated participants, or groups of participants, will faithfully execute their assigned function in the protocol and trust in the integrity of the transfer mechanism(s) integral to the protocol. Consequently, almost all protocols enforce a set of restrictions as to who may exercise them -- either spelled out explicitly or left implicit in the protocol specification. In addition there may be unanticipated or even unacceptable groupings of participants who can also exercise the protocol as a result of actions taken by some of the participants reflecting trusts that exist among them. Formal methods are developed to analyze trust as a fundamental dimension in protocol analysis and proof.

"Formal Verification of Cryptographic Protocols: A Survey," Advances in Cryptology - Asiacrypt '94, LNSC 917, Springer-Verlag, 1995, pp. 133-150. PostScript

In this paper we give a survey of the state of the art in the application of formal methods to the analysis of cryptographic protocols. We attempt to outline some of the major threads of research in this area, and also to document some emerging trends.

"Fail-Stop Protocols: An Approach to Designing Secure Protocols," Preprints of the Fifth International Working Conference on Dependable Computing for Critical Applications (DCCA-5), September 1995, pp. 44-55. (Final proceedings version forthcoming from Springer-Verlag). PostScript

We present a methodology to facilitate the design and analysis of secure cryptographic protocols. We advocate the general approach, and a new avenue for research, of restricting protocol designs to well-defined practices, instead of ever increasing the complexity of protocol security analysis mechanisms to deal with every newly discovered attack and the endless variations in protocol construction. In particular, we propose a novel notion of a fail-stop protocol, which automatically halts in response to any active attack that interferes with protocol execution, thus reducing protocol security analysis to that of passive attacks only. We suggest types of protocols that are fail-stop, outline some proof techniques for them, and use examples to illustrate how the notion of a fail-stop protocol can make protocol design easier and can provide a more solid basis for some available protocol analysis methods.

1994

"Tradeoff Areas in Secure System Development", Proceedings of CSESAW '94, Naval Surface Warfare Center, July 1994. PostScript

In this paper we identify several areas in which the satisfaction of security requirements can affect the cost and performance of a system, and describe what is known about tradeoffs in these areas. The areas we investigate include both features offered by the system and the procedures that are involved in building the system.

We discuss the feasibility of quantitative assessment of security, and outline several areas in which quantitative assessment may be possible and of practical use.

We discuss the necessity and practicality of constructing a failure model of security similar to that for fault-tolerance.

In this paper we develop a model of computation for the NRL Protocol Analyzer by modifying and extending the model of computation for Burroughs, Abadi, and Needham (BAN) logic developed by Abadi and Tuttle. We use the results to point out the similarities and differences between the NRL Protocol Analyzer and BAN logic, and discuss the issues this raises with respect to the possible integration of the two.

Three experimental methods have been developed to help apply formal methods to the security verification of cryptographic protocols of the sort used for key distribution and authentication. Two of these methods are based on Prolog programs, and one is based on a general-purpose specification and verification system. All three combine algebraic with state-transition approaches. For purposes of comparison, they were used to analyze the same example protocol with a known flaw.

The NRL Protocol Analyzer is a special-purpose verification tool, written in Prolog, that has been developed for the analysis of cryptographic protocols that are used to authenticate principals and services and distribute keys in a network. In this paper we give an overview of how the Analyzer works and describe its achievements so far. We also show how our use of the Prolog language benefited us in the design and implementation of the Analyzer.

We discuss generic formal requirements for reasoning about two party key distribution protocols, using a language developed for specifying security requirements for security protocols. Typically earlier work has considered formal analysis of already developed protocols. Our goal is to present sets of formal requirements for various contexts which can be applied at the design stage as well as to existing protocols. We use a protocol analysis tool we have developed to determine whether or not a specific protocol has met some of the requirements we specified. We show how this process uncovered a flaw in the protocol and helped us refine our requirements.

This paper presents a taxonomy of replay attacks on cryptographic protocols in terms of message origin and destination. The taxonomy is independent of any method used to analyze or prevent such attacks. It is also complete in the sense that any replay attack is composed entirely of elements classified by the taxonomy. The classification of attacks is illustrated using both new and previously known attacks on protocols. The taxonomy is also used to discuss the appropriateness of particular countermeasures and protocol analysis methods to particular kinds of replays.

``On Unifying Some Cryptographic Protocol Logics,'' Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy Oakland CA May 1994 IEEE CS Press (Los Alamitos, 1994) PostScript

We present a logic for analyzing cryptographic protocols. This logic encompasses a unification of four of its predecessors in the BAN family of logics including BAN itself. We also present a model-theoretic semantics with respect to which the logic is sound. The logic herein captures all of the desirable features of its predecessors and more; nonetheless, it accomplishes this with no more axioms or rules than the simplest of its predecessors.

In this paper we present a first order epistemic logic that incorporates the essentially finite character of what is actually known by any knower. Our logic and language allows us to represent familiarity with individuals including individual situations. It is also a logic of limited awareness in the manner of [Fagin & Halpern 88]. It is adequate for the syntactic characterization of the shared-situation account of common knowledge.e presented semantics.

1993

``Adding Time to a Logic of Authentication,'' Proceedings of the First ACM Conference on Computer and Communications Security, Fairfax VA Nov. 1993 ACM Press (New York, 1993) PostScript

In [BAN89] Burrows, Abadi, and Needham presented a logic (BAN) for analyzing cryptographic protocols in terms of belief. This logic is quite useful in uncovering flaws in protocols; however, it also has produced confusion and controversy. Much of the confusion was cleared up when Abadi and Tuttle provided a semantics for a version of that logic (AT) in [AT91].

In this paper we present a protocol to show that both BAN and AT are not expressive enough to capture all of the kinds of flaws that appear to be within their scope. We then present a logic that adds temporal formalisms to AT and that is rich enough to reveal the flaws in the presented protocol; nonetheless, this logic is sound with respect to the same semantics that was given in [AT91]. Finally, we argue that any approach of this type is inadequate by itself to demonstrate the absence of such flaws. We must supplement the formal logic with semantic analysis techniques.

In [KSL92], Kehne et al. present a protocol (KSL) for key distribution. Their protocol allows for repeated authentication by means of a ticket. They also give a proof in BAN logic [BAN89] that the protocol provides the principals with a reasonable degree of trust in the authentication and key distribution. They present an optimality result that their protocol contains a minimal number of messages. Nonetheless, in [NS93] Neuman and Stubblebine present a protocol (NS) as an explicit alternative to KSL that requires one less message in the initial authentication and key distribution. One goal of this paper is to examine some of the reasons for this discrepancy. Another goal is to demonstrate possible attacks on NS. Like any attacks on cryptographic protocols, these depend on assumptions about implementation details. But, when possible they are serious: a penetrator can initiate the protocol, masquerade as another principal, obtain the session key, and even generate the session key herself. We will set out implementation assumptions required for the attacks to take place and implementation assumptions that preclude such an attack. We will also look at other protocols, including one that is not subject to this form of attack and has the same number of messages as NS. Finally, we will briefly discuss the logical analysis of these repeat authentication protocols.

In this paper we present a formal language for specifying and reasoning about cryptographic protocol requirements. We give examples of simple sets of requirements in that language. We look at two versions of a protocol that might meet those requirements and show how to specify them in the language of the NRL Protocol Analyzer. We also show how to map one of our sets of formal requirements to the language of the NRL Protocol Analyzer and use the Analyzer to show that one version of the protocol meets those requirements. In other words, we use the Analyzer as a model checker to assess the validity of the formulae that make up the requirements.

1992

"Applying Formal Methods to the Analysis of a Key Managment Protocol,'' The Journal of Computer Security," vol 1, no 1, Jan. 1992. PostScript

In this paper we develop methods for analyzing key management and authentication protocols using techniques developed for the solutions of equations in a term rewriting system. In particular, we describe a model of a class of protocols and possible attacks on those protocols as term rewriting systems, and we also describe a software tool based on a narrowing algorithm that can be used in the analysis of such protocols. We formally model a protocol and describe the results of using these techniques to analyze security properties. We show how a security flaw was found, and we also describe the verification of a corrected scheme using these techniques.

We resolve a debate over the appropriateness for cryptographic protocol analysis of formalisms representing knowledge vs. those representing belief by showing that they are equally adequate for protocol analysis on the logical level. We discuss the significance of semantics for logics of cryptographic protocols. In particular, we look at semantics as a measure of a logic and as a reasoning tool in its own right. To illustrate the value of a semantics we use the semantics given in [Abadi and Tuttle 91] to resolve a debate over an alleged flaw in BAN, the logic of [Burrows, Abadi, and Needham 89].

1991

``The Use of Logic in the Analysis of Cryptographic Protocols,'' Proceedings of the 1991 IEEE Symposium on Research in Security and Privacy, Oakland CA May 1991 IEEE CS Press (Los Alamitos CA, 1991)

Logics for cryptographic protocol analysis are discussed and a study is made of the protocol features that they are appropirate for analyzing: some are appropriate for analyzing trust, others security. The goals of Burrows, Abadi, and Needham's BAN logic are examined, and it is found that there is confusion about these. Formal semantics is explored as a reasoning tool and the importance of soundness and completeness for protocol security is discussed. The logic KPL is used to resolve a debate over an alleged flaw in BAN logic.

1990

"A Logic for the Analysis of Cryptographic Protocols", NRL Formal Report 9305, December 1990

A corrected version of the logic and semantics from "Formal Semantics for Logics of Cryptographic Protocols" is presented. Also presented are soundness and completeness proofs for the logic.

A first order, epistemic logic for representing and analyzing cryptographic protocols is presented along with an associated model-theoretic semantics. The formal language presented has distinct means to represent knowledge of an individual word, e.g., the ability to recognize or produce a decryption key, and propositional knowledge. A sample analysis of a protocol is given.

Privacy Policy