Automatic proof of resistance of denial of service attacks in protocols

First,the applied PI calculus was extended from two aspects:attacker contexts and process expression,then from the view of protocol state,the protocols were modeled with the extended applied PI calculus and a automatic method of proof of resistance of denial of service attacks based on theorem proof...

Full description

Saved in:
Bibliographic Details
Main Authors: Bo MENG, Wei HUANG, De-jun WAND, Fei SHAO
Format: Article
Language:zho
Published: Editorial Department of Journal on Communications 2012-03-01
Series:Tongxin xuebao
Subjects:
Online Access:http://www.joconline.com.cn/zh/article/doi/1000-436X(2012)03-0112-10/
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:First,the applied PI calculus was extended from two aspects:attacker contexts and process expression,then from the view of protocol state,the protocols were modeled with the extended applied PI calculus and a automatic method of proof of resistance of denial of service attacks based on theorem proof with first order theorem prover ProVerif was presented,finally resistance of denial of service attacks in JFK protocol and IEEE 802.11 four-way handshake protocol were analyzed.The results obtained are that JFK protocol is resistance of denial of service attack and IEEE 802.11 four-way handshake protocol is not.At the same time a new al of service attack in IEEE 802.11 four-way handshake protocol was found.The methods to prevent resistance of denial of service attacks in IEEE 802.11 four-way handshake protocol were proposed.
ISSN:1000-436X