| A Framework for Automatic Web Service Composition |
30-Apr-2009 |
23 pages |
| Authors:
Anya Kim; Myong Kang; Catherine Meadows; John Sample; Elias Ioup; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
 | Complex mission plans need to incorporate information from various sources and domains to achieve a task. This information is available through a variety of web services in the Service-Oriented Architecture (SOA), but the ability to automatically compose them into a single coherent task is not readily available. Traditional composition approaches require human-intensive involvement, making them time-consuming and error prone. Therefore, the ability to automatically or semi-automatically orchestrate web services in ... |
|
| Deriving Key Distribution Protocols and their Security Properties |
04 DEC 2006 |
|
| Authors:
Iliano Cervesato; Catherine Meadows; Dusko Pavlovic; CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
|
 | We apply the derivational method of protocol verification to key distribution protocols. This method assembles the security properties of a protocol by composing the guarantees offered by embedded fragments and patterns. It has shed light on fundamental notions such as challenge-response and fed a growing taxonomy of protocols. Here, we similarly capture the essence of key distribution, authentication time stamps and key confirmation. With these building blocks, we derive the ... |
|
| Distance Bounding Protocols: Authentication Logic Analysis and Collusion Attacks |
2006 |
21 pages |
| Authors:
Catherine Meadows; Radha Poovendran; Dusko Pavlovic; LiWu Chang; Paul Syverson; NAVAL RESEARCH LAB WASHINGTON DC
|
| Distance estimation, that is the estimate of the distance between two nodes, plays of a fundamental part in the setting up and maintenance of sensor networks. For example, a node trying to localize itself, can, if it learns its distance from three or more nodes with known locations, use multilateration to determine where it sits. This computation is a major part of many localization algorithms. Distance estimation can also be ... |
|
| Resisting Traffic Analysis on Unclassified Networks |
01 NOV 2004 |
56 pages |
| Authors:
Roger Dingledine; Nick Mathewson; Catherine Meadows; Paul Syverson; NAVAL RESEARCH LAB WASHINGTON DC
|
| While the need for data and message confidentiality is well known, the need to protect against traffic analysis on networks, including unclassified networks, is less widely recognized. Tor is a circuit-based low-latency anonymous communication service that resists traffic analysis. This second-generation Onion Routing system adds to the first-generation design with perfect forward secrecy, congestion control, directory servers, integrity checking, variable exit policies, and a practical design for rendezvous points. Tor ... |
|
| Formal Specification and Analysis of the Group Domain of Intrepretation Protocol Using NPATRL and the NRL Protocol Analyzer (Preprint) |
2004 |
40 pages |
| Authors:
Catherine Meadows; Paul Syverson; Iliano Cervesato; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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 ... |
|
| Towards a Hierarchy of Cryptographic Protocol Models |
30 OCT 2003 |
3 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| Recently there has been an increasing amount of research on 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, the author presents a brief outline of a strategy for rendering the analysis of cryptographic protocols ... |
|
| Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends |
2003 |
12 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC
|
| 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 ... |
|
| A Procedure for Verifying Security Against Type Confusion Attacks |
2003 |
12 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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 ... |
|
| A Fault-Tree Representation of NPATRL Security Requirements |
2003 |
11 pages |
| Authors:
Iliano Cervesato; Catherine Meadows; ITT INDUSTRIES INC ALEXANDRIA VA ADVANCED ENGINEERING AND SCIENCES DIV
|
| 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 ... |
|
| What Makes a Cryptographic Protocol Secure? The Evolution of Requirements Specification in Formal Cryptographic Protocol Analysis |
2003 |
13 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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 ... |
|
| Identifying Potential Type Confusion in Authenticated Messages |
2002 |
12 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC
|
| 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 ... |
|
| Environmental Requirements for Authentication Protocols |
2002 |
18 pages |
| Authors:
Ran Canetti; Catherine Meadows; Paul Syverson; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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 ... |
|
| Formalizing GDOI Group Key Management Requirements in NPATRL |
2001 |
11 pages |
| Authors:
Catherine Meadows; Paul Syverson; Iliano Cervesato; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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 ... |
|
| Dolev-Yao is no better than Machiavelli |
2000 |
7 pages |
| Authors:
Paul Syverson; Catherine Meadows; Iliano Cervesato; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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 attack-equivalent to an adversary consisting of a single dishonest principal who is only willing to ... |
|
| A Cost-Based Framework for Analysis of Denial of Service in Networks |
2000 |
25 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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 ... |
|
| Invariant Generation Techniques in Cryptographic Protocol Analysis |
2000 |
10 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC
|
| 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 ... |
|
| Extending Formal Cryptographic Protocol Analysis Techniques for Group Protocols and Low-Level Cryptographic Primitives |
2000 |
5 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| We have recently seen the development of a number of new tools for the analysis of cryptographic protocols. Many of them are based on state exploration, that is, they try to find as many paths through the protocol as possible, in the hope that, if there is an error, it will be discovered. But, since the search space offered by a cryptographic protocol is infinite, this search alone cannot guarantee ... |
|
| The MFPS XV Security Session |
01-Jan-1999 |
5 pages |
| Authors:
Catherine Meadows; Dennis Volpano; NAVAL RESEARCH LAB WASHINGTON DC
|
| Security has long been a popular application of formal methods. This is because it is a fertile source of challenging problems that are important enough to justify the effort involved in developing mathematical models and formal techniques. We are moving to a more networked world where our vital transactions depend upon our ability to communicate securely over an untrusted network and upon information and software obtained from parties about whom ... |
|
| A Formal Framework and Evaluation Method for Network Denial of Service |
1999 |
12 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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 ... |
|
| Analysis of the Internet Key Exchange Protocol Using the NRL Protocol Analyzer |
1999 |
17 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC
|
| 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 ... |
|
| CAPSL Interface for the NRL Protocol Analyzer |
1999 |
11 pages |
| Authors:
Stephen Brackin; Catherine Meadows; Jonathan Millen; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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 ... |
|
| A Formal Specification of Requirements for Payment Transactions in the SET Protocol |
24 FEB 1998 |
16 pages |
| Authors:
Catherine Meadows; Paul Syverson; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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. ... |
|
| Language Generation and Verification in the NRL Protocol Analyzer |
1996 |
15 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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 ... |
|
| A Formal Language for Cryptographic Protocol Requirements |
1996 |
31 pages |
| Authors:
Paul Syverson; Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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 Diffe 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 ... |
|
| Applying the Dependability Paradigm to Computer Security |
1995 |
6 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| Dependability is that property of a computer system such that reliance can justifiably be place on the service it delivers [Lap94]. In this paper we contrast the way 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 ... |
|
| The Role of Trust in Information Integrity Protocols |
1995 |
12 pages |
| Authors:
G. J. Simmons; Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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 NRL Protocol Analyzer: An Overview |
1995 |
20 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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 the Prolog language benefited us in the design ... |
|
| Formal Requirements for Key Distribution Protocols |
1994 |
13 pages |
| Authors:
Paul Syverson; Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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 ... |
|
| Tradeoffs in Secure System Development: An Outline |
1994 |
12 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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. We also show where these tradeoffs appear in the life cycle of a system, and show how they are affected by different kinds of security requirements. |
|
| The Need for a Failure Model for Security |
1994 |
4 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| Researchers in fault tolerance have long made use of the notion of a failure model, which describes the different ways a component in a system can fail. For example, a node can fail quietly (that is, it send out no information), it can fail with respect to timing (that is, send out information too late), it can fail arbitrarily, or it can fail maliciously. The intent of the failure model ... |
|
| A Model of Computation for the NRL Protocol Analyzer |
1994 |
7 pages |
| Authors:
Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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. |
|
| A Logical Language for Specifying Cryptographic Protocol Requirements |
1993 |
14 pages |
| Authors:
Paul Syverson; Catherine Meadows; NAVAL RESEARCH LAB WASHINGTON DC CENTER FOR HIGH ASSURANCE COMPUTING SYSTEMS (CHACS)
|
| 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. [Mea91] [Mea92] We also show how to map one of our sets of formal requirements to ... |
|
Reports by Author
