Kestrel Institute - Research Staff - Dusko Pavlovic

Home : Research Staff : Dusko Pavlovic : Security

Security

2009

Quantifying pervasive authentication: the case of the Hancke-Kuhn protocol --- with Catherine Meadows

Abstract

As mobile devices pervade physical space, the familiar authentication patterns are becoming insufficient: besides entity authentication, many applications require, e.g. location authentication. While many interesting and subtle protocols have been proposed and implemented to provide such strengthened authentication, there are very few proofs that such protocols satisfy the required properties.

We consider the problem of adapting the Dolev-Yao-style reasoning methods for pervasive security. We show how the notion of guards, previously used for symbolic reasoning about secrecy, can be extended into a tool for analyzing pervasive authentication. It supports a simple form of probabilistic reasoning, necessary for situations where the authentication cannot be achieved in absolute sense, and needs to be quantified. We show that extension of our protocol derivation logic, although quite modest, suffices to uncover some interesting properties of the Hancke-Kuhn distance bounding protocol, and to explain some of its deceiving simplicity.

2008

Deriving authentication for pervasive security --- with Catherine Meadows

Abstract

In this paper we discuss some of the challenges and opportunities offered to authentication by pervasive computing and discuss the work we are doing in developing formal and graphical systems for reasoning about and understanding the security of protocols in pervasive computing. We provide an example of the verification of a proximity authentication protocol that uses several different types of channels to achieve its goals.

Dynamics, robustness and fragility of trust

Abstract

Trust is often conveyed through delegation, or through recommendation. This makes the trust authorities, who process and publish the trust recommendations, into an attractive target for attacks and spoofing. In some recent empiric studies, this was shown to lead to a remarkable phenomenon of adverse selection: a greater percentage of unreliable or malicious web merchants were found among those with certain types of trust certificates, then among those without. While such findings can be attributed to a lack of diligence in trust authorities, or even to conflicts of interest, our analysis of trust dynamics suggests that the public trust networks would probably remain vulnerable even if the trust authorities were perfectly diligent. The reason is that the main processes of trust building, under reasonable modeling assumptions, naturally lead to power-law distributions of trust: the rich get richer, the trusted attract more trust. The evolutionary processes governed by such distributions, ubiquitous in nature, are known to be robust with respect to random failures, but vulnerable to adaptive attacks. We recommend some ways to decrease this vulnerability, and suggest some ideas for exploration.

2007

Distance bounding protocols: authentication logic analysis and collusion attacks --- with Catherine Meadows, Radha Poovendran, LiWu Chang and Paul Syverson

Abstract

In this paper we consider the problem of securely measuring distance between two nodes in a wireless sensor network. The problem of measuring distance has fundamental applications in both localization and time synchronization, and thus would be a prime candidate for subversion by hostile attackers. We give a brief overview and history of protocols for secure distance bounding. We also give the first full-scale formal analysis of a distance bounding protocol, and we also show how this analysis helps us to reduce message and cryptographic complexity without reducing security. Finally, we address the important open problem of collusion. We analyze existing techniques for collusion prevention, and show how they are inadequate for addressing the collusion problems in sensor networks. We conclude with some suggestions for further research.

2006

Deriving secure network protocols for enterprise services architectures --- with Matthias Anlauff and Asuman Suenbuel

Abstract

Enterprise Service Architectures are emerging as a promising way to compose Web-Services as defined by the W3C consortium, to form complex, enterprise level services. However, due to the fact that each Web-Service composition is also a protocol composition, this composition gets problematic, if security protocol mechanisms are used for the individual Web-Services, because security properties are not preserved under composition. This paper outlines the derivational approach, that on the one hand mimics the general engineering practice when combining security features, but on the other hand avoids the problems that can arise during the composition of Web-Services by using well-founded mathematical concepts. The Protocol Derivation Assistant, a tool that supports this approach, is also briefly described.

Proving authentication properties in the Protocol Derivation Assistant --- with Matthias Anlauff, Richard Waldinger and Stephen Westfold

Abstract

We present a formal framework for incremental reasoning about authentication protocols, supported by the Protocol Derivation Assistant (Pda). A salient feature of our derivational approach is that proofs of properties of complex protocols are factored into simpler proofs of properties of their components, combined with proofs that the relevant refinement and composition operations preserve the proven properties or transform them in the desired way.

In the present paper, we introduce an axiomatic theory of authentication suitable for the automatic proof of authentication properties. We describe a proof of the authentication property of a simple protocol, as derived in Pda, for which the the proof obligations have been automatically generated and discharged. Producing the proof forced us to spell out previously unrecognized assumptions, on which the correctness of the protocol depends.

Pda has support for collaboration and tool integration. It can be freely downloaded from its web site.

