  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.
