When is a key establishment protocol correct?
Ling Dong, Kefei Chen, Xuejia Lai, Mi Wen · Security and Communication Networks · 2009
Abstract This paper presents sufficient and necessary conditions to guarantee the security of a Key Establishment (KE) protocol based on our formalism of the belief multisets. The formalism is used to express the security of a KE protocol and to reason about beliefs in the protocol. We observe that a freshness identifier such as a nonce may not be fresh for a legitimate party in a particular protocol run, hence we distinguish a trusted freshness identifier from the commonly used freshness identifier in the sense of a participant's beliefs about the security. A central ingredient in our approach is that all the beliefs should be established on the basis of a trusted freshness identifier. The reasoning results of our approach, comparing with the security conditions, can either establish the correctness of a KE protocol when the protocol is in fact correct, or identify the absence of the security properties, which leads to the structure to construct attacks directly. Two examples, the Kerberos pair‐key agreement approach in distributed sensor networks and the Needham—Schroeder public key protocol, are given to show the usability and the efficiency of our approach. Copyright © 2009 John Wiley & Sons, Ltd.