Deriving secrecy in key establishment protocols --- with Catherine Meadows

Abstract

Secrecy and authenticity properties of protocols are mutually dependent: every authentication is based on some secrets, and every secret must be authenticated. This interdependency is a significant source of complexity in reasoning about security. We describe a method to simplify it, by encapsulating the authenticity assumptions needed in the proofs of secrecy. This complements the method for encapsulating the secrecy assumptions in proofs of authenticity, presented in the preceding paper, presented at CSFW 2005. While logically straightforward, this idea of encapsulation in general, and the present treatment of secrecy in particular, allow formulating scalable and reusable reasoning patterns about the families of protocols of practical interest. The approach came about as a design detail in an ongoing development effort towards Protocol Derivation Assistant (Pda), a semantically based environment and toolkit for derivational approach to security.

2005

An encapsulated authentication logic for reasoning about key distribution --- with Iliano Cervesato and Catherine Meadows

Abstract

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.

A derivation system and compositional logic for security protocols --- with Anupam Datta, Ante Derek and John Mitchell

Abstract

Many authentication and key exchange protocols are built using an accepted set of standard concepts such as Diffie-Hellman key exchange, nonces to avoid replay, certificates from an accepted authority, and encrypted or signed messages. We propose a general framework for deriving security protocols from simple components, using composition, refinements, and transformations. As a case study, we examine the structure of a family of key exchange protocols that includes Station-To-Station (STS), ISO-9798-3, Just Fast Keying (JFK), IKE and related protocols, deriving all members of the family from two basic protocols. In order to associate formal proofs with protocol derivations, we extend our previous security protocol logic with preconditions, temporal assertions, composition rules, and several other improvements. Using the logic, which we prove is sound with respect to the standard symbolic model of protocol execution and attack (the “Dolev–Yao model”), the security properties of the standard signature based Challenge-Response protocol and the Diffie–Hellman key exchange protocol are established. The ISO- 9798-3 protocol is then proved correct by composing the correctness proofs of these two simple protocols. Although our current formal logic is not sufficient to modularly prove security for all of our current protocol derivations, the derivation system provides a framework for further improvements.

2004

Abstraction and Refinement in Protocol Derivation --- with Anupam Datta, Ante Derek and John Mitchell

Abstract

Protocols may be derived from initial components by composition, refinement, and transformation. Using a higher-order extension of a previous protocol logic, we present an abstraction-instantiation method for reasoning about a class of protocol refinements. The main idea is to view changes in a protocol as a combination of finding a meaningful ``protocol template" that contains function variables in messages, and producing the refined protocol as an instance of the template. Using higher-order protocol logic, we can develop a single proof for all instances of a template. A template can also be instantiated to another templates, or a single protocol may be an instance of more than one template, allowing separate protocol properties to be proved modularly. These methods are illustrated using some challenge-response and key generation protocol templates that also require adding symmetric encryption and cryptographic hash to the protocol logic. We show additional uses of the methodology and suggest future directions by exploring a design space surrounding JFK (Just Fast Keying) and related protocols from the IKE (Internet Key Exchange) family. This exploration reveals some trade-offs between authentication, identity protection, and non-repudiation; shows how counter-examples may be transferred from one protocol to another using derivation steps; and produces some interesting protocols that appear not to have been previously studied in the open literature.

Deriving, attacking and defending the GDOI protocol --- with Catherine Meadows

Abstract

As a part of a continued effort towards a logical framework for incremental reasoning about security, we attempted a derivational reconstruction of GDOI, the protocol proposed in IETF RFC 3547 for authenticated key agreement in group communication over IPsec. The main advantage of the derivational approach to protocols is that it tracks the way they are designed: by refining and composing basic protocol components --- but this time within a formal system, thus providing formal assurance of their security. Moreover, by distinguishing monotonic and compositional fragments of protocol designs, this approach facilitates tracking and formalizing of the incremental changes and modifications that complicate design process, increases reusability, and minimizes need for reverification.

While deriving GDOI, we have discovered that the simple logic, that we recently developed for deriving authentication, can also be used to prove its failures, and to generate attacks. By changing the proof goal, we have discovered an attack on GDOI that had not surfaced in the previous extensive analyses by other verification techniques. At the time of writing, we are working together with the Msec Working Group to develop a solution to this problem.

After a brief overview of the logic, we outline a derivation of GDOI, which displays its valid security properties, and the derivations of two attacks on it, which display its undesired properties. Finally, we discuss some modifications that eliminate these vulnerabilities. Their derivations suggest proofs of the desired authentication property.

2003

A compositional logic for proving security properties of protocols --- with Nancy Durgin and John Mitchell

Abstract

