Showing 1–4 of 4 results for author: Liskov, M

Cryptographically Assured Information Flow: Assured Remote Execution

Authors: Scott L. Dyer, Christian A. Femrite, Joshua D. Guttman, Julian P. Lanson, Moses D. Liskov

Abstract: Assured Remote Execution on a device is the ability of suitably authorized parties to construct secure channels with known processes -- i.e. processes executing known code -- running on it. Assured Remote Execution requires a hardware basis including cryptographic primitives. In this paper, we show that a simple hardware-level mechanism called Cryptographically Assured Information Flow (CAIF) enab… ▽ More Assured Remote Execution on a device is the ability of suitably authorized parties to construct secure channels with known processes -- i.e. processes executing known code -- running on it. Assured Remote Execution requires a hardware basis including cryptographic primitives. In this paper, we show that a simple hardware-level mechanism called Cryptographically Assured Information Flow (CAIF) enables Assured Remote Execution. CAIF is akin to some operations in existing Trusted Execution Environments, but securely implements an ideal functionality defined in terms of logging and confidential escrow. We show how to achieve Assured Remote Execution for a wide variety of processes on a CAIF device. Cryptographic protocol analysis demonstrates our security goals are achieved even against a strong adversary that may modify our programs and execute unauthorized programs on the device. Assured Remote Execution enables useful functionality such as trustworthy remote attestation, and provides some of the support needed for secure remote reprogramming. △ Less

Submitted 20 September, 2024; v1 submitted 4 February, 2024; originally announced February 2024.

Comments: 38 pp.We are grateful to the MITRE Independent Research and Development Program for support

Formal Methods Analysis of the Secure Remote Password Protocol

Authors: Alan T. Sherman, Erin Lanus, Moses Liskov, Edward Zieglar, Richard Chang, Enis Golaszewski, Ryan Wnuk-Fink, Cyrus J. Bonyadi, Mario Yaksetig, Ian Blumenfeld

Abstract: We analyze the Secure Remote Password (SRP) protocol for structural weaknesses using the Cryptographic Protocol Shapes Analyzer (CPSA) in the first formal analysis of SRP (specifically, Version 3). SRP is a widely deployed Password Authenticated Key Exchange (PAKE) protocol used in 1Password, iCloud Keychain, and other products. As with many PAKE protocols, two participants use knowledge of a pr… ▽ More We analyze the Secure Remote Password (SRP) protocol for structural weaknesses using the Cryptographic Protocol Shapes Analyzer (CPSA) in the first formal analysis of SRP (specifically, Version 3). SRP is a widely deployed Password Authenticated Key Exchange (PAKE) protocol used in 1Password, iCloud Keychain, and other products. As with many PAKE protocols, two participants use knowledge of a pre-shared password to authenticate each other and establish a session key. SRP aims to resist dictionary attacks, not store plaintext-equivalent passwords on the server, avoid patent infringement, and avoid export controls by not using encryption. Formal analysis of SRP is challenging in part because existing tools provide no simple way to reason about its use of the mathematical expression $v + g^b \mod q$. Modeling $v + g^b$ as encryption, we complete an exhaustive study of all possible execution sequences of SRP. Ignoring possible algebraic attacks, this analysis detects no major structural weakness, and in particular no leakage of any secrets. We do uncover one notable weakness of SRP, which follows from its design constraints. It is possible for a malicious server to fake an authentication session with a client, without the client's participation. This action might facilitate an escalation of privilege attack, if the client has higher privileges than does the server. We conceived of this attack before we used CPSA and confirmed it by generating corresponding execution shapes using CPSA. △ Less

Submitted 16 March, 2020; originally announced March 2020.

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.

Comments: 53 pages

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.