Catherine Meadows

Víctor García, Santaigo Escobar, Catherine Meadows et al.

Formal patterns are formally specified solutions to frequently occurring distributed system problems that are generic, executable, and come with strong qualitative and/or quantitative formal guarantees. A formal pattern is a generic system transformation which transforms a usually infinite class of systems in need of the pattern's solution into enhanced versions of such systems that solve the problem in question. In this paper we demonstrate the application of formal patterns to protocol dialects. Dialects are methods for hardening protocols so as to endow them with light-weight security, especially against easy attacks that can lead to more serious ones. A lingo is a dialect's key security component, because attackers are unable to ''speak'' the lingo. A lingo's ''talk'' changes all the time, becoming a moving target for attackers. In this paper we present several formal patterns for both lingos and dialects. Lingo formal patterns can make lingos stronger by both transforming them and by composing several lingos into a stronger lingo. Dialects themselves can be obtained by the application of a single dialect formal pattern, generic on both the chosen lingo and the chosen protocol.

Damián Aparicio-Sánchez, Santiago Escobar, Catherine Meadows et al.

We present a framework suited to the analysis of cryptographic protocols that make use of time in their execution. We provide a process algebra syntax that makes time information available to processes, and a transition semantics that takes account of fundamental properties of time. Additional properties can be added by the user if desirable. This timed protocol framework can be implemented either as a simulation tool or as a symbolic analysis tool in which time references are represented by logical variables, and in which the properties of time are implemented as constraints on those time logical variables. These constraints are carried along the symbolic execution of the protocol. The satisfiability of these constraints can be evaluated as the analysis proceeds, so attacks that violate the laws of physics can be rejected as impossible. We demonstrate the feasibility of our approach by using the Maude-NPA protocol analyzer together with an SMT solver that is used to evaluate the satisfiability of timing constraints. We provide a sound and complete protocol transformation from our timed process algebra to the Maude-NPA syntax and semantics, and we prove its soundness and completeness. We then use the tool to analyze Mafia fraud and distance hijacking attacks on a suite of distance-bounding protocols.

Christopher Lynch, Andrew M. Marshall, Catherine Meadows et al.

Asymmetric unification, or unification with irreducibility constraints, is a newly developed paradigm that arose out of the automated analysis of cryptographic protocols. However, there are still relatively few asymmetric unification algorithms. In this paper we address this lack by exploring the application of automata-based unification methods. We examine the theory of xor with a homomorphism, ACUNh, from the point of view of asymmetric unification, and develop a new automata-based decision procedure. Then, we adapt a recently developed asymmetric combination procedure to produce a general asymmetric- ACUNh decision procedure. Finally, we present a new approach for obtaining a solution-generating asymmetric-ACUNh unification automaton. We also compare our approach to the most commonly used form of asymmetric unification available today, variant unification.

Fan Yang, Santiago Escobar, Catherine Meadows et al.

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. To achieve this goal, we develop and give formal semantics to a process algebra for cryptographic protocols that supports a rich taxonomy of choice primitives for composing strand spaces. In our taxonomy, deterministic and non-deterministic choices are broken down further. Non-deterministic choice can be either explicit, i.e., one of two paths is chosen, or implicit, i.e., the value of a variable is chosen non-deterministically. Likewise, deterministic choice can be either an explicit if-then-else choice, i.e., one path is chosen if a predicate is satisfied, while the other is chosen if it is not, or implicit deterministic choice, i.e., execution continues only if a certain pattern is matched. We have identified a class of choices which includes finite branching and some cases of infinite branching, which we address in this paper. We provide a bisimulation result between the expected forwards execution semantics of the new process algebra and the original symbolic backwards semantics of Maude-NPA that preserves attack reachability. We have fully integrated the process algebra syntax and its transformation into strands in Maude-NPA. We illustrate its expressive power and naturalness with various examples, and show how it can be effectively used in formal analysis. This allows users to write protocols from now on using the process syntax, which is more convenient for expressing choice than the strand space syntax, in which choice can only be specified implicitly, via two or more strands that are identical until the choice point.

Antonio González-Burgueño, Damián Aparicio, Santiago Escobar et al.

In this paper, we perform an automated analysis of two devices developed by Yubico: YubiKey, designed to authenticate a user to network-based services, and YubiHSM, Yubicos hardware security module. Both are analyzed using the Maude-NPA cryptographic protocol analyzer. Although previous work has been done applying automated tools to these devices, to the best of our knowledge there has been no completely automated analysis to date. 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. In this work, we have been able to both prove properties of YubiKey and find the known attacks on the YubiHSM, in a completely automated way beyond the capabilities of previous work in the literature.

Sonia Santiago, Santiago Escobar, Catherine Meadows et al.

Protocols do not work alone, but together, one protocol relying on another to provide needed services. Many of the problems in cryptographic protocols arise when such composition is done incorrectly or is not well understood. In this paper we discuss an extension to the Maude-NPA syntax and its operational semantics to support dynamic sequential composition of protocols, so that protocols can be specified separately and composed when desired. This allows one to reason about many different compositions with minimal changes to the specification, as well as improving, in terms of both performance and ease of specification, on an earlier composition extension we presented in [18]. We show how compositions can be defined and executed symbolically in Maude-NPA using the compositional syntax and semantics. We also provide an experimental analysis of the performance of Maude-NPA using the compositional syntax and semantics, and compare it to the performance of a syntax and semantics for composition developed in earlier research. Finally, in the conclusion we give some lessons learned about the best ways of extending narrowing-based state reachability tools, as well as comparison with related work and future plans.