We introduce a logic for reasoning about contextual trust for web addresses, provide a Kripke semantics for it, and prove its soundness under reasonable assumptions about principals' policies. Self-Authenticating Traditional Addresses (SATAs) are valid DNS addresses or URLs that are generally meaningful—to both humans and web infrastructure—and contain a commitment to a public key in the address itself. Trust in web addresses is currently established via domain name registration, TLS certificates, and other hierarchical elements of the internet infrastructure. SATAs support such structural roots of trust but also complementary contextual roots associated with descriptive properties. The existing structural roots leave web connections open to a variety of well-documented and significant hijack vulnerabilities. Contextual trust roots provide, among other things, stronger resistance to such vulnerabilities. We also consider labeled SATAs, which include descriptive properties such as that a SATA is an address for a news organization, a site belonging to a particular government or company, a site with information about a certain topic, etc. Our logic addresses both trust in the bound together identity of the address and trust in the binding of labels to it. Our logic allows reasoning about delegation of trust with respect to specified labels, relationships between labels that provide more or less specific information, and the interaction between these two aspects. In addition to soundness, we prove that if a principal trusts a particular identity (possibly with label), then either this trust is initially assumed, or there is a trust chain of delegations to this from initial trust assumptions. We also present an algorithm that effectively derives all possible trust statements from the set of initial trust assumptions and show it to be sound, complete, and terminating.

The problem of covert communication via computer systems is almost as old as the problem of computer security itself. In the earliest years, covert communication was seen as mainly as a theoretical problem. But as computer systems have become more complex and ubiquitous, covert communication has begun to see practical use, particularly in the last two decades (see, e.g. Mazurcyk et al. in [MW19].) In this talk I will be reporting on the work we have been doing at NRL on evaluating the impact that existing research on the asymptotic behavior on covert channels has on embeddings in real-world channels.

We perform an automated analysis of two devices developed by Yubico: YubiKey, de- signed to authenticate a user to network-based services, and YubiHSM, Yubico’s hardware security module. Both are analyzed using the Maude-NPA cryptographic protocol an- alyzer. Although previous work has been done applying formal tools to these devices, there has not been any completely automated analysis. This is not surprising, because both YubiKey and YubiHSM, which make use of cryptographic APIs, involve a number of complex features: (i) discrete time in the form of Lamport clocks, (ii) a mutable memory for storing previously seen keys or nonces, (iii) event-based properties that require an analysis of sequences of actions, and (iv) reasoning modulo exclusive-or. Maude-NPA has provided support for exclusive-or for years but has not provided support for the other three features, which we show can also be supported by using constraints on natural numbers, protocol composition and reasoning modulo associativity. In this work, we have been able to automatically prove security properties of YubiKey and find the known at- tacks on the YubiHSM, in both cases beyond the capabilities of previous work using the Tamarin Prover due to the need of auxiliary user-defined lemmas and limited support for exclusive-or. Tamarin has recently been endowed with exclusive-or and we have rewritten the original specification of YubiHSM in Tamarin to use exclusive-or, confirming that both attacks on YubiHSM can be carried out by this recent version of Tamarin.

Roles in cryptographic protocols do not always have a linear execution, but may include choice points causing the protocol to continue along different paths. In this paper we address the problem of representing choice in the strand space model of cryptographic protocols, particularly as it is used in the Maude-NPA cryptographic protocol analysis tool.

Recent advances in the automated analysis of cryptographic protocols have aroused new interest in the practical application of unification modulo theories, especially theories that describe the algebraic properties of cryptosystems. However, this application requires unification algorithms that can be easily implemented and easily extended to combinations of different theories of interest. In practice this has meant that most tools use a version of a technique known as variant unification. This requires, among other things, that the theory be decomposable into a set of axioms B and a set of rewrite rules R such that R has the finite variant property with respect to B. Most theories that arise in cryptographic protocols have decompositions suitable for variant unification, but there is one major exception: the theory that describes encryption that is homomorphic over an Abelian group.

A number of new cryptographic protocols are being designed to secure applications such as video-conferencing and electronic voting. Many of them rely upon cryptographic functions with complex algebraic properties that must be accounted for in order to be correctly analyzed by automated tools. Maude-NPA is a cryptographic protocol analysis tool based on narrowing and typed equational unification which takes into account these algebraic properties. It has already been used to analyze protocols involving bounded associativity, modular exponentiation, and exclusive-or. All of the above can be handled by the same general variant-based equational unification technique. However, there are important properties, in particular homomorphic encryption, that cannot be handled by variant-based unification in the same way. In these cases the best available approach is to implement specialized unification algorithms and combine them within a modular framework. In this paper we describe how we apply this approach within Maude-NPA, with respect to encryption homomorphic over a free operator. We also describe the use of Maude-NPA to analyze several protocols using such an encryption operation. To the best of our knowledge, this is the first implementation of homomorphic encryption of any sort in a tool for verifying the security of a protocol in the presence of active attackers.

