Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols

Nisansala P. Yatapanage, Cliff B. Jones

TL;DR

This paper investigates the reliance/guarantee 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.

Abstract

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.

Using Rely/Guarantee to Pinpoint Assumptions underlying Security Protocols

TL;DR

This paper investigates the reliance/guarantee 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.

Abstract

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.
Paper Structure (15 sections, 6 theorems, 1 equation, 2 figures)

This paper contains 15 sections, 6 theorems, 1 equation, 2 figures.

Table of Contents

  1. Introduction
  2. Rely-guarantee thinking
  3. Protocols
  4. The Needham-Schroeder protocol proposal
  5. Protocol specification
  6. Optimistic specification (postponing encryption)
  7. Abstract state
  8. Specification
  9. Pseudo-code
  10. Correctness argument
  11. Lowe's analysis
  12. Lowe's attack and "correction"
  13. Specifying the extra check
  14. Encryption introduced as a reification
  15. Conclusion and Related Work

Key Result

lemma 1

Synchronisation of the two threads in Fig. F-dCode follows from the semantics of the message $\kw{send/rcv}$ statements.

Figures (2)

  • Figure 1: Specification for NS with users $from/to$ conforming to the protocol
  • Figure 2: Distributed code for N-S

Theorems & Definitions (6)

  • lemma 1
  • lemma 2
  • lemma 3
  • lemma 4
  • lemma 5
  • lemma 6