Cross-Tool Semantics for Protocol Security Goals

Presented as part of the 2017 HCSS conference.

Abstract:

This talk will be based on our paper at Security Standardisation Research, and it is relevant to the HCSS theme, Industrialization of Formal Methods [4]. In particular, we focus on standardizing security protocols. We observe that protocols proposed in the standards process should be equipped with analysis using protocol analysis tools such as Maude-NPA [3], Scyther [2], CPSA [5] or ProVerif [1]. Indeed, when alternate versions of a protocol are under consideration, different tools may have been used to analyze competing proposals. How can they be compared in a scientifically meaningfully way?

Formal protocol analysis tools provide objective evidence that a protocol under standardization meets security goals, as well as counterexamples to goals it does not meet (“attacks”). Different tools are however based on different execution semantics and adversary models. If different tools are applied to alternative protocols under standardization, can formal evidence offer a yardstick to compare the results?

We propose a family of languages within first order predicate logic to formalize protocol safety goals (though not indistinguishability). Although these languages were originally designed for the strand space formalism that supports the tool CPSA, we show how to translate them to goals for the applied π calculus that supports the tool ProVerif. We give a criterion for protocols expressed in the two formalisms to correspond, and prove that if a protocol in the strand space formalism satisfies a goal, then a corresponding applied π process satisfies the translation of that goal. We show that the converse also holds for a class of goal formulas, and conjecture a broader equivalence. We also describe a compiler that, from any protocol in the strand space formalism, constructs a corresponding applied π process and the relevant goal translation.

References:

1. Bruno Blanchet. An efficient protocol verifier based on Prolog rules. In 14th Computer Security Foundations Workshop, pages 82–96. IEEE CS Press, June 2001.
2. Cas Cremers and Sjouke Mauw. Operational semantics and verification of security protocols.Springer, 2012.
3. Santiago Escobar, Catherine Meadows, and José Meseguer. Maude-NPA: Cryptographic protocol analysis modulo equational properties. In Foundations of Security Analysis and Design V, FOSAD 2007–2009 Tutorial Lectures, volume 5705 of Lecture Notes in Computer Science, pages 1–50. Springer, 2009.
4. Joshua D. Guttman, John D. Ramsdell, and Paul D. Rowe. Cross-Tool Semantics for Protocol Security Goals, pages 32–61. Springer, 2016.
5. John D. Ramsdell, Joshua D. Guttman, and Moses Liskov. CPSA: A cryptographic protocol shapes analyzer, 2016. http://hackage.haskell.org/package/cpsa.

__

Joshua Guttman is Senior Principal Scientist at the MITRE Corporation, and Research Professor at Wprcester Polytechnic Institute. He has focused on security foundations and applications, including cryptographic protocol analysis and design, network security, operating systems security, and information flow. He was educated at Princeton and the University of Chicago.