Skip to main content
main-content

Über dieses Buch

This Festschrift volume is published in honor of Catherine A. Meadows and contains essays presented at the Catherine Meadows Festschrift Symposium held in Fredericksburg, VA, USA, in May 2019.

Catherine A. Meadows has been a pioneer in developing symbolic formal verification methods and tools. Her NRL Protocol Analyzer, a tool and methodology that embodies symbolic model checking techniques, has been fruitfully applied to the analysis of many protocols and protocol standards and has had an enormous influence in the field. She also developed a new temporal logic to specify protocol properties, as well as new methods for analyzing various kinds of properties beyond secrecy such as authentication and resilience under Denial of Service (DoS) attacks and has made important contributions in other areas such as wireless protocol security, intrusion detection, and the relationship between computational and symbolic approaches to cryptography. This volume contains 14 contributions authored by researchers from Europe and North America. They reflect on the long-term evolution and future prospects of research in cryptographic protocol specification and verification.

Inhaltsverzeichnis

Frontmatter

Cathy Meadows: A Central Figure in Protocol Analysis

Abstract
This anecdotal note describes Cathy Meadow’s leadership role in formal specification and verification of cryptographic protocols. Cathy has been a central figure in protocol analysis through her significant research and successful efforts to bring researchers together to form a unified, cohesive, and effective community to design and evaluate cryptographic protocols.
Sylvan Pinsky

A Long, Slow Conversation

Abstract
Cathy has always been an inspiration for me, because of the example she has set for quality in her research work, and more personally for her interest in my own attempts in the same area. In all her professional activities, I admire her humility, energy, constructive ideas, and commitment to serving the research community.
Jon Millen

Key Reminiscences

Abstract
I offer some reminiscences about work by Cathy Meadows as well as about working with and for Cathy Meadows. I also recall cryptographic protocol properties introduced in our work in the 1990s and show their applicability to analyzing novel protocols today. Specifically, I describe a recent protocol [8] for anonymous proof of account ownership using the novel primitive of secure channel injection (SCI). And I describe how the claim of transcript privacy for a specific SCI protocol depends on an implicit and not necessarily justified assumption of key virginity. I also discuss ways to modify the protocol to achieve intended goals.
Paul Syverson

Canonical Narrowing with Irreducibility Constraints as a Symbolic Protocol Analysis Method

Abstract
This work proposes canonical constrained narrowing, a new symbolic reachability analysis technique applicable to topmost rewrite theories where the equational theory has the finite variant property. Our experiments suggest that canonical constrained narrowing is more efficient than both standard narrowing and the previously studied contextual narrowing. These results are relevant not only for Maude-NPA, but also for symbolically analyzing many other concurrent systems specified by means of rewrite theories.
Santiago Escobar, José Meseguer

Finding Intruder Knowledge with Cap-Matching

Abstract
Given two terms s and t, a substitution \(\sigma \) matches s onto t if \(s\sigma = t\). We extend the matching problem to handle \(\mathbf{Cap }\)-terms, which are constructed of function symbols from the signature and a \(\mathbf{Cap }\) operator which represents an unbounded number of applications of function symbols from the signature to a set of \(\mathbf{Cap }\)-terms. A \(\mathbf{Cap }\)-term represents an infinite number of terms. A \(\mathbf{Cap }\)-substitution maps variables to \(\mathbf{Cap }\)-terms and represents an infinite number of term substitutions. \(\mathbf{Cap }\) matching is the problem of, given a term s and a \(\mathbf{Cap }\)-term T, find a set of \(\mathbf{Cap }\)-substitutions which represents the set of substitutions that matches s onto all the terms t represented by T. We give a sound, complete and terminating algorithm for \(\mathbf{Cap }\)-matching, which has been implemented in Maude. We show how the \(\mathbf{Cap }\)-matching problem can be used to find all the messages learnable by an active intruder in a cryptographic protocol, where the \(\mathbf{Cap }\) operator represents all the possible functions that can be performed by the intruder.
Erin Hanna, Christopher Lynch, David Jaz Myers, Corey Richardson

Robust Declassification by Incremental Typing

Abstract
Security of software systems has to be preserved while they grow and change incrementally. The problem is to make the analysis of their security properties adhere to such a development. In particular we concentrate here on static type systems. Given a non-incremental type system, the algorithm we propose permits using it incrementally, so avoiding to develop new incremental versions of it. As a proof-of-concept we show how our technique permits an incremental checking of non-interference with robust declassification, starting from the classical type system by Myers, Sabelfeld and Zdancewic.
Matteo Busi, Pierpaolo Degano, Letterio Galletta

JRIF: Reactive Information Flow Control for Java

Abstract
A reactive information flow (RIF) automaton for a value v specifies (i) restrictions on uses for v and (ii) the RIF automaton for any value that might be derived from v. RIF automata thus specify how transforming a value alters restrictions for the result. As labels, RIF automata are both expressive and intuitive vehicles for describing allowed information flows. JRIF is a dialect of Java that uses RIF automata for specifying information flow control policies. The implementation of JRIF involved replacing the information flow type system of the Jif language by a RIF-based type system. JRIF demonstrates (i) the practicality and utility of RIF automata, and (ii) the ease with which an existing information flow control system can be modified to support the expressive power of RIF automata.
Elisavet Kozyri, Owen Arden, Andrew C. Myers, Fred B. Schneider

Symbolic Timed Trace Equivalence

