{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,18]],"date-time":"2024-06-18T00:04:59Z","timestamp":1718669099299},"reference-count":14,"publisher":"World Scientific Pub Co Pte Ltd","issue":"04","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2016,5]]},"abstract":"<jats:p>Ensuring the fairness and non-repudiation in the security exchange protocol of web service is critical. Model checking is often used for automatic verification for the security properties of protocol. However, the current model checker tools cannot support formalizing protocols with cryptographic primitives, specifying properties with linear temporal logic (LTL) and automatically generating resilient intruder model simultaneously and the application range of them is severely limited. To solve this problem, a model checker Fepchecker is proposed to verify the fairness and non-repudiation properties, which are critical features in security exchange protocols. Firstly, applied pi-calculus is extended to specify the protocols, and the LTL assertion is used for precisely describing fairness and non-repudiation. Secondly, an intruder model is applied to construct their behavior sequences automatically and the protocol sessions and message pattern are used to alleviate the states explosion problem. Thirdly, in our model checking algorithm, the fairness and non-repudiation properties are verified based on Labeled Transition System (LTS) semantics model and the MakeOneMove method is used to explore the state space on-the-fly in the verification process. Finally, Fepchecker is applied to verify six representative protocols and the results show that Fepchecker can effectively verify their fairness and non-repudiation properties.<\/jats:p>","DOI":"10.1142\/s0218194016400027","type":"journal-article","created":{"date-parts":[[2016,6,15]],"date-time":"2016-06-15T13:22:31Z","timestamp":1465996951000},"page":"563-585","source":"Crossref","is-referenced-by-count":1,"title":["Fepchecker: An Automatic Model Checker for Verifying Fairness and Non-Repudiation of Security Protocols in Web Service"],"prefix":"10.1142","volume":"26","author":[{"given":"Xiaohong","family":"Li","sequence":"first","affiliation":[{"name":"Tianjin Key Laboratory of Cognitive Computing and Application, School of Computer Science and Technology, Tianjin University, 300350 Tianjin, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiayi","family":"Xu","sequence":"additional","affiliation":[{"name":"Tianjin Key Laboratory of Cognitive Computing and Application, School of Computer Science and Technology, Tianjin University, 300350 Tianjin, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guangquan","family":"Xu","sequence":"additional","affiliation":[{"name":"Tianjin Key Laboratory of Cognitive Computing and Application, School of Computer Science and Technology, Tianjin University, 300350 Tianjin, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianye","family":"Hao","sequence":"additional","affiliation":[{"name":"Digital Media Group, School of Software, Tianjin University, 300350 Tianjin, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoru","family":"Li","sequence":"additional","affiliation":[{"name":"Tianjin Key Laboratory of Cognitive Computing and Application, School of Computer Science and Technology, Tianjin University, 300350 Tianjin, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhiyong","family":"Feng","sequence":"additional","affiliation":[{"name":"Tianjin Key Laboratory of Cognitive Computing and Application, School of Computer Science and Technology, Tianjin University, 300350 Tianjin, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Honghao","family":"Gao","sequence":"additional","affiliation":[{"name":"Computing Center, Shanghai University, 200444 Shanghai, P.\u00a0R.\u00a0China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2016,6,14]]},"reference":[{"key":"S0218194016400027BIB001","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-4223(02)00015-7"},{"key":"S0218194016400027BIB005","doi-asserted-by":"publisher","DOI":"10.1007\/s00779-012-0536-z"},{"issue":"7","key":"S0218194016400027BIB007","first-page":"1049","volume":"15","author":"Yongbin Z.","year":"2004","journal-title":"J. Softw"},{"issue":"2","key":"S0218194016400027BIB008","first-page":"282","volume":"37","author":"Qing Z.","year":"2008","journal-title":"J. Univ. Electron. Sci. Technol. China"},{"issue":"2","key":"S0218194016400027BIB009","first-page":"300","volume":"42","author":"Yuexiang G.","year":"2013","journal-title":"J. Univ. Electro. Sci. Technol. China"},{"key":"S0218194016400027BIB012","series-title":"LNCS","volume-title":"Isabelle\/HOL- A Proof Assistant for Higher-Order Logic","volume":"2283","author":"Nipkow T.","year":"2002"},{"key":"S0218194016400027BIB013","volume":"2014","author":"Zhang C.","year":"2014","journal-title":"J. Appl. Math."},{"key":"S0218194016400027BIB014","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2001-91-203"},{"key":"S0218194016400027BIB018","doi-asserted-by":"publisher","DOI":"10.1145\/844357.844360"},{"key":"S0218194016400027BIB020","doi-asserted-by":"publisher","DOI":"10.1080\/00207160.2012.748902"},{"key":"S0218194016400027BIB021","volume-title":"Design and Validation of Computer Protocols","author":"Holzmann G. J.","year":"1991"},{"issue":"1","key":"S0218194016400027BIB027","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/s11704-012-2903-3","volume":"6","author":"Tuan L. A.","year":"2012","journal-title":"Front. Comp. Sci."},{"key":"S0218194016400027BIB030","first-page":"451","volume":"11","author":"Gordon A. D.","year":"2003","journal-title":"Comput. Sci. Net. Secur."},{"key":"S0218194016400027BIB033","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194016400027","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,17]],"date-time":"2024-06-17T16:55:03Z","timestamp":1718643303000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218194016400027"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5]]},"references-count":14,"journal-issue":{"issue":"04","published-online":{"date-parts":[[2016,6,14]]},"published-print":{"date-parts":[[2016,5]]}},"alternative-id":["10.1142\/S0218194016400027"],"URL":"https:\/\/doi.org\/10.1142\/s0218194016400027","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,5]]}}}