No abstract available.

In this paper, we show how we can increase the ease of reading and writing security requirements for cryptographic protocols at the Dolev-Yao level of abstraction by developing a visual language based on fault trees. We develop such semantics for a subset of NRL protocol analyzer temporal requirements language (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. Other examples involve a property of Kerberos 5 and a visual account of the requirements in Lowe's authentication hierarchy.

Authentication and secrecy properties are proved by very different methods: the former by local reasoning, leading to matching knowledge of all principals about the order of their actions, the latter by global reasoning towards the impossibility of knowledge of some data. Hence, proofs conceptually decompose in two parts, each encapsulating the other as an assumption. From this observation, we develop a simple logic of authentication that encapsulates secrecy requirements as assumptions. We apply it within the derivational framework to derive a large class of key distribution protocols based on the authentication properties of their components.

We study the problem of characterizing the wormhole attack, an attack that can be mounted on a wide range of wireless network protocols without compromising any cryptographic quantity or network node. A wormhole, in essence, creates a communication link between an origin and a destination point that could not exist with the use of the regular communication channel. Hence, a wormhole modifies the connectivity matrix of the network, and can be described by a graph abstraction of the ad hoc network. Making use of geometric random graphs induced by the communication range constraint of the nodes, we present the necessary and sufficient conditions for detecting and defending against wormholes. Using our theory, we also present a defense mechanism based on local broadcast keys. We believe our work is the first one to present analytical calculation of the probabilities of detection. We also present simulation results to illustrate our theory.

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 analysi

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., 2000) 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 attacks 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.

The history of the application of formal methods to cryptographic protocol analysis spans over 20 years and 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 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.

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.

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 fo

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 than the ones for which they were developed. 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.

Formal methods have been successfully applied to exceedingly abstract system specifications to verify high level security properties such as authentication, key exchange, and fail-safe revocation. Furthermore, considerable research exists on evaluating particular ciphers and secure hash functions used to implement high level security properties. However, verifying that less abstract system specifications satisfy low level security properties has been largely impractical. This is evidenced by innumerable system vulnerabilities where high level properties are not attained due to failed assumptions of low level properties. This paper presents ongoing work on investigating known pairs and chosen text using the NRL Protocol Analyzer. We give a formal characterization of known and chosen pairs, and translate it to necessary and sufficiency conditions in the NRL Protocol Analyzer model. It is the first work the authors are aware of automatically discovering known-pair and chosen-text attacks. We describe the use of the analyzer to rediscover attacks, to find new variants of attacks on an early version of the ESP protocol, and to show how our experience in using it has led us to refine our model. This was the first use of the Analyzer to model protocols at such a low level of abstraction.

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 themselves. 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.

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.

In the last year or so, research in the formal analysis of cryptographic protocols has matured to the point where researchers are going beyond the mechanics of verification and considering the problem of providing specification languages that make it easier to specify protocols for analysis. A number of different approaches are being applied. Some are modifying existing formal specification languages, while others are implementing languages that are closely based on existing informal specification styles. Likewise, some are implementing languages that are closely tied to existing tools, while others are implementing toolindependent languages. An effort is also underway to develop a common language, CAPSL, that will serve as an interface to other tools and languages. The purpose of this panel is to bring together those who are working on this problem to compare notes and explore current issues. Some of the questions we will consider are: 1.

This paper describes three paradigms in computer security in terms of how they relate to the existing infrastructure: by existing within it, replacing it, or by extending it or replacing only small portions. We identify the third as the most desirable, and discuss some of the implications of this approach. 1

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 test easier by automating the generation of lemmas involving the use of formal languages.

Dependability is that property of a computer system such that reliance can justifiably be place on the service it delivers. 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 in dependability, largely concentrating on fault prevention and removal while neglecting fault tolerance and forecasting, and we 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 forecasting in computer security.

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 tha t 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.

We develop a model of computation for the NRL Protocol Analyzer by modifying and extending the model of computation for Burrows, Abadi, and Needham (BAN) logic (M. Burrows et al., 1990) developed by M. Abadi and M. Tuttle (1991). 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.>

Article Free Access Share on An outline of a taxonomy of computer security research and development Author: Catherine Meadows Naval Research Laboratory, Code 5543, Washington, D.C. Naval Research Laboratory, Code 5543, Washington, D.C.View Profile Authors Info & Claims NSPW '92-93: Proceedings on the 1992-1993 workshop on New security paradigmsAugust 1993 Pages 33–35https://doi.org/10.1145/283751.283770Online:03 August 1993Publication History 9citation363DownloadsMetricsTotal Citations9Total Downloads363Last 12 Months6Last 6 weeks3 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

