Secure Device Design via Protocol Analysis

ABSTRACT

Protocol analysis tools such as cpsa and Tamarin are designed to explore all of the behaviors possible for a protocol that uses cryptography when it interacts with an adversary as well as other compliant peers. However, the word protocol may be understood in a wide sense. Since both of those analysis tools allow modeling mutable state as well as message passing, they can be used to model, analyze, and redesign security-relevant devices. Many devices use stored values and cryptographic primitives to control boot-time behavior, access to keys, and remote attestation.

We report a design exercise in which we use cpsa to design a simple cryptographic device. It has a long-term stored boot key used to ensure that it starts executing the intended executable image. This boot image also invokes an attestation process with exclusive access to a particular signing key. We discuss a sequence of specifications for such a device with gradually improving security properties and functionality. At each step, cpsa identifies the strengths and weaknesses of the current version, and the effects of each alteration.

We highlight the choice of adversary model, showing how to use CPSA roles to model an adversary that may have partial access to device state, as an adversary would if it had the ability to install some post-boot executables.

This presentation focuses on the Protocol Verification theme of this year’s HCSS. We will identify confidentiality, integrity, and authenticity properties that the device and its protocol roles achieve. Our work on the choice of adversary model is particularly relevant to the “validation of assumptions” topic raised in the CFP. Also mentioned under this topic is the question of environment; our specifications distinguish between secure environments such as initial configurations at a secure facility, such as a manufacturer or customer may maintain, and more general communications environments. The specifications allow certain communication channels to be labeled as authentic channels or confidential channels (or both), which are two key properties a secure facility may be used to achieve.

Author

Dr. Joshua Guttman is a Senior Principal Scientist at the MITRE Corporation, and Research Professor at Worcester Polytechnic Institute.  He was educated at Princeton and the University of Chicago.  He has focused on security foundations and applications, including cryptographic protocol analysis and design, network security, operating systems security, and information flow.
Dr. Guttman has been a program chair for the IEEE Computer Security Foundations Workshop (now a symposium), the first Conference on Principles of Security and Trust at ETAPS, the Workshop on Issues in the Theory of Security, the workshop on Formal Aspects of Security and Trust, and an NSF workshop on Formal Methods for Security.

View Slides (You must register and request HCSS Community Membership to download the slides.)