Using Admissible Interference to Detect Denial of Service Vulnerabilities

Meadows recently proposed a formal cost-based framework for analysis of denial of service. It was showed how some principles that have already been used to make cryptographic protocols more resistant to denial of service by trading off the cost to defender against the cost to the attacker can be formalized. The first contribution of this paper is to introduce a new security property called impassivity which intends to capture the ability of a protocol to achieve these goals in the framework of a generic value-passing process algebra called Security Process Algebra (SPPA) extended with local function calls, cryptographic primitives and special semantic features in order to cope with cryptographic protocols. More specifically, impassivity is defined as an information flow property founded on bisimulation-based non-deterministic admissible interference. A sound and complete proof method for impassivity is also provided. The method extends previous results presented by the authors on ...

• Type: Conference
• Year: 2003
• Where: IWFM
• Authors: Stéphane Lafrance, John Mullins
• Keywords: Cryptographic Protocols, Formal Cost-based Framework, Formal Methods, IWFM 2003, Non-deterministic Admissible Interference