Formal Theory for Security Protocol Analysis of Distributed Denial of Service
Rui Jiang, Bharat Bhargava · INTERNATIONAL JOURNAL OF NEXT-GENERATION COMPUTING · 2014
Distributed Denial of Service (DDoS) attack is a great threat to the Internet. Generally, the research in this area focuses on the behaviors of the network, which can not fundamentally solve the problem. In fact, the main reason for the DDoS attack is the loss of security in the communication protocol, therefore what needs to be done is the security protocol analysis. In this paper, a novel formal theory for security protocol analysis of DDoS is proposed. Based on the strand space model, the novel formal theory extends the strand space model with the weighted graph, the state functions of the nodes and a new penetrator model. Then, two kinds of DDoS test models are proposed with the goal of anti-DDoS attack. The DDoS test 1 states that, when an incoming message is received, if it can be authenticated by the receiver, the cost to the sender of preparing it should be greater than the cost to the recipient of authenticating it. The DDoS test 2 states that, when a message is received, if its sender cannot be determined, then the cost to prepare its reply should be negligible, and no state should be needed to complete the session. To show the correctness of the formal theory, two example protocols, which are the Internet key exchange (IKE) and the efficient DoS-resistant secure key exchange protocol (JFK), are formally analyzed. It is proved that the IKE easily suffers from the DDoS attacks, and the JFK is resistant against DDoS attack for the server, respectively. The new formal theory is concise and straightforward, and can keep all the merits of the original strand space model.