A formal language is presented for specifying and reasoning about cryptographic protocol requirements. Examples of simple sets of requirements in that language are given. The authors examine two versions of a protocol that might meet those requirements and show how to specify them in the language of the NRL Protocol Analyzer. They also show how to map one of the 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. The Analyzer is used as a model checker to assess the validity of the formulas that make up the requirements.>

Information flow models are usually conceived in terms of requirements on system traces, while verification that a system satisfies information flow requirements is usually done in terms of a state machine specification. The necessary translation from one model to another may result in a loss of understandability and expressiveness. J. McLean (JACM, Vol.31, no.3, pp.600-627, July 1984) showed how a language based on traces of procedure calls may be used to reason about security, and how one may prove that a program satisfies a specification written in that language. The language that he uses, however, does not easily lend itself to specification of composition of communicating processes. The present work modifies the language so that it is possible to specify the composition of systems. Several different information flow properties analogous to properties that have been defined for other systems, along with their composability, are defined and discussed.>

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 a

The author gives a brief description of the NRL protocol analysis tool, and contrasts its approach with other approaches. The NRL protocol analysis tool was developed in order to assist in security proofs for protocols. However, it has also proved to be useful in pointing out previously undiscovered flaws in already published protocols. The successes using the protocol analysis tool suggests, that in many cases a hybrid approach, relying upon human intuition when possible, and providing mechanical assistance when necessary, will provide the most practical advantage.>

Describes a formal specification language and verification technique for analyzing key management protocols. A prototype verification tool that can be used to apply this technique is introduced. A protocol intended for use in the management of resource sharing, is formally specified and verified, and it is shown how the use of the considered techniques led to the discovery of a flaw that could be exploited by an intruder to convince a user of the system that he has obtained a service when he actually has not.>

The author extends a security model and specification language for key distribution protocols which describes protocols algebraically in terms of term-rewriting systems to include certain kinds of partial knowledge available to a penetrator. She also shows how the model describes the actions by which a penetrator takes advantage of partial knowledge, and gives an example of a protocol specified in the language.>

It is shown how the Brewer-Nash Chinese wall model can be extended to a policy for handling the aggregation problem in a multilevel context. A lattice-based information flow policy that can be integrated into both the multilevel and Drewer-Nash context is derived. This information flow policy is used to develop a security policy described in terms of labeled subjects accessing labeled objects that will make it possible to construct a system that prevents users from accessing aggregates that they are not cleared to see.>

The author develops methods for analyzing cryptographic protocols using techniques developed for the solutions of equations in a term rewriting system. In particular, she describes a model of a class of cryptographic protocols and possible attacks on those protocols as term rewriting systems. She also describes a software tool based on the narrowing algorithm that can be used in the analysis of such protocols. Finally, she uses the tool in the analysis of a simple protocol and outlines ways in which the tool might be improved to provide greater assistance in the analysis of more complex protocols.>

In this paper we set forth a simple and efficient algorithm for managing replicated data in a decentralized distributed system, which allows for inserts, deletes, updates, and synonyms and which achieves a high degree of availability in the face of node or communication failures. We focus on the approach developed recently by Fischer and Michael and exploit the knowledge of the semantics of the database operations.

The integrity lock architecture provides a means of constructing a secure database management system with a relatively small amount of trusted code, using a trusted filter which verifies the integrity of security labels on data from an untrusted DBMS by computing cryptographic checksums. However, since the trusted filter can only check whether or not an individual item of data has been tampered with, and not whether or not that item is a correct answer to a particular database query, a covert channel exists through which a Trojan Horse in the DBMS can leak classified information by encoding it in various incorrect (but unclassified) answers to seemingly innocuous queries. in this paper we discuss a possible solution to this covert channel problem for message systems.

The problem of authentication of mutually suspicious parties is one that is becoming more and more important with the proliferation of distributed systems. In this paper we describe a protocol, based on the difficulty of finding discrete logarithms over finite fields, by which users can verify whether they have matching credentials without revealing their credentials to each other unless there is a match. This protocol requires a trusted third party, but does not require it to be available to the users except when they sign up for the system. Thus it is useful in situations in which a trusted third party exists but is not available to all users at all times.

The problem of authentication of mutually suspicious parties is one that is becoming more and more important with the proliferation of distributed systems. In this paper we construct a protocol in which users can verify whether they have matching credentials without revealing their credentials to each other unless there is a match. Thk protocol requires a trusted third party, but does not require it to be available to the users except when they sign up for the system. Thus it is useful in situations in which a trusted third party exists, but is not available to all users at all times.

Davida, Wells and Kam used the Chinese Remainder Theorem to construct an encryption system allowing access to individual data fields of a record in a relational database. Their system is public-key in the sense that the read and write keys of a given data field are different. In this paper we present a database encryption system based on ideas similar to theirs. It is not public key, but has some other useful features. It makes possible the computation of averages and other statistics pertinent to unencrypted data, but it uses only encrypted data in the computation.