An Information Flow Method to Detect Denial of Service Vulnerabilities
Дата
Авторы
Lafrance,Stéphane
Mullins,John
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
Meadows recently proposed a formal cost-based framework for the analysis of denial of service, showing how to formalize some existing principles used to make cryptographic protocols more resistant to denial of service by comparing the cost to the defender against the cost to the attacker. The firrst contribution of this paper is to introduce a new security property called impassivity designed to capture the abiity 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 handle cryptographic protocols. 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 provided. The method extends previous results of the authors on bisimulation-based non-deterministic admissible interference and its application to the analysis of cryptographic protocols. It is illustrated by its application to the TCP/IP protocol. Key Words: Denial of service, Protocols, Ad
Ключевые слова
denial of service , protocols , admissible interference , bisimulation , equivalence-checking