{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:42:28Z","timestamp":1740123748480,"version":"3.37.3"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,9,21]],"date-time":"2017-09-21T00:00:00Z","timestamp":1505952000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Mobile Netw Appl"],"published-print":{"date-parts":[[2018,2]]},"DOI":"10.1007\/s11036-017-0903-0","type":"journal-article","created":{"date-parts":[[2017,9,21]],"date-time":"2017-09-21T03:34:26Z","timestamp":1505964866000},"page":"44-56","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal Analysis of the PKMv3 Protocol"],"prefix":"10.1007","volume":"23","author":[{"given":"Xiaoran","family":"Zhu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuanmin","family":"Xu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xin","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jian","family":"Guo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0797-0152","authenticated-orcid":false,"given":"Phan","family":"Cong Vinh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,9,21]]},"reference":[{"key":"903_CR1","doi-asserted-by":"publisher","unstructured":"Bosnacki D, Dams D (1998) Discrete-time Promela and spin. In: Formal techniques in real-time and fault-tolerant systems, 5th international symposium, FTRTFT\u201998, Lyngby, Denmark, September 14\u201318, 1998, proceedings, pp 307\u2013310. \n                        https:\/\/doi.org\/10.1007\/BFb0055359","DOI":"10.1007\/BFb0055359"},{"key":"903_CR2","doi-asserted-by":"publisher","unstructured":"Bosnacki D, Dams D (1998) Discrete-time Promela and spin. In: Formal techniques in real-time and fault-tolerant systems, 5th international symposium, FTRTFT\u201998, Lyngby, Denmark, September 14\u201318, 1998, proceedings, pp 307\u2013310. \n                        https:\/\/doi.org\/10.1007\/BFb0055359","DOI":"10.1007\/BFb0055359"},{"key":"903_CR3","doi-asserted-by":"publisher","unstructured":"Chen Z, Gu Y, Huang Z, Zheng J, Liu C, Liu Z (2015) Model checking aircraft controller software: a case study. Softw Pract Exper 45(7):989\u20131017. \n                        https:\/\/doi.org\/10.1002\/spe.2242","DOI":"10.1002\/spe.2242"},{"key":"903_CR4","doi-asserted-by":"publisher","unstructured":"Chen Z, Zhang D, Ma Y (2015) Modeling and analyzing the convergence property of the BGP routing protocol in SPIN. Telecommun Syst 58(3):205\u2013217. \n                        https:\/\/doi.org\/10.1007\/s11235-014-9870-y","DOI":"10.1007\/s11235-014-9870-y"},{"key":"903_CR5","first-page":"802","volume":"16m","author":"ILSs Committee","year":"2011","unstructured":"Committee I.L.S. et al. (2011) Standard for local and metropolitan area networks-Part 16: air interface for broadband wireless access systems-amendment 3: advanced air interface. IEEE Std 16m:802","journal-title":"IEEE Std"},{"key":"903_CR6","doi-asserted-by":"publisher","unstructured":"Dabaghchian M, Azgomi MA (2015) Model checking the observational determinism security property using PROMELA and SPIN. Form Asp Comput 27(5-6):789\u2013804. \n                        https:\/\/doi.org\/10.1007\/s00165-014-0331-x","DOI":"10.1007\/s00165-014-0331-x"},{"key":"903_CR7","doi-asserted-by":"publisher","unstructured":"Dabaghchian M, Azgomi MA (2015) Model checking the observational determinism security property using PROMELA and SPIN. Form Asp Comput 27(5-6):789\u2013804. \n                        https:\/\/doi.org\/10.1007\/s00165-014-0331-x","DOI":"10.1007\/s00165-014-0331-x"},{"key":"903_CR8","first-page":"41","volume":"4","author":"AM El-Amin","year":"2013","unstructured":"El-Amin AM, El-agooz S, Shehata AEDR, Amer EAE (2013) Design, verification and implementation of enhanced PKM WiMAX authentication protocol. International Journal of Computer Science and Telecommunications 4:41\u201346","journal-title":"International Journal of Computer Science and Telecommunications"},{"issue":"4","key":"903_CR9","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/s10009-014-0307-4","volume":"16","author":"JF Ferreira","year":"2014","unstructured":"Ferreira JF, Gherghina C, He G, Qin S, Chin WN (2014) Automated verification of the freertos scheduler in hip\/sleek. Int J Softw Tools Technol Transfer 16(4):381\u2013397","journal-title":"Int J Softw Tools Technol Transfer"},{"issue":"4","key":"903_CR10","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/s10009-014-0306-5","volume":"16","author":"C Gherghina","year":"2014","unstructured":"Gherghina C, David C, Qin S, Chin WN (2014) Expressive program verification via structured specifications. Int J Softw Tools Technol Transfer 16(4):363\u2013380","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"903_CR11","doi-asserted-by":"crossref","unstructured":"Kahya N, Ghoualmi N, Lafourcade P (2012) Formal analysis of PKM using scyther tool. In: International conference on information technology and e-services (ICITes), 2012. IEEE, pp 1\u20136","DOI":"10.1109\/ICITeS.2012.6216598"},{"issue":"1","key":"903_CR12","doi-asserted-by":"publisher","first-page":"21","DOI":"10.4230\/DagMan.1.1.21","volume":"1","author":"J Kreiker","year":"2011","unstructured":"Kreiker J, Tarlecki A, Vardi MY, Wilhelm R (2011) Modeling, analysis, and verification - the formal methods manifesto 2010 (dagstuhl perspectives workshop 10482). Dagstuhl Manifestos 1(1):21\u201340. \n                        https:\/\/doi.org\/10.4230\/DagMan.1.1.21","journal-title":"Dagstuhl Manifestos"},{"issue":"4","key":"903_CR13","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/SURV.2009.090402","volume":"11","author":"I Papapanagiotou","year":"2009","unstructured":"Papapanagiotou I, Toumpakaris D, Lee J, Devetsikiotis M (2009) A survey on next generation mobile WiMAX networks: objectives, features and technical challenges. IEEE Commun Surv Tutorials 11(4):3\u201318. \n                        https:\/\/doi.org\/10.1109\/SURV.2009.090402","journal-title":"IEEE Commun Surv Tutorials"},{"issue":"2","key":"903_CR14","doi-asserted-by":"publisher","first-page":"287","DOI":"10.3233\/AIC-150689","volume":"29","author":"S Pathak","year":"2016","unstructured":"Pathak S, Pulina L, Tacchella A (2016) Evaluating probabilistic model checking tools for verification of robot control policies. AI Commun 29(2):287\u2013299. \n                        https:\/\/doi.org\/10.3233\/AIC-150689","journal-title":"AI Commun"},{"key":"903_CR15","unstructured":"Process analysis toolkit spin home page. \n                        http:\/\/spinroot.com\/spin\/whatispin.html"},{"key":"903_CR16","doi-asserted-by":"publisher","unstructured":"Rai AK, Mishra S, Tripathi PN (2011) An improved secure authentication protocol for wiMAX with formal verification. In: Advances in computing and communications - first international conference, ACC 2011, Kochi, India, July 22\u201324, 2011. Proceedings, pp 407\u2013416. \n                        https:\/\/doi.org\/10.1007\/978-3-642-22714-1_42","DOI":"10.1007\/978-3-642-22714-1_42"},{"key":"903_CR17","doi-asserted-by":"publisher","unstructured":"Raju KVK, Kumari VV, Varma NS, Raju KVSVN (2010) Formal verification of IEEE802.16m PKMv3 protocol using CasperFDR. In: Information and communication technologies - international conference, ICT 2010, Kochi, Kerala, India, September 7\u20139, 2010. Proceedings, pp 590\u2013595. \n                        https:\/\/doi.org\/10.1007\/978-3-642-15766-0_101","DOI":"10.1007\/978-3-642-15766-0_101"},{"key":"903_CR18","doi-asserted-by":"publisher","unstructured":"Sadeghi MMG, Ali BM, Ma M, Manan JA (2014) Scalable and efficient key management for Mobile WiMAX networks. Int J Commun Syst 27(10):2166\u20132189. \n                        https:\/\/doi.org\/10.1002\/dac.2466","DOI":"10.1002\/dac.2466"},{"key":"903_CR19","doi-asserted-by":"publisher","unstructured":"Saha I, Roy S (2006) A finite state modeling of AFDX frame management using spin. In: Formal methods: applications and technology, 11th international workshop, FMICS 2006 and 5th international workshop PDMC 2006, Bonn, Germany, August 26\u201327, and August 31, 2006, revised selected papers, pp 227\u2013243. \n                        https:\/\/doi.org\/10.1007\/978-3-540-70952-7_15","DOI":"10.1007\/978-3-540-70952-7_15"},{"key":"903_CR20","doi-asserted-by":"publisher","unstructured":"Saha I, Roy S (2007) A finite state analysis of time-triggered CAN (TTCAN) protocol using spin. In: 2007 international conference on computing: theory and applications (ICCTA 2007), 5\u20137 March 2007, Kolkata, India, pp 77\u201381. \n                        https:\/\/doi.org\/10.1109\/ICCTA.2007.4","DOI":"10.1109\/ICCTA.2007.4"},{"key":"903_CR21","unstructured":"Taha AM, Abdel-Hamid AT, Tahar S (2009) Formal verification of IEEE 802.16 security sublayer using scyther tool. IEEE, pp 1\u20135"},{"key":"903_CR22","doi-asserted-by":"publisher","unstructured":"Trivedi DH, Patil MS (2011) Security in wimax using privacy and key management protocol. In: Proceedings of the ICWET \u201911 international conference & workshop on emerging trends in technology, Mumbai, Maharashtra, India, February 25\u201326, 2011, p 1372. \n                        https:\/\/doi.org\/10.1145\/1980022.1980379","DOI":"10.1145\/1980022.1980379"},{"key":"903_CR23","doi-asserted-by":"crossref","unstructured":"Xu S, Huang CT, Matthews MM (2008) Modeling and analysis of IEEE 802.16 PKM protocols using CasperFDR. In: IEEE international symposium on wireless communication systems. 2008. ISWCS \u201908. IEEE, pp 653\u2013657","DOI":"10.1109\/ISWCS.2008.4726137"},{"key":"903_CR24","doi-asserted-by":"crossref","unstructured":"Yang F (2011) Comparative analysis on TEK exchange between PKMv1 and PKMV2 for WiMAX. In: 7th international conference on wireless communications, networking and mobile computing (WiCOM), 2011, pp 1\u20134","DOI":"10.1109\/wicom.2011.6040271"},{"key":"903_CR25","unstructured":"You Z, Xie X, Zheng W (2010) Verification and research of a wimax authentication protocol based on SSM"},{"key":"903_CR26","doi-asserted-by":"publisher","unstructured":"Zhu X, Xu Y, Guo J, Wu X, Zhu H, Miao W (2015) Formal verification of PKMv3 protocol using DT-spin. In: 2015 international symposium on theoretical aspects of software engineering, TASE 2015, Nanjing, China, September 12\u201314, 2015, pp 71\u201378. \n                        https:\/\/doi.org\/10.1109\/TASE.2015.20","DOI":"10.1109\/TASE.2015.20"}],"container-title":["Mobile Networks and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11036-017-0903-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-017-0903-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-017-0903-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,3,6]],"date-time":"2018-03-06T05:42:59Z","timestamp":1520314979000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11036-017-0903-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,9,21]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,2]]}},"alternative-id":["903"],"URL":"https:\/\/doi.org\/10.1007\/s11036-017-0903-0","relation":{},"ISSN":["1383-469X","1572-8153"],"issn-type":[{"type":"print","value":"1383-469X"},{"type":"electronic","value":"1572-8153"}],"subject":[],"published":{"date-parts":[[2017,9,21]]}}}