-
Evidence Tampering and Chain of Custody in Layered Attestations
Authors:
Ian D. Kretz,
Clare C. Parran,
John D. Ramsdell,
Paul D. Rowe
Abstract:
In distributed systems, trust decisions are made on the basis of integrity evidence generated via remote attestation. Examples of the kinds of evidence that might be collected are boot time image hash values; fingerprints of initialization files for userspace applications; and a comprehensive measurement of a running kernel. In layered attestations, evidence is typically composed of measurements o…
▽ More
In distributed systems, trust decisions are made on the basis of integrity evidence generated via remote attestation. Examples of the kinds of evidence that might be collected are boot time image hash values; fingerprints of initialization files for userspace applications; and a comprehensive measurement of a running kernel. In layered attestations, evidence is typically composed of measurements of key subcomponents taken from different trust boundaries within a target system. Discrete measurement evidence is bundled together for appraisal by the components that collectively perform the attestation.
In this paper, we initiate the study of evidence chain of custody for remote attestation. Using the Copland attestation specification language, we formally define the conditions under which a runtime adversary active on the target system can tamper with measurement evidence. We present algorithms for identifying all such tampering opportunities for given evidence as well as tampering "strategies" by which an adversary can modify incriminating evidence without being detected. We then define a procedure for transforming a Copland-specified attestation into a maximally tamper-resistant version of itself. Our efforts are intended to help attestation protocol designers ensure their protocols reduce evidence tampering opportunities to the smallest, most trustworthy set of components possible.
△ Less
Submitted 31 January, 2024;
originally announced February 2024.
-
Report on the First HIPstIR Workshop on the Future of Information Retrieval
Authors:
Laura Dietz,
Bhaskar Mitra,
Jeremy Pickens,
Hana Anber,
Sandeep Avula,
Asia Biega,
Adrian Boteanu,
Shubham Chatterjee,
Jeff Dalton,
Shiri Dori-Hacohen,
John Foley,
Henry Feild,
Ben Gamari,
Rosie Jones,
Pallika Kanani,
Sumanta Kashyapi,
Widad Machmouchi,
Matthew Mitsui,
Steve Nole,
Alexandre Tachard Passos,
Jordan Ramsdell,
Adam Roegiest,
David Smith,
Alessandro Sordoni
Abstract:
The vision of HIPstIR is that early stage information retrieval (IR) researchers get together to develop a future for non-mainstream ideas and research agendas in IR. The first iteration of this vision materialized in the form of a three day workshop in Portsmouth, New Hampshire attended by 24 researchers across academia and industry. Attendees pre-submitted one or more topics that they want to pi…
▽ More
The vision of HIPstIR is that early stage information retrieval (IR) researchers get together to develop a future for non-mainstream ideas and research agendas in IR. The first iteration of this vision materialized in the form of a three day workshop in Portsmouth, New Hampshire attended by 24 researchers across academia and industry. Attendees pre-submitted one or more topics that they want to pitch at the meeting. Then over the three days during the workshop, we self-organized into groups and worked on six specific proposals of common interest. In this report, we present an overview of the workshop and brief summaries of the six proposals that resulted from the workshop.
△ Less
Submitted 20 December, 2019;
originally announced December 2019.
-
Homomorphisms and Minimality for Enrich-by-Need Security Analysis
Authors:
Daniel J. Dougherty,
Joshua D. Guttman,
John D. Ramsdell
Abstract:
Cryptographic protocols are used in different environments, but existing methods for protocol analysis focus only on the protocols, without being sensitive to assumptions about their environments. LPA is a tool which analyzes protocols in context. LPA uses two programs, cooperating with each other: CPSA, a well-known system for protocol analysis, and Razor, a model-finder based on SMT technology.…
▽ More
Cryptographic protocols are used in different environments, but existing methods for protocol analysis focus only on the protocols, without being sensitive to assumptions about their environments. LPA is a tool which analyzes protocols in context. LPA uses two programs, cooperating with each other: CPSA, a well-known system for protocol analysis, and Razor, a model-finder based on SMT technology. Our analysis follows the enrich-by-need paradigm, in which models of protocol execution are generated and examined. The choice of which models to generate is important, and we motivate and evaluate LPA's strategy of building minimal models. "Minimality" can be defined with respect to either of two preorders, namely the homomorphism preorder and the embedding preorder (i.e. the preorder of injective homomorphisms); we discuss the merits of each. Our main technical contributions are algorithms for building homomorphism-minimal models and for generating a set-of-support for the models of a theory, in each case by scripting interactions with an SMT solver.
△ Less
Submitted 19 April, 2018;
originally announced April 2018.
-
Enrich-by-need Protocol Analysis for Diffie-Hellman (Extended Version)
Authors:
Moses D. Liskov,
Joshua D. Guttman,
John D. Ramsdell,
Paul D. Rowe,
F. Javier Thayer
Abstract:
Enrich-by-need protocol analysis is a style of symbolic protocol analysis that characterizes all executions of a protocol that extend a given scenario. In effect, it computes a strongest security goal the protocol achieves in that scenario. CPSA, a Cryptographic Protocol Shapes Analyzer, implements enrich-by-need protocol analysis.
In this paper, we describe how to analyze protocols using the Di…
▽ More
Enrich-by-need protocol analysis is a style of symbolic protocol analysis that characterizes all executions of a protocol that extend a given scenario. In effect, it computes a strongest security goal the protocol achieves in that scenario. CPSA, a Cryptographic Protocol Shapes Analyzer, implements enrich-by-need protocol analysis.
In this paper, we describe how to analyze protocols using the Diffie-Hellman mechanism for key agreement (DH) in the enrich-by-need style. DH, while widespread, has been challenging for protocol analysis because of its algebraic structure. DH essentially involves fields and cyclic groups, which do not fit the standard foundational framework of symbolic protocol analysis. By contrast, we justify our analysis via an algebraically natural model.
This foundation makes the extended CPSA implementation reliable. Moreover, it provides informative and efficient results.
An appendix explains how unification is efficiently done in our framework.
△ Less
Submitted 16 April, 2018;
originally announced April 2018.
-
Formal Support for Standardizing Protocols with State
Authors:
Joshua D. Guttman,
Moses D. Liskov,
John D. Ramsdell,
Paul D. Rowe
Abstract:
Many cryptographic protocols are designed to achieve their goals using only messages passed over an open network. Numerous tools, based on well-understood foundations, exist for the design and analysis of protocols that rely purely on message passing. However, these tools encounter difficulties when faced with protocols that rely on non-local, mutable state to coordinate several local sessions.…
▽ More
Many cryptographic protocols are designed to achieve their goals using only messages passed over an open network. Numerous tools, based on well-understood foundations, exist for the design and analysis of protocols that rely purely on message passing. However, these tools encounter difficulties when faced with protocols that rely on non-local, mutable state to coordinate several local sessions.
We adapt one of these tools, {\cpsa}, to provide automated support for reasoning about state. We use Ryan's Envelope Protocol as an example to demonstrate how the message-passing reasoning can be integrated with state reasoning to yield interesting and powerful results.
Keywords: protocol analysis tools, stateful protocols, TPM, PKCS#11.
△ Less
Submitted 24 September, 2015;
originally announced September 2015.
-
A Hybrid Analysis for Security Protocols with State
Authors:
John D. Ramsdell,
Daniel J. Dougherty,
Joshua D. Guttman,
Paul D. Rowe
Abstract:
Cryptographic protocols rely on message-passing to coordinate activity among principals. Each principal maintains local state in individual local sessions only as needed to complete that session. However, in some protocols a principal also uses state to coordinate its different local sessions. Sometimes the non-local, mutable state is used as a means, for example with smart cards or Trusted Platfo…
▽ More
Cryptographic protocols rely on message-passing to coordinate activity among principals. Each principal maintains local state in individual local sessions only as needed to complete that session. However, in some protocols a principal also uses state to coordinate its different local sessions. Sometimes the non-local, mutable state is used as a means, for example with smart cards or Trusted Platform Modules. Sometimes it is the purpose of running the protocol, for example in commercial transactions.
Many richly developed tools and techniques, based on well-understood foundations, are available for design and analysis of pure message-passing protocols. But the presence of cross-session state poses difficulties for these techniques.
In this paper we provide a framework for modeling stateful protocols. We define a hybrid analysis method. It leverages theorem-proving---in this instance, the PVS prover---for reasoning about computations over state. It combines that with an "enrich-by-need" approach---embodied by CPSA---that focuses on the message-passing part. As a case study we give a full analysis of the Envelope Protocol, due to Mark Ryan.
△ Less
Submitted 16 June, 2014; v1 submitted 15 April, 2014;
originally announced April 2014.
-
Proving Security Goals With Shape Analysis Sentences
Authors:
John D. Ramsdell
Abstract:
The paper that introduced shape analysis sentences presented a method for extracting a sentence in first-order logic that completely characterizes a run of CPSA. Logical deduction can then be used to determine if a security goal is satisfied.
This paper presents a method for importing shape analysis sentences into a proof assistant on top of a detailed theory of strand spaces. The result is a se…
▽ More
The paper that introduced shape analysis sentences presented a method for extracting a sentence in first-order logic that completely characterizes a run of CPSA. Logical deduction can then be used to determine if a security goal is satisfied.
This paper presents a method for importing shape analysis sentences into a proof assistant on top of a detailed theory of strand spaces. The result is a semantically rich environment in which the validity of a security goal can be determined using shape analysis sentences and the foundation on which they are based.
△ Less
Submitted 14 March, 2014;
originally announced March 2014.
-
An Analysis of the CAVES Attestation Protocol using CPSA
Authors:
John D. Ramsdell,
Joshua D. Guttman,
Jonathan K. Millen,
Brian O'Hanlon
Abstract:
This paper describes the CAVES attestation protocol and presents a tool-supported analysis showing that the runs of the protocol achieve stated goals. The goals are stated formally by annotating the protocol with logical formulas using the rely-guarantee method. The protocol analysis tool used is the Cryptographic Protocol Shape Analyzer.
This paper describes the CAVES attestation protocol and presents a tool-supported analysis showing that the runs of the protocol achieve stated goals. The goals are stated formally by annotating the protocol with logical formulas using the rely-guarantee method. The protocol analysis tool used is the Cryptographic Protocol Shape Analyzer.
△ Less
Submitted 2 July, 2012;
originally announced July 2012.
-
Deducing Security Goals From Shape Analysis Sentences
Authors:
John D. Ramsdell
Abstract:
Guttman presented a model-theoretic approach to establishing security goals in the context of Strand Space theory. In his approach, a run of the Cryptographic Protocol Shapes Analyzer (CPSA) produces models that determine if a goal is satisfied. This paper presents a method for extracting a sentence that completely characterizes a run of CPSA. Logical deduction can then be used to determine if a g…
▽ More
Guttman presented a model-theoretic approach to establishing security goals in the context of Strand Space theory. In his approach, a run of the Cryptographic Protocol Shapes Analyzer (CPSA) produces models that determine if a goal is satisfied. This paper presents a method for extracting a sentence that completely characterizes a run of CPSA. Logical deduction can then be used to determine if a goal is satisfied. This method has been implemented and is available to all.
△ Less
Submitted 5 February, 2018; v1 submitted 2 April, 2012;
originally announced April 2012.
