{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,8]],"date-time":"2023-10-08T08:43:01Z","timestamp":1696754581539},"reference-count":37,"publisher":"Wiley","issue":"2","license":[{"start":{"date-parts":[[2009,6,12]],"date-time":"2009-06-12T00:00:00Z","timestamp":1244764800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Security Comm Networks"],"published-print":{"date-parts":[[2011,2]]},"abstract":"Abstract<\/jats:title>Model checking cryptographic protocols have evolved to a valuable method for discovering counterintuitive security flaws, which makes it possible for a hostile agent to subvert the goals of the protocol. Published works and existing security analysis tools are usually based on general intruder models that embody at least some aspects of the seminal work of Dolev\u2013Yao, in an attempt to detect failures of secrecy. In this work, we propose an alternative intruder model, which is based on a thorough analysis of how potential attacks might proceed. We introduce an intruder model that provides an open\u2010ended base for the integration of multiple basic attack tactics. Those attack tactics have the possibility to be combined, in a way to compose complex attack actions that require a number of procedural steps from the intruder's side, such as a Denial of Service attack. In our model checking approach, protocol correctness is checked by appropriate user\u2010supplied assertions or reachability of invalid end states. The analyst can express security properties of specific attack actions that are not restricted to safety violations captured by a generic model checker. The described intruder model methodology was implemented within the SPIN model checker for verifying two security protocols, Micromint and PayWord. Copyright \u00a9 2009 John Wiley & Sons, Ltd.<\/jats:p>","DOI":"10.1002\/sec.119","type":"journal-article","created":{"date-parts":[[2009,6,12]],"date-time":"2009-06-12T11:28:42Z","timestamp":1244806122000},"page":"147-161","source":"Crossref","is-referenced-by-count":9,"title":["Synthesis of attack actions using model checking for the verification of security protocols"],"prefix":"10.1002","volume":"4","author":[{"given":"Stylianos","family":"Basagiannis","sequence":"first","affiliation":[]},{"given":"Panagiotis","family":"Katsaros","sequence":"additional","affiliation":[]},{"given":"Andrew","family":"Pombortsis","sequence":"additional","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2011,1,28]]},"reference":[{"key":"e_1_2_8_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_8_3_2","doi-asserted-by":"crossref","unstructured":"BasagiannisS KatsarosP PombortsisA.Intrusion attack tactics for the model checking of e\u2010commerce security guarantees. InProceedings of the 26th International Conference on Computer Safety Reliability and Security(SAFECOMP) Nuremberg Germany LNCS 4680 Springer Verlag 2007;238\u2013251","DOI":"10.1007\/978-3-540-75101-4_22"},{"key":"e_1_2_8_4_2","unstructured":"The Spin Model Checker: Primer and Reference Manual Addison\u2010Wesley ISBN 0\u2010321\u201022862\u20106."},{"key":"e_1_2_8_5_2","unstructured":"The SPIN model checker official website available athttp:\/\/spinroot.com\/(last accessed 12\/12\/2008)."},{"key":"e_1_2_8_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-4048(93)90083-H"},{"key":"e_1_2_8_7_2","volume-title":"The Theory and Practice of Concurrency","author":"Roscoe AW","year":"1998"},{"key":"e_1_2_8_8_2","doi-asserted-by":"publisher","DOI":"10.1002\/sec.3"},{"key":"e_1_2_8_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0140-3664(02)00049-X"},{"key":"e_1_2_8_10_2","volume-title":"Design and Validation of Computer Protocols","author":"Holzmann GJ","year":"1991"},{"key":"e_1_2_8_11_2","doi-asserted-by":"publisher","DOI":"10.1002\/dac.729"},{"key":"e_1_2_8_12_2","doi-asserted-by":"crossref","unstructured":"MeadowsCA.Formal verification of cryptographic protocols: a survey.Advances in Cryptology\u2014International Conference on the Theory and Application of Cryptology(ASIACRYPT) LNCS917 Springer\u2010Verlag 1995;133\u2013150.","DOI":"10.1007\/BFb0000430"},{"key":"e_1_2_8_13_2","doi-asserted-by":"crossref","unstructured":"CremersCJF.Feasibility of multi\u2010protocol attacks. InProceedings of the First International Conference on Availability Reliability and Security IEEE Computer Society Press 2006.","DOI":"10.1109\/ARES.2006.63"},{"key":"e_1_2_8_14_2","doi-asserted-by":"crossref","unstructured":"BasagiannisS KatsarosP PombortsisA AlexiouN.A probabilistic attacker model for quantitative verification of DoS security threats. InProceedings of the 32nd Annual International Computer and Applications Software(COMPSAC) Turku Finland 2008.","DOI":"10.1109\/COMPSAC.2008.48"},{"key":"e_1_2_8_15_2","unstructured":"MoskowitzR NikanderP JokelaP HendersonT.Host Identity Protocol. Internet Engineering Task Force 2008; RFC5201."},{"key":"e_1_2_8_16_2","doi-asserted-by":"crossref","unstructured":"RivestRL ShamirA.Payword and Micromint: two simple micropayment schemes. InProceedings of the Fourth International Workshop on Security Protocols LNCS1189 Springer\u2010Verlag 1996;69\u201387.","DOI":"10.1007\/3-540-62494-5_6"},{"key":"e_1_2_8_17_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1987.233151"},{"key":"e_1_2_8_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/363516.363528"},{"key":"e_1_2_8_19_2","unstructured":"MitchellJC MitchellM SternU.Automated analysis of cryptographic protocols using Mur\u03c6 InProceedings of the IEEE Symposium on Research in Security and Privacy IEEE Computer Society 1997;141\u2013153."},{"key":"e_1_2_8_20_2","unstructured":"RoscoeAW.Modeling and verifying key\u2010exchange protocols using CSP and FDR InProceedings of the 8th IEEE Computer Security Foundations Workshop IEEE Computer Society 1995;98\u2013107."},{"key":"e_1_2_8_21_2","unstructured":"WooTYC LamSS.A semantic model for authentication protocols. InProceedings of the IEEE Symposium on Research in Security and Privacy 1993."},{"key":"e_1_2_8_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00141-4"},{"key":"e_1_2_8_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/77648.77649"},{"key":"e_1_2_8_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/382258.382789"},{"key":"e_1_2_8_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0055-7"},{"key":"e_1_2_8_26_2","unstructured":"LoweG.Casper: a compiler for the analysis of security protocols. InProceedings of the IEEE Computer Security Foundations Workshop IEEE Computer Society 1997;18\u201330."},{"issue":"2","key":"e_1_2_8_27_2","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00197942","article-title":"Three systems for cryptographic protocol analysis","volume":"7","author":"Meadows C","year":"1994","journal-title":"Journal of Cryptology"},{"key":"e_1_2_8_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0140-3664(99)00030-4"},{"key":"e_1_2_8_29_2","unstructured":"AVISPA: automated validation of Internet security protocols and applications 2003. FET Open Project IST\u20102001\u20103925 2 http:\/\/www.avispa\u2010project.org"},{"key":"e_1_2_8_30_2","doi-asserted-by":"crossref","unstructured":"CederquistJG DashtiMT.An intruder model for verifying liveness in security protocols. InProceedings of the fourth ACM workshop on Formal Methods in Security(FMSE'06) Alexandria Virginia USA 2006;23\u201332","DOI":"10.1145\/1180337.1180340"},{"key":"e_1_2_8_31_2","unstructured":"LoweG.Towards a completeness result for model\u2010checking of Security Protocols InProceedings of the 11th Computer Security Foundations Workshop. IEEE Computer Society Press 1998."},{"key":"e_1_2_8_32_2","unstructured":"RoscoeAW GoldsmithM.The perfect spy for model\u2010checking cryptoprotocols InProceedings of the Workshop on Design and Formal Verification of Security Protocols(DIMACS) 1997."},{"key":"e_1_2_8_33_2","unstructured":"ClarkJ JacobJ.A survey of authentication protocol literature: version 1.0 Technical Report University of York 1997."},{"key":"e_1_2_8_34_2","unstructured":"HeatherJ LoweG SchneiderS.How to prevent type flaw attacks on security protocols InProceedings of the 13th IEEE Computer Security Foundations Workshop IEEE Computer Society 2000;255\u2013268."},{"key":"e_1_2_8_35_2","unstructured":"CarlsenU.Cryptographic protocol flaws\u2014Know your enemy InProceedings of the 7th IEEE Computer Security Foundations Workshop IEEE Computer Society 1994;192\u2013200."},{"key":"e_1_2_8_36_2","doi-asserted-by":"crossref","unstructured":"SyversonP CervesatoI.The logic of authentication protocols. InProceedings of the 1st International School on Foundations of Security Analysis and Design(FOSAD 2000)LNCS2171 Springer\u2010Verlag 2001 63\u2013137.","DOI":"10.1007\/3-540-45608-2_2"},{"key":"e_1_2_8_37_2","doi-asserted-by":"publisher","DOI":"10.1002\/sec.22"},{"key":"e_1_2_8_38_2","doi-asserted-by":"crossref","unstructured":"RivestRL.The MD5 Message\u2010Digest Algorithm Internet informational RFC1321 1992.","DOI":"10.17487\/rfc1321"}],"container-title":["Security and Communication Networks"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fsec.119","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/sec.119","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,7]],"date-time":"2023-10-07T13:28:30Z","timestamp":1696685310000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/sec.119"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1,28]]},"references-count":37,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2011,2]]}},"alternative-id":["10.1002\/sec.119"],"URL":"https:\/\/doi.org\/10.1002\/sec.119","archive":["Portico"],"relation":{},"ISSN":["1939-0114","1939-0122"],"issn-type":[{"value":"1939-0114","type":"print"},{"value":"1939-0122","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,1,28]]}}}