Abstract
Intruders can infer properties of a system by measuring the time it takes for the system to respond to some request of a given protocol, that is, by exploiting time side channels. These properties may help intruders distinguish whether a system is a honeypot or concrete system helping them avoid defense mechanisms, or track a user among others violating his privacy. Observational and trace equivalence are technical machineries used for verifying whether two systems are distinguishable. Automating the check for trace equivalence suffers the state-space explosion problem. Symbolic verification is used to mitigate this problem allowing for the verification of relatively large systems. This paper introduces a novel definition of timed trace equivalence based on symbolic time constraints. Protocol verification problems can then be reduced to problems solvable by off-the-shelf SMT solvers. We implemented such machinery in Maude and carry out a number of experiments demonstrating the feasibility of our approach.
Vivek Nigam, Carolyn Talcott, Abraão Aires Urquiza

Symbolic Analysis of Identity-Based Protocols

Abstract
We show how the Tamarin tool can be used to model and reason about security protocols using identity-based cryptography, including identity-based encryption and signatures. Although such protocols involve rather different primitives than conventional public-key cryptography, we illustrate how suitable abstractions and Tamarin ’s support for equational theories can be used to model and analyze realistic industry protocols, either finding flaws or gaining confidence in their security with respect to different classes of adversaries.
Technically, we propose two models of identity-based cryptography. First, we formalize an abstract model, based on simple equations, in which verification of realistic protocols is feasible. Second, we formalize a more precise model, leveraging Tamarin ’s support for bilinear pairing and exclusive-or. This model is much closer to practical realizations of identity-based cryptography, but deduction is substantially more complex. Along the way, we point out the limits of precise modeling and highlight challenges in providing support for equational reasoning. We also evaluate our models on an industrial protocol where we find and fix flaws.
David Basin, Lucca Hirschi, Ralf Sasse

Enrich-by-Need Protocol Analysis for Diffie-Hellman

Abstract
Enrich-by-need analysis characterizes all executions of a security protocol that extend a given scenario. It computes a strongest security goal the protocol achieves in that scenario. cpsa, a Cryptographic Protocol Shapes Analyzer, implements enrich-by-need analysis.
In this paper, we show how cpsa now analyzes protocols with Diffie-Hellman key agreement (DH) in the enrich-by-need style. While this required substantial changes both to the cpsa implementation and its theory, the new version retains cpsa’s efficient and informative behavior. Moreover, the new functionality is justified by an algebraically natural model of the groups and fields which DH manipulates.
The model entails two lemmas that describe the conditions under which the adversary can deliver DH values to protocol participants. These lemmas determined how cpsa handles the new cases. The lemmas may also be of use in other approaches.
This paper is dedicated to Cathy Meadows, with warmth and gratitude.
Moses D. Liskov, Joshua D. Guttman, John D. Ramsdell, Paul D. Rowe, F. Javier Thayer

Key Agreement via Protocols

Abstract
Inspired by the ideas of no cloning and measurable degrading that quantum key agreement protocols rely on, we devise novel key agreement protocols for the classical world. Our protocols are based on identical devices that are mass produced and distributed among parties participating in the protocol. We thus use protocols a little outside their normal range and seemingly achieve the impossible by relying on certain assumptions on the devices.
Andrew William Roscoe, Lei Wang

Privacy Protocols

Abstract
Security protocols enable secure communication over insecure channels. Privacy protocols enable private interactions over secure channels. Security protocols set up secure channels using cryptographic primitives. Privacy protocols set up private channels using secure channels. But just like some security protocols can be broken without breaking the underlying cryptography, some privacy protocols can be broken without breaking the underlying security. Such privacy attacks have been used to leverage e-commerce against targeted advertising from the outset; but their depth and scope became apparent only with the overwhelming advent of influence campaigns in politics. The blurred boundaries between privacy protocols and privacy attacks present a new challenge for protocol analysis. Or maybe they do not, as the novelty is often in the eye of the observer. Cathy Meadows spearheaded and steered our research in security protocols. The methods for analyzing privacy protocols arise directly from her work.
Jason Castiglione, Dusko Pavlovic, Peter-Michael Seidel

A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols

Abstract
Catherine Meadows has played an important role in the advancement of formal methods for protocol security verification. Her insights on the use of, for example, narrowing and rewriting logic has made possible the automated discovery of new attacks and the shaping of new protocols. Meadows has also investigated other security aspects, such as, distance-bounding protocols and denial of service attacks. We have been greatly inspired by her work. This paper describes the use of Multiset Rewriting for the specification and verification of timing aspects of protocols, such as network delays, timeouts, timed intruder models and distance-bounding properties. We detail these timed features with a number of examples and describe decidable fragments of related verification problems.
Musab A. Alturki, Tajana Ban Kirigin, Max Kanovich, Vivek Nigam, Andre Scedrov, Carolyn Talcott

Belenios: A Simple Private and Verifiable Electronic Voting System

Abstract
We present the electronic voting protocol Belenios together with its associated voting platform. Belenios guarantees vote privacy and full verifiability, even against a compromised voting server. While the core of the voting protocol was already described and formally proved secure, we detail here the complete voting system from the setup to the tally and the recovery procedures.
We comment on the use of Belenios in practice. In particular, we discuss the security choices made by election administrators w.r.t. the decryption key and the delegation of some setup tasks to the voting platform.
Véronique Cortier, Pierrick Gaudry, Stéphane Glondu

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise