{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,26]],"date-time":"2026-01-26T15:37:22Z","timestamp":1769441842290,"version":"3.49.0"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,2,22]],"date-time":"2012-02-22T00:00:00Z","timestamp":1329868800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/2.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Wireless Com Network"],"published-print":{"date-parts":[[2012,12]]},"DOI":"10.1186\/1687-1499-2012-57","type":"journal-article","created":{"date-parts":[[2012,2,22]],"date-time":"2012-02-22T06:16:46Z","timestamp":1329891406000},"source":"Crossref","is-referenced-by-count":20,"title":["A formally verified AKA protocol for vertical handover in heterogeneous environments using Casper\/FDR"],"prefix":"10.1186","volume":"2012","author":[{"given":"Mahdi","family":"Aiash","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Glenford","family":"Mapp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aboubaker","family":"Lasebae","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Raphael","family":"Phan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan","family":"Loo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,2,22]]},"reference":[{"key":"255_CR1","volume-title":"Mobile Communications","author":"S Jochen","year":"2003","unstructured":"Jochen S: Mobile Communications. Pearson Education Limited, UK; 2003."},{"key":"255_CR2","unstructured":"Long Term Evolution Protocol Overview, Freescale Semiconductor, 2008[\n                    http:\/\/www.freescale.com\/files\/wireless_comm\/doc\/white_paper\/LTEPTCLOVWWP.pdf\n                    \n                  ]"},{"key":"255_CR3","first-page":"1765","volume-title":"ICWN2011","author":"M Aiash","year":"2011","unstructured":"Aiash M, Mapp G, Lasebae A: A QoS framework for Heterogeneous Networking. In ICWN2011. London UK; 2011:1765-1769."},{"key":"255_CR4","unstructured":"Internet Engineering Task Force: Handover keying working group (hokey wg).[\n                    http:\/\/www.ietf.org\/html.charters\/hokey-charter.html\n                    \n                  ]"},{"key":"255_CR5","unstructured":"3rd Generation Partnership Project (3GPP)[\n                    http:\/\/www.3gpp.org\/\n                    \n                  ]"},{"key":"255_CR6","volume-title":"IEEE 802.21\/D8.0, Draft Standard for Local and Metropolitan Area Networks: Media Independent Handover Services","author":"Institute of Electrical and Electronics Engineers","year":"2007","unstructured":"Institute of Electrical and Electronics Engineers: IEEE 802.21\/D8.0, Draft Standard for Local and Metropolitan Area Networks: Media Independent Handover Services. 2007."},{"key":"255_CR7","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1023\/B:WIRE.0000047061.87235.8b","volume":"29","author":"K Masahiro","year":"2004","unstructured":"Masahiro K, Mariko Y, Ryoji O, Shinsaku K, Tanaka T: Secure service and network framework for mobile ethernet. Wirel Personal Commun 2004, 29: 161-190.","journal-title":"Wirel Personal Commun"},{"key":"255_CR8","volume-title":"3GPP Technical Specifications.: 3G Security; WLAN interworking security (Release 7)","author":"3rd Generation Partnership Project","year":"2006","unstructured":"3rd Generation Partnership Project: 3GPP Technical Specifications.: 3G Security; WLAN interworking security (Release 7). 2006."},{"key":"255_CR9","volume-title":"PhD Thesis","author":"AS Ali","year":"2010","unstructured":"Ali AS: Authentication and key management in heterogeneous wireless networks. In PhD Thesis. Electrical and Computer Engineering, The University of British Columbia; 2010."},{"key":"255_CR10","volume-title":"Extensible Authentication Protocol (EAP) RFC 3748","author":"B Aboba","year":"2004","unstructured":"Aboba B, Blunk L, Vollbrecht J, Carlson J, Levkowetz H: Extensible Authentication Protocol (EAP) RFC 3748. 2004."},{"issue":"4","key":"255_CR11","first-page":"65","volume":"52","author":"I KENTARO","year":"2007","unstructured":"KENTARO I, Masahiro K: Mobile Ethernet Technologies: 5-1: Scalable Mobile Ethernet and Fast Vertical Handover. Review of the National Institute of Information and Communications Technology 2007, 52(4):65-74.","journal-title":"Review of the National Institute of Information and Communications Technology"},{"key":"255_CR12","volume-title":"The modelling and analysis of security protocols","author":"P Ryan","year":"2010","unstructured":"Ryan P, Schneider S, Goldsmith M, Lowe G, Roscoe AW: The modelling and analysis of security protocols. PEARSON Ltd; 2010."},{"key":"255_CR13","unstructured":"Formal Systems (Europe) Ltd.:Failures-Divergence Refinement. FDR2 User Manual. Accessed 19 August 2011 [\n                    http:\/\/www.fsel.com\/documentation\/fdr2\/fdr2manual.pdf\n                    \n                  ]"},{"key":"255_CR14","first-page":"653","volume-title":"Wireless Communication Systems, ISWCS'08","author":"S Xu","year":"2008","unstructured":"Xu S, Tser Huang C, Matthews MM: Modeling and analysis of IEEE 802.16 PKM Protocols using CasperFDR. In Wireless Communication Systems, ISWCS'08. Reykjavik, Iceland; 2008:653-657."},{"key":"255_CR15","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-20573-6_44","volume":"147","author":"KV Krishnam Raju","year":"2011","unstructured":"Krishnam Raju KV, Valli Kumari V: Formal verification of IEEE802.11i WPA-GPG authentication protocol. Commun Comput Inf Sci 2011, 147: 267-272. 10.1007\/978-3-642-20573-6_44","journal-title":"Commun Comput Inf Sci"},{"key":"255_CR16","doi-asserted-by":"publisher","first-page":"590","DOI":"10.1007\/978-3-642-15766-0_101","volume":"101","author":"KV Krishnam Raju","year":"2010","unstructured":"Krishnam Raju KV, Valli Kumari V, Sandeep Varma N, Raju KVSVN: Formal verification of IEEE802.16m PKMv3 protocol using CasperFDR. Commun Comput Inf Sci 2010, 101: 590-595. 10.1007\/978-3-642-15766-0_101","journal-title":"Commun Comput Inf Sci"},{"key":"255_CR17","unstructured":"Lowe G, Broadfoot P, Dilloway C, Hui M: Casper, a compiler for the Analysis of security protocol.[\n                    http:\/\/www.comlab.ox.ac.uk\/gavin.lowe\/Security\/Casper\/\n                    \n                  ]"},{"key":"255_CR18","volume-title":"Global Information Infrastructure, Internet Protocol Aspects And Next Generation Networks, Y.140.1","author":"International Telecommunication Union (ITU-T)","year":"2004","unstructured":"International Telecommunication Union (ITU-T): Global Information Infrastructure, Internet Protocol Aspects And Next Generation Networks, Y.140.1. 2004."},{"key":"255_CR19","first-page":"1","volume-title":"16 th Mobile and Wireless Communications Summit, Budapest","author":"S Sargento","year":"2007","unstructured":"Sargento S, Jesus V, Sousa F, Mitrano F, Strauf T, Schmoll C, Gozdecki J, Lemos G, Almeida M, Corujo D: Context-Aware End-to-End QoS Architecture in Multi-technology, Multi-interface Environments. 16 th Mobile and Wireless Communications Summit, Budapest 2007, 1-6."},{"key":"255_CR20","unstructured":"IEEE P802.21\/D14.0 Media Independent Handover Services 2008."},{"key":"255_CR21","first-page":"14","volume-title":"IEEE Wirel Commun","author":"U Horn","year":"2004","unstructured":"Horn U, Prehofer C, Karl H: Ambient networks: an architecture for communication networks beyond 3G. IEEE Wirel Commun 2004, 14-22."},{"key":"255_CR22","unstructured":"Y-Comm Research[\n                    http:\/\/www.mdx.ac.uk\/research\/areas\/software\/ycomm_research.aspx\n                    \n                  ]"},{"key":"255_CR23","volume-title":"EAP Extensions for EAP Re-authentication Protocol (ERP) RFC 5296","author":"V Narayanan","year":"2008","unstructured":"Narayanan V, Dondeti L: EAP Extensions for EAP Re-authentication Protocol (ERP) RFC 5296. 2008."},{"key":"255_CR24","unstructured":"IEEE Standard for local and metropolitan area networks: Air Interface for Fixed Broadband Wireless Access Systems, Part 16, Amendment 2 and Corrigendum 1. IEEE Std 802.16e-2005 and IEEE Std 802.16-2004\/Cor1-2005"},{"key":"255_CR25","volume-title":"WiMAX Forum, Rel. 1, ver. 1.2","author":"WiMAX Forum Network Architecture Stage 3","year":"2008","unstructured":"WiMAX Forum Network Architecture Stage 3: Detailed Protocols and Procedures. WiMAX Forum, Rel. 1, ver. 1.2 2008."},{"key":"255_CR26","doi-asserted-by":"publisher","DOI":"10.1201\/9781439821916","volume-title":"Handbook of Applied Cryptography","author":"A Menezes","year":"1996","unstructured":"Menezes A, van Oorschot P, Vanstone S: Handbook of Applied Cryptography. CRC Press, Boca Raton, FL, USA; 1996."},{"key":"255_CR27","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1016\/B978-075067746-2\/50009-8","volume-title":"Bulletproof Wireless Security: GSM, UMTS, 802.11 and Ad Hoc Security","author":"P Chandra","year":"2005","unstructured":"Chandra P: Bulletproof Wireless Security: GSM, UMTS, 802.11 and Ad Hoc Security. Newnes, Oxford; 2005:129-158."},{"key":"255_CR28","volume-title":"Security Architecture for the Internet Protocol RFC 2401","author":"S Kent","year":"1998","unstructured":"Kent S, Atkinson R: Security Architecture for the Internet Protocol RFC 2401. 1998."},{"key":"255_CR29","unstructured":"Xavier D: COSP-J: A compiler for security protocols, Master Thesis, Oxford University Computing Laboratory.[\n                    http:\/\/www.cs.ox.ac.uk\/gavin.lowe\/Security\/Casper\/COSPJ\/secu.pdf\n                    \n                  ]"}],"container-title":["EURASIP Journal on Wireless Communications and Networking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1186\/1687-1499-2012-57\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/1687-1499-2012-57.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1186\/1687-1499-2012-57.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,22]],"date-time":"2019-01-22T05:48:50Z","timestamp":1548136130000},"score":1,"resource":{"primary":{"URL":"https:\/\/jwcn-eurasipjournals.springeropen.com\/articles\/10.1186\/1687-1499-2012-57"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2,22]]},"references-count":29,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,12]]}},"alternative-id":["255"],"URL":"https:\/\/doi.org\/10.1186\/1687-1499-2012-57","relation":{},"ISSN":["1687-1499"],"issn-type":[{"value":"1687-1499","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,2,22]]},"article-number":"57"}}