We present a logic for proving security properties of protocols that use nonces (randomly generated numbers that uniquely identify a protocol session) and public-key cryptography. The logic, designed around a process calculus with actions for each possible protocol step, consists of axioms about protocol actions and inference rules that yield assertions about protocols composed of multiple steps. Although assertions are written using only steps of the protocol, the logic is sound in a stronger sense: each provable assertion about an action or sequence of actions holds in any run of the protocol that contains the given actions and arbitrary additional actions by a malicious attacker. This approach lets us prove security properties of protocols under attack while reasoning only about the sequence of actions taken by honest parties to the protocol. The main security-specific parts of the proof system are rules for reasoning about the set of messages that could reveal secret data and an invariant rule called the “honesty rule”.

A derivation system for security protocols and its logical formalization --- with Anupam Datta, Ante Derek and John Mitchell

Abstract

Security protocols are often built starting from an accepted set of standard conceptual components, such as Diffie-Hellman key exchange, nonces, certificates, and encryptions or signatures. We introduce a basic framework for deriving security protocols from such simple components. We apply it to a family of key exchange protocols that includes Station-To-Station (STS), ISO-9798-3, Just Fast Keying (JFK), IKE and related protocols, deriving all members of the family from two basic protocol patterns, using a small set of refinements and protocol transformations. As initial steps toward associating logical derivations with protocol derivations, we extend a previous security protocol logic with preconditions and temporal assertions. Using this logic, we prove the security properties of the standard signature based Challenge-Response protocol and the Diffie-Hellman key exchange protocol. The ISO-9798-3 protocol is then proved correct by composing the correctness proofs of these two simple protocols.

Secure protocol composition --- with Anupam Datta, Ante Derek and John Mitchell

Abstract

This paper continues the program of research towards a derivation system for security protocols. The general idea is that complex protocols can be formally derived, starting from basic security components, using a sequence of refinements and transformations, just like logical proofs are derived starting from axioms, using proof rules and transformations. The claim is that in practice, many protocols are already derived in such a way, but informally. Capturing this practice in a suitable formalism turns out to be a considerable task.

The present paper proposes rules for composing security protocols from given security components. In general, security protocols are, of course, not compositional: information revealed by one may interfere with the security of the other. However, annotating protocol steps by pre- and post-conditions, allows secure sequential composition. Establishing that protocol components satisfy each other's invariants allows more general forms of composition, that ensure that the individually secure sub-protocols will not interact insecurely in the composite protocol.

The applicability of the method is demonstrated on modular derivations of two standard protocols, together with their simple security properties.

2002

Authentication for Mobile IPv6 --- with Anupam Datta, John Mitchell and Frederic Mueller

Abstract

We present a protocol for authenticating Mobile IPv6 connections, addressing requirements established in the relevant Internet Draft. The protocol imposes minimal computational requirements on mobile nodes, uses as few messages as possible, and may be adapted to resist denial of service attacks. Our protocol has two parts, an initialization phase and an update phase. The initialization phase can take advantage of local public-key infrastructure, a bidirectional chain of trust, or operate without prior authenticating information. Each execution of the update phase uses the shared secret established in the previous phase to maintain security of the mobile connection. We have formally verified the correctness of the protocol using the finite-state analysis tool MurPhi, which has been used previously to analyze hardware designs and security properties of several protocols.

Derivation of the JFK Protocol --- with Anupam Datta and John Mitchell

Abstract

We introduce a basic framework for deriving security protocols from simple components, like proofs are derived from axioms. As an initial case study, we derive the recently proposed key agreement protocol JFK (Just Fast Keying), starting from the basic Diffie-Hellman exchange, and the generic challenge-response scheme, and refining them by the other required security features, formalized in our derivation system by suitable refinement and transformation rules.

2001

A compositional logic for protocol correctness --- with Nancy Durgin and John Mitchell

Abstract

We present a specialized protocol logic that is built around a process language for describing the actions of a protocol. In general terms, the relation between logic and protocol is like the relation between assertions in Floyd-Hoare logic and standard imperative programs. Like Floyd-Hoare logic, our logic contains axioms and inference rules for each of the main protocol actions and proofs are protocol-directed, meaning that the outline of a proof of correctness follows the sequence of actions in the protocol. We prove that the protocol logic is sound, in a specific sense: each provable assertion about an action or sequence of actions holds in any run of the protocol, under attack, in which the given actions occur. This approach lets us prove properties of protocols that hold in all runs, while explicitly reasoning only about the sequence of actions needed to achieve this property. In particular, no explicit reasoning about the potential actions of an attacker is required.

- Back to Top -

- Home - About Kestrel - Research Staff - Current Projects - Project Archive -
- Publications - Technology Transfer - Career Opportunities - Contact Kestrel -