{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T08:40:10Z","timestamp":1746348010527,"version":"3.40.4"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319113784"},{"type":"electronic","value":"9783319113791"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11379-1_17","type":"book-chapter","created":{"date-parts":[[2014,8,20]],"date-time":"2014-08-20T03:14:54Z","timestamp":1408504494000},"page":"341-361","source":"Crossref","is-referenced-by-count":8,"title":["Formal Analysis of Security Procedures in LTE - A Feasibility Study"],"prefix":"10.1007","author":[{"given":"Noomene","family":"Ben Henda","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karl","family":"Norrman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"3GPP The Mobile Broadband Standard, http:\/\/www.3gpp.org\/specifications\/"},{"key":"17_CR2","unstructured":"10th Computer Security Foundations Workshop (CSFW 1997), Rockport, Massachusetts, USA, June 10-12. IEEE Computer Society (1997)"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-540-24725-8_24","volume-title":"Programming Languages and Systems","author":"M. Abadi","year":"2004","unstructured":"Abadi, M., Blanchet, B., Fournet, C.: Just Fast Keying in the Pi Calculus. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 340\u2013354. Springer, Heidelberg (2004)"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Hankin, C., Schmidt, D. (eds.) POPL, pp. 104\u2013115. ACM (2001)","DOI":"10.1145\/373243.360213"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Mancini, L.I., Ritter, E., Ryan, M., Golde, N., Redon, K., Borgaonkar, R.: New privacy issues in mobile telephony: fix and verification. In: Yu, T., Danezis, G., Gligor, V.D. (eds.) ACM Conference on Computer and Communications Security, pp. 205\u2013216. ACM (2012)","DOI":"10.1145\/2382196.2382221"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A. Armando","year":"2005","unstructured":"Armando, A., et al.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"key":"17_CR7","unstructured":"Blanchet, B.: Automatic verification of correspondences for security protocols"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: CSFW, pp. 82\u201396. IEEE Computer Society (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Chaudhuri, A.: Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage. In: IEEE Symposium on Security and Privacy, pp. 417\u2013431. IEEE Computer Society (2008)","DOI":"10.1109\/SP.2008.12"},{"key":"17_CR10","unstructured":"Blanchet, B., Smyth, B., Cheval, V.: ProVerif 1.88: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial"},{"key":"17_CR11","unstructured":"Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Nielson, H.R.: Automatic validation of protocol narration"},{"issue":"11-12","key":"17_CR12","doi-asserted-by":"crossref","first-page":"1365","DOI":"10.1007\/BF03253324","volume":"62","author":"M.S. Bouassida","year":"2007","unstructured":"Bouassida, M.S., Chridi, N., Chrisment, I., Festor, O., Vigneron, L.: Automated verification of a key management architecture for hierarchical group protocols. Annales des T\u00e9l\u00e9communications\u00a062(11-12), 1365\u20131387 (2007)","journal-title":"Annales des T\u00e9l\u00e9communications"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-540-70545-1_38","volume-title":"Computer Aided Verification","author":"C.J.F. Cremers","year":"2008","unstructured":"Cremers, C.J.F.: The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 414\u2013418. Springer, Heidelberg (2008)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-01957-9_2","volume-title":"Applied Cryptography and Network Security","author":"C.J.F. Cremers","year":"2009","unstructured":"Cremers, C.J.F.: Session-state Reveal Is Stronger Than Ephemeral Key Reveal: Attacking the NAXOS Authenticated Key Exchange Protocol. In: Abdalla, M., Pointcheval, D., Fouque, P.-A., Vergnaud, D. (eds.) ACNS 2009. LNCS, vol.\u00a05536, pp. 20\u201333. Springer, Heidelberg (2009)"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-23822-2_18","volume-title":"Computer Security \u2013 ESORICS 2011","author":"C. Cremers","year":"2011","unstructured":"Cremers, C.: Key Exchange in IPsec Revisited: Formal Analysis of IKEv1 and IKEv2. In: Atluri, V., Diaz, C. (eds.) ESORICS 2011. LNCS, vol.\u00a06879, pp. 315\u2013334. Springer, Heidelberg (2011)"},{"issue":"2","key":"17_CR16","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.-C.: On the security of public key protocols. IEEE Transactions on Information Theory\u00a029(2), 198\u2013207 (1983)","journal-title":"IEEE Transactions on Information Theory"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"Fang, J., Jiang, R.: An analysis and improvement of 3GPP SAE AKA protocol based on strand space model. In: 2010 2nd IEEE International Conference on Network Infrastructure and Digital Content, pp. 789\u2013793 (September 2010)","DOI":"10.1109\/ICNIDC.2010.5657890"},{"issue":"5","key":"17_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The Model Checker SPIN. IEEE Trans. Software Eng.\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Software Eng."},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-45353-9_14","volume-title":"Topics in Cryptology - CT-RSA 2001","author":"M. Jakobsson","year":"2001","unstructured":"Jakobsson, M., Wetzel, S.: Security Weaknesses in Bluetooth. In: Naccache, D. (ed.) CT-RSA 2001. LNCS, vol.\u00a02020, pp. 176\u2013191. Springer, Heidelberg (2001)"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Lowe, G.: A Hierarchy of Authentication Specification. In: CSFW [2], pp. 31\u201344","DOI":"10.1109\/CSFW.1997.596782"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Lowe, G.: Casper: A Compiler for the Analysis of Security Protocols. In: CSFW [2], pp. 18\u201330","DOI":"10.1109\/CSFW.1997.596779"},{"issue":"2","key":"17_CR22","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL Protocol Analyzer: An Overview. J. Log. Program.\u00a026(2), 113\u2013131 (1996)","journal-title":"J. Log. Program."},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S. Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 696\u2013701. Springer, Heidelberg (2013)"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Qachri, N., Markowitch, O., Dricot, J.-M.: A formally Verififed Protocol for Secure Vertical Handovers in 4G Heterogeneous Networks. International Journal of Security and Its Applications\u00a07(6) (2013)","DOI":"10.14257\/ijsia.2013.7.6.32"},{"key":"17_CR25","unstructured":"Schmidt, B., Sasse, R., Basin, D.: Automated Verification of Group Key Agreement Protocols. In: IEEE Symposium on Security and Privacy (to appear, 2014)"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Taha, A.M., Abdel-Hamid, A.T., Tahar, S.: Formal analysis of the handover schemes in mobile WiMAX networks. In: IFIP International Conference on Wireless and Optical Communications Networks, WOCN 2009, pp. 1\u20135 (April 2009)","DOI":"10.1109\/WOCN.2009.5010502"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Taha, A.M., Abdel-Hamid, A.T., Tahar, S.: Formal Verification of IEEE 802.16 Security Sublayer Using Scyther Tool. In: International Conference on Network and Service Security, N2S 2009, pp. 1\u20135 (June 2009)","DOI":"10.1109\/WOCN.2009.5010502"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Tang, C., Naumann, D.A., Wetzel, S.: Symbolic Analysis for Security of Roaming Protocols in Mobile Networks - (Extended Abstract). In: Rajarajan, M., Piper, F., Wang, H., Kesidis, G. (eds.) SecureComm. LNICST, vol.\u00a096, pp. 480\u2013490. Springer (2011)","DOI":"10.1007\/978-3-642-31909-9_29"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-3-642-33704-8_6","volume-title":"Computer Network Security","author":"J.-K. Tsay","year":"2012","unstructured":"Tsay, J.-K., Mj\u00f8lsnes, S.F.: A Vulnerability in the UMTS and LTE Authentication and Key Agreement Protocols. In: Kotenko, I., Skormin, V. (eds.) MMM-ACNS 2012. LNCS, vol.\u00a07531, pp. 65\u201376. Springer, Heidelberg (2012)"},{"key":"17_CR30","unstructured":"Zhang, M., Fang, Y.: Security analysis and enhancements of 3gpp authentication and key agreement protocol"}],"container-title":["Lecture Notes in Computer Science","Research in Attacks, Intrusions and Defenses"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11379-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T08:27:11Z","timestamp":1746347231000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11379-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319113784","9783319113791"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11379-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}