乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,8,31]],"date-time":"2024-08-31T11:32:17Z","timestamp":1725103937818},"reference-count":54,"publisher":"Wiley","issue":"5-7","license":[{"start":{"date-parts":[[2014,4,29]],"date-time":"2014-04-29T00:00:00Z","timestamp":1398729600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"funder":[{"name":"Fond national pour la societe numerique","award":["DAST"]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Software Testing Verif & Rel"],"published-print":{"date-parts":[[2015,8]]},"abstract":"Summary<\/jats:title>In recent years, important efforts have been made for offering a dedicated language for modelling and verifying security protocols. Outcome of the European project AVISPA, the high\u2010level security protocol language (HLPSL) aims at providing a means for verifying usual security properties (such as data secrecy) in message exchanges between agents. However, verifying the security protocol model does not guarantee that the actual implementation of the protocol will fulfil these properties. This article presents a model\u2010based testing approach, relying on the mutation of HLPSL models to generate abstract test cases. The proposed mutations aim at introducing leaks in the security protocols and represent real\u2010world implementation errors. The mutated models are then analysed by the automated validation of Internet security protocols and applications tool set, which produces, when the mutant protocol is declared unsafe, counterexample traces exploiting the security flaws and, thus, providing test cases. A dedicated framework is then used to concretize the abstract attack traces, bridging the gap between the formal model level and the implementation level. This model\u2010based testing technique has been experimented on a wide range of security protocols, in order to evaluate the mutation operators. This process has also been fully tool\u2010supported, from the mutation of the HLPSL model to the concretization of the abstract test cases into test scripts. It has been applied to a realistic case study of the Paypal payment protocol, which made it possible to discover a vulnerability in an implementation of an e\u2010commerce framework. Copyright \u00a9 2014 John Wiley & Sons, Ltd.<\/jats:p>","DOI":"10.1002\/stvr.1531","type":"journal-article","created":{"date-parts":[[2014,4,29]],"date-time":"2014-04-29T09:23:31Z","timestamp":1398763411000},"page":"684-711","source":"Crossref","is-referenced-by-count":15,"title":["Model\u2010based mutation testing from security protocols in HLPSL"],"prefix":"10.1002","volume":"25","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Dadeau","sequence":"first","affiliation":[{"name":"Femto\u2010ST institute\/INRIA CASSIS, 16 route de Gray, 25030 Besan\u00e7on France France"}]},{"given":"Pierre\u2010Cyrille","family":"H\u00e9am","sequence":"additional","affiliation":[{"name":"Femto\u2010ST institute\/INRIA CASSIS, 16 route de Gray, 25030 Besan\u00e7on France France"},{"name":"INRIA Nancy Grand Est et LORIA, 615, rue du Jardin Botanique 54602 Villers les Nancy CEDEX France"}]},{"given":"Rafik","family":"Kheddam","sequence":"additional","affiliation":[{"name":"Univ. Grenoble Alpes, LCIS 26900 Valence France"}]},{"given":"Ghazi","family":"Maatoug","sequence":"additional","affiliation":[{"name":"INRIA Nancy Grand Est et LORIA, 615, rue du Jardin Botanique 54602 Villers les Nancy CEDEX France"}]},{"given":"Michael","family":"Rusinowitch","sequence":"additional","affiliation":[{"name":"INRIA Nancy Grand Est et LORIA, 615, rue du Jardin Botanique 54602 Villers les Nancy CEDEX France"}]}],"member":"311","published-online":{"date-parts":[[2014,4,29]]},"reference":[{"key":"e_1_2_13_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_27"},{"key":"e_1_2_13_3_1","unstructured":"The high level protocol specification language: AVISPA project Delivrable 2.1 2003. Available from:http:\/\/www.avispa\u2010project.org\/delivs\/2.1\/d2\u20101.pdf[accessed on 18 April 2014]."},{"key":"e_1_2_13_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_21"},{"key":"e_1_2_13_5_1","first-page":"194","article-title":"Approximation\u2010based tree regular model\u2010checking","volume":"14","author":"Boichut Y","year":"2008","journal-title":"Nordic Journal of Computing"},{"key":"e_1_2_13_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1456396.1456397"},{"key":"e_1_2_13_7_1","unstructured":"Web\u2010based reference implementation of SAML\u2010based SSO for Google apps: Google. Available from:https:\/\/developers.google.com\/google\u2010apps\/sso\/saml_reference_implementation_web[accessed on 18 April 2014]."},{"key":"e_1_2_13_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16074-5_6"},{"key":"e_1_2_13_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866337"},{"key":"e_1_2_13_10_1","unstructured":"Pkcs #11 v.2.20: cryptographic token interface standard: RSA Security Inc 2004."},{"key":"e_1_2_13_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/C-M.1978.218136"},{"key":"e_1_2_13_12_1","unstructured":"DeMilloRA.Test adequacy and program mutation.International Conference on Software Engineering Pittsburg PA USA 1989;355\u2013356."},{"key":"e_1_2_13_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0096-0551(85)90011-6"},{"key":"e_1_2_13_14_1","volume-title":"Black\u2010Box Testing: Techniques for Functional Testing of Software and Systems","author":"Beizer B","year":"1995"},{"key":"e_1_2_13_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10003-2_69"},{"key":"e_1_2_13_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61042-1_43"},{"issue":"1","key":"e_1_2_13_17_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/JCS-2006-14101","article-title":"A survey of algebraic properties used in cryptographic protocols","volume":"14","author":"Cortier V","year":"2006","journal-title":"Journal of Computer Security"},{"key":"e_1_2_13_18_1","unstructured":"A Beginner's guide to modelling and analysing Internet security protocols: AVISPA project. Available from:http:\/\/www.avispa\u2010project.org\/package\/tutorial.pdf[accessed on 18 April 2014]."},{"key":"e_1_2_13_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_13_20_1","first-page":"350","volume-title":"SFCS '81: Proceedings of the 22nd Annual Symposium on Foundations of Computer Science","author":"Dolev D","year":"1981"},{"key":"e_1_2_13_21_1","series-title":"Lecture Notes in Computer Science","first-page":"131","volume-title":"Formal Methods for the Design of Real\u2010Time Systems","author":"Bozga M","year":"2004"},{"key":"e_1_2_13_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0055-7"},{"key":"e_1_2_13_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-007-0041-y"},{"key":"e_1_2_13_24_1","unstructured":"ClarkJ JacobJ.A survey of authentification protocol literature University of York UK 1997."},{"key":"e_1_2_13_25_1","unstructured":"IEEE 802.1 local and metropolitan area networks: wireless LAN medium acess control (MAC) and physical (PHY) specifications 1999."},{"key":"e_1_2_13_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1996.502669"},{"key":"e_1_2_13_27_1","doi-asserted-by":"crossref","unstructured":"MillenJK ShmatikovV.Constraint solving for bounded\u2010process cryptographic protocol analysis.ACM Conference on Computer and Communications Security Philadelphia PA USA 2001;166\u2013175.","DOI":"10.1145\/501983.502007"},{"key":"e_1_2_13_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30473-6_3"},{"key":"e_1_2_13_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2009.04.016"},{"key":"e_1_2_13_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32009-5_37"},{"key":"e_1_2_13_31_1","series-title":"Lecture Notes in Computer Science","volume-title":"4th SETOP International Workshop on Autonomous and Spontaneous Security","author":"Avanesov T","year":"2012"},{"key":"e_1_2_13_32_1","unstructured":"Magento community edition. Available from:http:\/\/www.magentocommerce.com\/[accessed on 18 April 2014]."},{"key":"e_1_2_13_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.26"},{"key":"e_1_2_13_34_1","unstructured":"Paypal development & integration guides. Available from:https:\/\/developer.paypal.com\/webapps\/developer\/docs\/classic\/products\/[accessed on 18 April 2014]."},{"key":"e_1_2_13_35_1","unstructured":"XAMPP an easy to install Apache distribution. Available from:http:\/\/www.apachefriends.org\/en\/xampp.html[accessed on 18 April 2014]."},{"key":"e_1_2_13_36_1","unstructured":"Fiddler: the free Web debugging proxy for any browser system or platform. Available from:http:\/\/www.telerik.com\/fiddler[accessed on 18 April 2014]."},{"key":"e_1_2_13_37_1","first-page":"240","volume-title":"ICST'11","author":"Dadeau F","year":"2011"},{"key":"e_1_2_13_38_1","first-page":"649","article-title":"An analysis and survey of the development of mutation testing","volume":"99","author":"Jia Y","year":"2010","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"1","key":"e_1_2_13_39_1","first-page":"77","article-title":"Testing with model checkers: insuring fault visibility","volume":"2","author":"Okun V","year":"2003","journal-title":"WSEAS Transaction System"},{"key":"e_1_2_13_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2009.06.030"},{"key":"e_1_2_13_41_1","unstructured":"FabbriSCPF DelamaroME MaldonadoJC MasieroP.Mutation analysis testing for finite state machines.Proceedings of the 5th International Symposium on Software Reliability Engineering 1994;220\u2013229."},{"key":"e_1_2_13_42_1","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1109\/ICSEA.2006.261272","volume-title":"Proceedings of the International Conference on Software Engineering Advances (ICSEA 2006)","author":"Fraser G","year":"2006"},{"key":"e_1_2_13_43_1","unstructured":"ProbertRL GuoF.Mutation testing of protocols: principles and preliminary experimental results.Proceedings of the Workshop on Protocol Test Systems: Leidschendam Netherland 15\u2010171991October;57\u201376."},{"key":"e_1_2_13_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2004.09.009"},{"key":"e_1_2_13_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/AST.2007.1"},{"key":"e_1_2_13_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44830-6_22"},{"key":"e_1_2_13_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/26.494307"},{"key":"e_1_2_13_48_1","first-page":"25","volume-title":"ICDCS '07: Proceedings of the 27th International Conference on Distributed Computing Systems","author":"Shu G","year":"2007"},{"key":"e_1_2_13_49_1","series-title":"LNCS","first-page":"357","volume-title":"Testing of Communicating Systems, 18th IFIP TC6\/WG6.1 International Conference (TESTCOM 2006)","author":"Shu G","year":"2006"},{"key":"e_1_2_13_50_1","first-page":"471","volume-title":"ICFEM '02: Proceedings of the 4th International Conference on Formal Engineering Methods","author":"Wimmel G","year":"2002"},{"key":"e_1_2_13_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61648-9_58"},{"key":"e_1_2_13_52_1","unstructured":"AslamT KrsulI SpaffordEH.Use of a taxonomy of security faults.19th NIST\u2010NCSC National Information Systems Security Conference Baltimore MD USA 1996;551\u2013560."},{"key":"e_1_2_13_53_1","series-title":"TAP'11","first-page":"69","volume-title":"Proceedings of the 5th International Conference on Tests and Proofs","author":"B\u00fcchler M","year":"2011"},{"key":"e_1_2_13_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/SERE.2012.38"},{"key":"e_1_2_13_55_1","unstructured":"AVANTSSAR.Delivrable 2.1: requirements for modelling and aslan v1 2008. Available from:http:\/\/www.avantssar.eu[accessed on 18 April 2014]."}],"container-title":["Software Testing, Verification and Reliability"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fstvr.1531","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/stvr.1531","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T06:24:41Z","timestamp":1694586281000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/stvr.1531"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4,29]]},"references-count":54,"journal-issue":{"issue":"5-7","published-print":{"date-parts":[[2015,8]]}},"alternative-id":["10.1002\/stvr.1531"],"URL":"https:\/\/doi.org\/10.1002\/stvr.1531","archive":["Portico"],"relation":{},"ISSN":["0960-0833","1099-1689"],"issn-type":[{"value":"0960-0833","type":"print"},{"value":"1099-1689","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,4,29]]}}}