Formal Theory for Security Protocol Analysis of Distributed Denial of Service




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.


How to Cite
RUI JIANG, & BHARAT BHARGAVA. (2014). Formal Theory for Security Protocol Analysis of Distributed Denial of Service. International Journal of Next-Generation Computing, 5(3), 233–248.


  1. Peng T, Leckie C, Ramamohanarao K, Survey of network-based defense mechanisms countering the DoS and DDoS problems, ACM Computing Surveys , 2007, 39(1).
  2. Kumar P A R, Selvakumar S,Distributed Denial-of-Service Threat in Collaborative Environment - A Survey on DDoS Attack Tools and Traceback MechanismsIEEE International Conference on Advance Computing 2009IACC 20096-7 March 2009pp.1275 -1280.
  3. Yi Xie, Shun-Zheng Yu, Monitoring the Application-Layer DDoS Attacks for Popular WebsitesIEEE/ACM Transactions on Networking, Vol.17, No.1, 2009, pp.15-25.
  4. Muthuprasanna M, Manimaran G, Distributed divide and conquer techniques for effective DDoS attack defenses, In Proc. IEEE ICDCS, 2008.
  5. Chonka A, Singh J, Wanlei Zhou, Chaos theory based detection against network mimicking DDoS attacksIEEE Communications Letters, Vol.13, No.9, 2009, pp.717-719.
  6. Kandula S, Katabi D, Jacob M, Botz-4-sale : surviving organized DDoS attacks that mimic flash crowds, In Proc. USENIX NSDI, 2005.
  7. Nagaratna M, Prasad V K, Kumar S T, Detecting and Preventing IP-spoofed DDoS Attacks by Encrypted Marking Based Detection and Filtering (EMDAF), International Conference on Advances in Recent Technologies in Communication and Computing 2009 (ARTCom ’09), 27-28 Oct. 2009, pp.753-755.
  8. Liu X, Yang X, Lu Y, To filter or to authorize: network-layer DoS defense against multimillion-node botnets. In Proc. ACM SIGCOMM, 2008.
  9. Yu Chen, Kai Hwang, Wei-Shinn Ku, Collaborative Detection of DDoS Attacks over Multiple Network Domains, IEEE Transactions on Parallel and Distributed Systems, Vol.18, No.12, 2007, pp.1649-1662.
  10. Parno B, Wendlandt D, Shi E, Portcullis: protecting connection setup from denial of capability attacks, In Proc. ACM SIGCOMM, 2007.
  11. C. Meadows, Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends, IEEE Journal on Selected Areas in Communications, Vol. 21, No. 1, January 2003, pp.44-54.
  12. D. Dolev and A. Yao, On the security of public key protocols, IEEE Trans. Inform. Theory, vol. ITC29, pp. 198C208, Mar. 1983.
  13. C. Meadows, Applying formal methods to the analysis of a key management protocol, Journal of Computer Security, vol. 1, pp. 5C53, 1992.
  14. M. Burrows, M. Abadi, and R. Needham, A logic of authentication, ACM Trans. Comput. Syst., vol. 8, pp. 18C36, Feb. 1990.
  15. G. Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using FDR, Softw.Concepts Tools, vol. 17, no. 3, pp. 93C102, 1996.
  16. F. T. Fbrega, J. Herzog, and J. Guttman, Strand spaces: Proving security protocols correct, Journal of Computer Security, 7(2/3): 191C230, 1999.
  17. C. Meadows, A formal framework and evaluation method for network denial of service, in Proc. 12th IEEE Computer Security Foundations Workshop, June 1999, pp. 4C13.
  18. Stylianos Basagiannis, Panagiotis Katsaros, Andrew Pombortsis, Nikolaos Alexiou, Probabilistic model checking for the quantification of DoS security threats, Computers Security, Vol.28, No.5, 2009, pp. 450-465.
  19. Rui Jiang, A Novel Formal Theory for Security Protocol Analysis of Denial of Service Based on Extended Strand Space Model, China Communications, Vol.7, No.4, 2010, pp.23-28.
  20. L. Gong and P. Syverson, Fail-stop protocols: An approach to design secure protocols, Dependable Computing for Critical Applications 5, pages 79-100. IEEE Computer Society 1998.
  21. D. Harkins and D. Carrel. (1998) The Internet Key Exchange (IKE). Internet Engineering Task Force. [Online]. Available:
  22. W. Aiello, S. M. Bellovin, M. Blaze, R. Canetti, J. Loannidis, A. D. Keromytis and O. Reingold, Efficient, DoS-resistant, Secure key exchange for Internet protocols, ACM CCS 02, pages 27-39, Nov. 2002, Washington,DC USA.
  23. A. Juels and J. Brainard, Client puzzles: A cryptographic countermeasure against connection depletion attacks,In Proc. 1999 Network and Distributed Systems Security Symposium (NDSS), pages 151C165, San Diego, CA, February 1999. Internet Society.
  24. T. Aura, P. Nikander, and J. Leiwo, DoS-resistant authentication with client puzzles, Security Protocols Workshop 2000, pages 170-177.
  25. K. Matsuura and H. Imai, Protection of authenticated key-agreement protocol against a denial-of-service attack,In Proceedings of 1998 International Symposium on Information Theory and Its Applications (ISITA 98), pp.466-470, Oct. 1998.
  26. J. Zhou, Further analysis of the Internet key exchange protocol, Computer Communications, 23, 2000, pp.1606C1612.
  27. C. Schuba, I. Krsul, M. Kuhn, E. Spafford, A. Sundaram, and D. Zamboni, Analysis of a Denial of Service Attack on TCP, In Proceedings of the 1997 IEEE Symposium on Security and Privacy, pp. 208-223. IEEEComputer Society Press, May 1997.
  28. J. D. Guttman and F. J. Thayer Fabrega, Authentication tests and the structure of bundles, Theoretical Computer Science, 283(2): 333-380, 2002.
  29. M. Abadi, B. Blanchet, and C. Fournet, Just Fast Keying in the Pi Calculus, In Proceedings of 13th European Symposium on Programming (ESOP 2004), Barcelona, Spain, March 29-April 2, 2004.
  30. K. Sowmyadevi and T. V. Jenitha, Detect DDoS Attack Using Border Gateways and Edge Routers, International Journal of Computer Applications, Vol. 42, No. 9, 2012, pp. 9-13.
  31. B. B. Gupta, R. C. Joshi, and M. Misra, ANN Based Scheme to Predict Number of Zombies in a DDoS Attack, International Journal of Network Security, Vol. 14, No. 2, 2012, pp. 61-70.