| 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.
|
|---|
