Joshua D. Guttman

Will Thomas, Logan Schmalz, Adam Petz et al.

Attestation means providing evidence that a remote target system is worthy of trust for some sensitive interaction. Although attestation is already used in network access control, security management, and trusted execution environments, it mainly concerns only a few system components. A clever adversary might manipulate these shallow attestations to mislead the relying party. Reliable attestations require layering. We construct attestations whose layers report evidence about successive components of the target system. Reliability also requires structuring the target system so only a limited set of components matters. We show how to structure an example system for reliable attestations despite a well-defined, relatively strong adversary. It is based on widely available hardware, such as Trusted Platform Modules, and software, such as Linux with SELinux. We isolate our principles in a few maxims that guide system development. We provide a cogent analysis of our mechanisms against our adversary model, as well as an empirical appraisal of the resulting system. We also identify two improvements to the mechanisms so attestation can succeed against strengthened adversaries. The performance burden of our attestation is negligible, circa 1.3 percent. After our first example, we vary our application level, and then also its underlying hardware anchor to use confidential computing with AMD's SEV-SNP. The same maxims help us achieve trustworthy attestations.

Daniel J. Dougherty, Joshua D. Guttman, John D. Ramsdell

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.

Moses D. Liskov, Joshua D. Guttman, John D. Ramsdell et al.

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.

Joshua D. Guttman, Moses D. Liskov, John D. Ramsdell et al.

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.

Joshua D. Guttman, Paul D. Rowe

We view a distributed system as a graph of active locations with unidirectional channels between them, through which they pass messages. In this context, the graph structure of a system constrains the propagation of information through it. Suppose a set of channels is a cut set between an information source and a potential sink. We prove that, if there is no disclosure from the source to the cut set, then there can be no disclosure to the sink. We introduce a new formalization of partial disclosure, called *blur operators*, and show that the same cut property is preserved for disclosure to within a blur operator. This cut-blur property also implies a compositional principle, which ensures limited disclosure for a class of systems that differ only beyond the cut.

John D. Ramsdell, Daniel J. Dougherty, Joshua D. Guttman et al.

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.

John D. Ramsdell, Joshua D. Guttman, Jonathan K. Millen et al.

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.

Daniel J. Dougherty, Joshua D. Guttman

We extend symbolic protocol analysis to apply to protocols using Diffie-Hellman operations. Diffie-Hellman operations act on a cyclic group of prime order, together with an exponentiation operator. The exponents form a finite field. This rich algebraic structure has resisted previous symbolic approaches. We work in an algebra defined by the normal forms of a rewriting theory (modulo associativity and commutativity). These normal forms allow us to define our crucial notion of indicator, a vector of integers that summarizes how many times each secret exponent appears in a message. We prove that the adversary can never construct a message with a new indicator in our adversary model. Using this invariant, we prove the main security goals achieved by several different protocols that use Diffie-Hellman operators in subtle ways. We also give a model-theoretic justification of our rewriting theory: the theory proves all equations that are uniformly true as the order of the cyclic group varies.