The verification of security protocols is essential, in order to ensure the absence of potential attacks. However, verification results are only valid with respect to the assumptions under which the verification was performed. These assumptions are often hidden and are difficult to identify, making it unclear whether a given protocol is safe to deploy into a particular environment. Rely/guarantee provides a mechanism for abstractly reasoning about the interference from the environment. Using this approach, the assumptions are made clear and precise. This paper investigates this approach on the Needham-Schroeder Public Key protocol, showing that the technique can effectively uncover the assumptions under which the protocol can withstand attacks from intruders.

翻译：为确保不存在潜在攻击，安全协议的验证至关重要。然而，验证结果仅在验证所依据的假设条件下才有效。这些假设通常被隐藏且难以识别，导致难以判断特定协议在给定环境中部署是否安全。Rely/guarantee提供了一种对环境干扰进行抽象推理的机制。通过该方法，假设条件得以清晰精确地呈现。本文以Needham-Schroeder公钥协议为例对该方法进行研究，表明该技术能有效揭示协议抵御攻击者攻击所需的假设条件。