Using equivalence-checking to verify robustness to denial of service

In this paper, we introduce a new security property which intends to capture the ability of a cryptographic protocol being resistant to denial of service. This property, called impassivity, is formalised in the framework of a generic value-passing process algebra, called Security Protocol Process Algebra, extended with local function calls, cryptographic primitives and special semantics features in order to cope with cryptographic protocols. Impassivity is defined as an information flow property founded on bisimulation-based non-deterministic admissible interference. A sound and complete proof method, based on equivalence-checking, for impassivity is also derived. The method extends results presented in a previous paper on admissible interference and its application to the analysis of cryptographic protocols. Our equivalence-checking method is illustrated throughout the paper on the TCP/IP connection protocol and on the 1KP secure electronic payment protocol.