A Model for Secure Protocols and Their Compositions (extended abstract)
Nevin Heintze, J.D. Tygart · 1994
We give a formal model of protocol security. Our model allows us to reason about the security of protocols, and considers issues of beliefs of agents, time, and secrecy. We prove a composition theorem which allows us to state sufficient conditions on two secure protocols A and B such that they may be combined to form a new secure protocol C. Moreover, we give counter-examples to show that when the conditions are not met, the protocol C may not be secure. 1 Introduction What does it mean for a protocol to be secure? How can we reason about secure protocols? If we combine two existing protocols into a common protocol, what can we say about the security of the new protocol? This paper develops a family of tools for reasoning about protocol security. We adopt a model-theoretic approach to defining properties of protocol security. This allows us to describe security properties in much greater detail and precision than previous frameworks for reasoning about protocol security. One of the mo...