Deciding security properties for cryptographic protocols. Application to key cycles

TL;DR

This paper presents a simplified decision procedure for security protocol verification, proving NP-completeness of key cycle detection in bounded sessions and applying it to authentication and timestamp protocols.

Contribution

It introduces a set of constraint simplification rules that reduce deducibility constraints to solved forms, enabling efficient decision procedures for key cycles and related security properties.

Findings

Deciding key cycles is NP-complete for bounded sessions.

The decision procedure applies to authentication and timestamp protocols.

The approach simplifies protocol verification by reducing constraints to solved forms.

Abstract

There is a large amount of work dedicated to the formal verification of security protocols. In this paper, we revisit and extend the NP-complete decision procedure for a bounded number of sessions. We use a, now standard, deducibility constraints formalism for modeling security protocols. Our first contribution is to give a simple set of constraint simplification rules, that allows to reduce any deducibility constraint system to a set of solved forms, representing all solutions (within the bound on sessions). As a consequence, we prove that deciding the existence of key cycles is NP-complete for a bounded number of sessions. The problem of key-cycles has been put forward by recent works relating computational and symbolic models. The so-called soundness of the symbolic model requires indeed that no key cycle (e.g., enc(k,k)) ever occurs in the execution of the protocol. Otherwise, stronger security assumptions (such as KDM-security) are required. We show that our decision procedure can also be applied to prove again the decidability of authentication-like properties and the decidability of a significant fragment of protocols with timestamps.