Automatic detection of DoS vulnerabilities of cryptographic protocols

• Autorzy: Krawczyk U. , Sapiecha P.

Identyfikatory

DOI

10.2478/v10065-012-0028-9

• Języki publikacji: EN

Abstrakty

EN

In this article the subject of DoS vulnerabilities of cryptographic key establishment and authentication protocols is discussed. The system for computer-aided DoS protocol resistance analysis, which employs the Petri nets formalism and Spin model-checker, is presented.

Słowa kluczowe

EN

automatic detection; DoS; denial of service attacks; Petri net; SPIN model checker

• Wydawca: Wydawnictwo UMCS
• Czasopismo: Annales Universitatis Mariae Curie-Skłodowska. Sectio AI, Informatica
• Rocznik: 2012
• Tom: Vol. 12, no. 4
• Strony: 51--67
• Opis fizyczny: Bibliogr. 21 poz., rys., tab.

Twórcy

autor

Krawczyk U.

• Krypton-Polska, Al. Jerozolimskie 131 Warsaw, Poland

autor

Sapiecha P.

• Krypton-Polska Al. Jerozolimskie 131 Warsaw, Poland
• Department of Electronics and Information Technology, Warsaw University of Technology, Warsaw, Poland

Bibliografia

• [1] Headlines, Bank of America Hit By Anonymous DDoS Attack, (27.12.2010); www.infosecisland.com
• [2] Adair S., Pushdo DDoS’ing or Blending In?, (2010); www.shadowserver.org/wiki/pmwiki.php/Calendar/20100129
• [3] Moore D., Shannon C.,The Spread of the Code Red Worm (crv2) (2001); www.caida.org/analysis/security/codered/coderedv2_analysis.xml
• [4] Meadows C., A Cost-Based Framework for Analysis of Denial of Service in Networks (2001); citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.31.9001&rep=rep1&type=pdf
• [5] Smith J., Gonzalez-Nieto J. M., Boyd C., Modelling Denial of Service Attacks on JFK with Meadows Cost-Based Framework (2006); citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.3877
• [6] Tritilanunt S., Boyd C., Foo E., Gonzalez Nieto J. M., Using Coloured Petri Nets to Simulate DoS-resistant protocols (2006); www.daimi.au.dk/CPnets/workshop06/cpn/papers/Paper15.pdf
• [7] Vanek T., Rohlik M., Model of DoS Resistant Broadcast Authentication Protocol in Colored Petri Net Environment, (2010); www.ic.uff.br/iwssip2010/Proceedings/nav/papers/paper_85.pdf
• [8] Sapiecha P., Krawczyk U., DoS Analizer language syntax (2012); www.krypton-polska.com/upload/1f0e3dad99908345f7439f8ffabdffc4.pdf
• [9] Balbo G., Desel J., Jensen K., Reisig W., Rozenberg G., Silva M., Introductory Tutorial - Petri Nets (2000); www.informatik.uni-hamburg.de/TGI/PetriNets/introductions/pn2000_introtut
• [10] Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, annual workshops in years 1998-2008; www.daimi.au.dk/CPnets
• [11] Jensen K., An Introduction to the Theoretical Aspects of Coloured Petri Nets (1994); www.dsc.ufcg.edu.br/ãbrantes/CursosAnteriores/MVSRP/rex.pdf
• [12] Holzmann G. J., Spin model-checker; http://spinroot.com
• [13] Sapiecha P., Krawczyk U., Effective reduction of cryptographic protocols specification for modelchecking with Spin, Annales UMCS, Informatica AI 11 (3) (2011): 27; DOI: 10.2478/v10065-011-0002-y
• [14] Jensen K., CPN Tools, www.daimi.au.dk/CPNTools
• [15] Boyd C., Mathuria A., Protocols for authentication and key establishment, Springer (2003).
• [16] Krawczyk H., SIGMA: the ’SIGn-and-MAc’ Approach to Authenticated Diffie-Hellman and its Use in the IKE Protocols (2003); ftp://ftp.pwg.org/pub/pwg/wbmm/security/sigma.pdf
• [17] Bitan S., Krawczyk H., SIGMA: the ’SIGn-and-MAc’ Crypto rationale and proposals – for IETF meeting (2001); www.ietf.org/proceedings/52/slides/ipsec-9.pdf
• [18] Barker E., et. all, Computer security - Recomendation for key management (2007); csrc.nist.gov
• [19] Giry D., BlueKrypt - Cryptographic Key Lenght Recomentation (2010); www.keylength.com/en
• [20] Dai W., Crypto++ 5.2.1 Benchmarks (16.01.2011); www.cryptopp.com
• [21] Beal J., Shepard T., Deamplification of DoS attacks via puzzles (2004); web.mit.edu/jakebeal/www/Unpublished/puzzle.pdf