Joshua D. Guttman - Foundations of Security, Protocols, and Equational Reasoning: Essays Dedicated to Catherine A. Meadows

Commenced Publication in 1973

Founding and Former Series Editors:

Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen

More information about this series at http://www.springer.com/series/7410

Cover illustration: Composite Privacy Protocol: Social Networking (SNet), p. 184

This Springer imprint is published by the registered company Springer Nature Switzerland AG

The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland

Catherine A. Meadows

This volume contains the papers presented at the Catherine Meadows Festschrift Symposium held during May 2223, 2019, in Fredericksburg, Virginia.

Dr. Catherine A. Meadows, Head of the Formal Methods Group at the US Naval Research Laboratory (NRL) in Washington, D.C., has beensince the very inception of the fielda key leading researcher in formal specification and verification of cryptographic protocols. Her research ideas continue to have immense influence in shaping and advancing it.

The pervasiveness of cryptographic protocols in a massively interconnected world makes their security a direct concern, not just for governments and businesses, but also for the lives of billions of people worldwide. Formal approaches to cryptographic protocol verification are important, since even rigorous review and testing of these protocols has repeatedly failed to reveal significant vulnerabilities. The key technical point is that, even under the optimistic assumption that the cryptographic primitives used by a communication protocol cannot be broken, the protocol itself can be broken. That is, a malicious attacker can still sometimes obtain the secret information sent by an honest user without violating the protocols specification. This subversion is typically achieved by a so-called man-in-the-middle attack. Since communicationfor example, wireless or Internet communicationcan often be intercepted, an attacker can listen to various communications and maliciously participate in them, impersonating various participants at various times. In this way, the attacker can obtain correctly encrypted pieces of information, combine and use them in clever ways, and reveal protected information or obtain unauthorized capabilities. Well-tested protocols have fallen victim to subtle attacks after years of practical use, dramatically demonstrating that testing by itself is not a reliable method to ensure security. Some of Dr. Meadowss most important contributions have been precisely in the development of formal specification and verification methods and tools that can uncover such subtle attacks by a systematic formal analysis that exhaustively considers all the possible malicious actions of an attacker.

This kind of formal verification is quite challenging for at least three reasons: (1) the number of actions an attacker can perform is unbounded; (2) the number of protocol sessions an attacker can participate in to obtain and combine information from various users to mount an attack is likewise unbounded; and (3) the algebraic properties of the cryptographic functions employed by the protocol can also be used by an intruder to mount even more subtle attacks. What is challenging about issues (1)(3) is that they make it difficult to automatically verify protocols by standard model checking methods, since standard model checkers assume a finite set of reachable states, which is ruled out by both (1) and (2).

Dr. Meadows has been a pioneer in developing symbolic formal verification methods and tools that are automatic and overcome the above difficulties. Her methods can be described as a novel form of symbolic model checking of infinite-state systems that exploits the specific properties of cryptographic protocols. By using a symbolic expression to stand for a typically infinite set of concrete protocol states, both difficulties (1) and (2) can be overcome. And by reasoning symbolically about the algebraic properties of the protocols cryptographic functions using equational unification and narrowing methods, difficulty (3) can likewise be overcome. In the 1990s, Dr. Meadows first embodied these symbolic model checking techniques in her NRL Protocol Analyzer, a tool and methodology that has been fruitfully applied to the analysis of many protocols and protocol standards and has had an enormous influence in the field. Although protocol security is an undecidable problem, by using very powerful state reduction techniques based on grammars, the NRL Protocol Analyzer was able in a good number of cases to terminate its exhaustive symbolic analysis of a given protocol security property with either an actual attack or an absence of attacks that, by the exhaustive nature of the analysis, proved the desired property.