Using equivalence-checking to verify robustness to denial of service

9 years 1 months ago
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. Key words: Equivalence-ch...
Stéphane Lafrance
Added 11 Dec 2010
Updated 11 Dec 2010
Type Journal
Year 2006
Where CN
Authors Stéphane Lafrance
Comments (0)