{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T11:02:05Z","timestamp":1781607725896,"version":"3.54.5"},"publisher-location":"Cham","reference-count":54,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030620769","type":"print"},{"value":"9783030620776","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-62077-6_9","type":"book-chapter","created":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T11:25:37Z","timestamp":1603884337000},"page":"103-126","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Formal Methods Analysis of the Secure Remote Password Protocol"],"prefix":"10.1007","author":[{"given":"Alan T.","family":"Sherman","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Erin","family":"Lanus","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Moses","family":"Liskov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Edward","family":"Zieglar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Richard","family":"Chang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Enis","family":"Golaszewski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ryan","family":"Wnuk-Fink","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cyrus J.","family":"Bonyadi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mario","family":"Yaksetig","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ian","family":"Blumenfeld","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,10,28]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","unstructured":"Adrian, D., et al.: Imperfect forward secrecy: how Diffie-Hellman fails in practice. In: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, CCS 2015, pp. 5\u201317. ACM, New York (2015). \nhttps:\/\/doi.org\/10.1145\/2810103.2813707","DOI":"10.1145\/2810103.2813707"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Arapinis, M., et al.: New privacy issues in mobile telephony: fix and verification. In: Proceedings of the 2012 ACM Conference on Computer and Communications Security, CCS 2012, pp. 205\u2013216. Association for Computing Machinery, New York (2012). \nhttps:\/\/doi.org\/10.1145\/2382196.2382221","DOI":"10.1145\/2382196.2382221"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-319-08970-6_6","volume-title":"Interactive Theorem Proving","author":"E-I Bartzia","year":"2014","unstructured":"Bartzia, E.-I., Strub, P.-Y.: A formal library for elliptic curves in the Coq proof assistant. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 77\u201392. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08970-6_6"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/978-3-642-15497-3_21","volume-title":"Computer Security \u2013 ESORICS 2010","author":"D Basin","year":"2010","unstructured":"Basin, D., Cremers, C.: Modeling and analyzing security in the presence of compromising adversaries. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 340\u2013356. Springer, Heidelberg (2010). \nhttps:\/\/doi.org\/10.1007\/978-3-642-15497-3_21"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Basin, D., Cremers, C.: Know your enemy: compromising adversaries in protocol analysis. ACM Trans. Inf. Syst. Secur. 17(2) (2014). \nhttps:\/\/doi.org\/10.1145\/2658996","DOI":"10.1145\/2658996"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Bellovin, S.M., Merritt, M.: Encrypted key exchange: password-based protocols secure against dictionary attacks. In: IEEE Symposium on Research in Security and Privacy, pp. 72\u201384, May 1992","DOI":"10.1145\/168588.168618"},{"key":"9_CR7","unstructured":"Blake-Wilson, S., Menezes, A.: Authenticated Diffie-Hellman key agreement protocols. In: Proceedings of the Selected Areas in Cryptography, SAC 1998, pp. 339\u2013361. Springer, Heidelberg (1999). \nhttp:\/\/dl.acm.org\/citation.cfm?id=646554.694440"},{"key":"9_CR8","unstructured":"Blanchet, B., Smyth, B., Cheval, V.: Proverif 1.90: automatic cryptographic protocol verifier, user manual and tutorial (2015). \nhttp:\/\/prosecco.gforge.inria.fr\/personal\/bblanche\/proverif\/manual.pdf"},{"issue":"1","key":"9_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/JCS-140523","volume":"24","author":"F B\u00f6hl","year":"2016","unstructured":"B\u00f6hl, F., Unruh, D.: Symbolic universal composability. J. Comput. Secur. 24(1), 1\u201338 (2016)","journal-title":"J. Comput. Secur."},{"key":"9_CR10","unstructured":"Boneh, D., Shoup, V.: A graduate course in applied cryptography version 0.5, January 2020. \nhttps:\/\/crypto.stanford.edu\/~dabo\/cryptobook\/BonehShoup_0_5.pdf"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Browning, S.: Cryptol, a DSL for cryptographic algorithms. In: ACM SIGPLAN Commercial Users of Functional Programming, p. 1. ACM (2010)","DOI":"10.1145\/1900160.1900171"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: Proceedings of the 42nd IEEE Symposium on Foundations of Computer Science, FOCS 2001, p. 136. IEEE Computer Society, USA (2001)","DOI":"10.1109\/SFCS.2001.959888"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Canetti, R., Stoughton, A., Varia, M.: EasyUC: using EasyCrypt to mechanize proofs of universally composable security. In: 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), pp. 167\u2013183 (2019)","DOI":"10.1109\/CSF.2019.00019"},{"issue":"2","key":"9_CR14","doi-asserted-by":"publisher","first-page":"345","DOI":"10.2307\/2371045","volume":"58","author":"A Church","year":"1936","unstructured":"Church, A.: An unsolvable problem of elementary number theory. Am. J. Math. 58(2), 345\u2013363 (1936)","journal-title":"Am. J. Math."},{"key":"9_CR15","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.entcs.2004.10.007","volume":"121","author":"R Corin","year":"2005","unstructured":"Corin, R., Doumen, J., Etalle, S.: Analysing password protocol security against off-line dictionary attacks. Electron. Notes Theoret. Comput. Sci. 121, 47\u201363 (2005)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"9_CR16","unstructured":"Delaune, S., Kremer, S., Pereira, O.: Simulation based security in the applied pi calculus. In: Kannan, R., Kumar, K.N. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), vol. 4, pp. 169\u2013180. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2009). \nhttp:\/\/drops.dagstuhl.de\/opus\/volltexte\/2009\/2316"},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"Diffie, W., Hellman, M.: New directions in cryptography. IEEE Trans. Inf. Theor. 22(6), 644\u2013654 (2006). \nhttps:\/\/doi.org\/10.1023\/A:1008302122286","DOI":"10.1023\/A:1008302122286"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-319-52153-4_11","volume-title":"Topics in Cryptology \u2013 CT-RSA 2017","author":"J Ding","year":"2017","unstructured":"Ding, J., Alsayigh, S., Lancrenon, J., RV, S., Snook, M.: Provably secure password authenticated key exchange based on RLWE for the post-quantum world. In: Handschuh, H. (ed.) CT-RSA 2017. LNCS, vol. 10159, pp. 183\u2013204. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-52153-4_11"},{"key":"9_CR19","unstructured":"Doghmi, S., Guttman, J., Thayer, F.J.: Skeletons and the shapes of bundles. In: Proceedings of the 7th International Workshop on Issues in the Theory of Security, pp. 24\u201325 (2006)"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/978-3-540-71209-1_41","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"SF Doghmi","year":"2007","unstructured":"Doghmi, S.F., Guttman, J.D., Thayer, F.J.: Searching for shapes in cryptographic protocols. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 523\u2013537. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71209-1_41"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. In: Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, SFCS 1981, pp. 350\u2013357. IEEE Computer Society, Washington, DC (1981). \nhttps:\/\/doi.org\/10.1109\/SFCS.1981.32","DOI":"10.1109\/SFCS.1981.32"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-662-54455-6_6","volume-title":"Principles of Security and Trust","author":"J Dreier","year":"2017","unstructured":"Dreier, J., Dum\u00e9nil, C., Kremer, S., Sasse, R.: Beyond subterm-convergent equational theories in automated verification of stateful protocols. In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 117\u2013140. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54455-6_6\n\n. \nhttps:\/\/hal.inria.fr\/hal-01430490\/document"},{"issue":"1\u20132","key":"9_CR23","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/j.tcs.2006.08.035","volume":"367","author":"S Escobar","year":"2006","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theoret. Comput. Sci. 367(1\u20132), 162\u2013202 (2006)","journal-title":"Theoret. Comput. Sci."},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design V","author":"S Escobar","year":"2009","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-03829-7_1"},{"key":"9_CR25","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA, Version 3.0, April 2017"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Fabrega, F.J.T., Herzog, J.C., Guttman, J.D.: Strand spaces: why is a security protocol correct? In: Proceedings of the 1998 IEEE Symposium on Security and Privacy (Cat. No. 98CB36186), pp. 160\u2013171, May 1998. \nhttps:\/\/doi.org\/10.1109\/SECPRI.1998.674832","DOI":"10.1109\/SECPRI.1998.674832"},{"key":"9_CR27","unstructured":"Green, M.: Let\u2019s talk about PAKE, October 2018. \nhttps:\/\/blog.cryptographyengineering.com\/2018\/10\/19\/lets-talk-about-pake\/"},{"key":"9_CR28","unstructured":"Green, M.: Should you use SRP? October 2018. \nhttps:\/\/blog.cryptographyengineering.com\/should-you-use-srp\/"},{"key":"9_CR29","unstructured":"Guttman, J.D., Liskov, M.D., Ramsdell, J.D., Rowe, P.D.: The Cryptographic Protocol Shapes Analyzer (CPSA). \nhttps:\/\/github.com\/mitre\/cpsa"},{"key":"9_CR30","first-page":"1","volume":"2019","author":"B Haase","year":"2018","unstructured":"Haase, B., Labrique, B.: AuCPace: Efficient verifier-based PAKE protocol tailored for the IIoT. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2019, 1\u201348 (2018)","journal-title":"IACR Trans. Cryptogr. Hardw. Embed. Syst."},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-319-14054-4_2","volume-title":"Security Standardisation Research","author":"F Hao","year":"2014","unstructured":"Hao, F., Shahandashti, S.F.: The SPEKE protocol revisited. In: Chen, L., Mitchell, C. (eds.) SSR 2014. LNCS, vol. 8893, pp. 26\u201338. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-14054-4_2"},{"issue":"5","key":"9_CR32","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/242896.242897","volume":"26","author":"DP Jablon","year":"1996","unstructured":"Jablon, D.P.: Strong password-only authenticated key exchange. ACM Comput. Commun. Rev. 26(5), 5\u201326 (1996)","journal-title":"ACM Comput. Commun. Rev."},{"key":"9_CR33","unstructured":"Jarecki, S., Krawczyk, H., Xu, J.: OPAQUE: An asymmetric PAKE protocol secure against pre-computation attacks. Cryptology ePrint Archive, Report 2018\/163 (2018). \nhttps:\/\/eprint.iacr.org\/"},{"key":"9_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-319-78372-7_15","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2018","author":"S Jarecki","year":"2018","unstructured":"Jarecki, S., Krawczyk, H., Xu, J.: OPAQUE: an asymmetric PAKE protocol secure against pre-computation attacks. In: Nielsen, J.B., Rijmen, V. (eds.) EUROCRYPT 2018. LNCS, vol. 10822, pp. 456\u2013486. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-78372-7_15"},{"key":"9_CR35","unstructured":"Lanus, E., Zieglar, E.: Analysis of a forced-latency defense against man-in-the-middle attacks. J. Inf. Warfare 16(2), 66\u201378 (2017). \nhttps:\/\/www.jstor.org\/stable\/26502758"},{"key":"9_CR36","unstructured":"Liskov, M.D., Ramsdell, J.D., Guttman, J.D., Rowe, P.D.: The Cryptographic Protocol Shapes Analyzer: A Manual. The MITRE Corporation (2016)"},{"key":"9_CR37","doi-asserted-by":"crossref","unstructured":"Liskov, M.D., Rowe, P.D., Thayer, F.J.: Completeness of CPSA. Technical report MTR110479, The MITRE Corporation (2011)","DOI":"10.21236\/ADA562264"},{"key":"9_CR38","unstructured":"Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Inf. Process. Lett. 56(3), 131\u2013133 (1995). \nhttp:\/\/www.sciencedirect.com\/science\/article\/pii\/0020019095001442"},{"key":"9_CR39","doi-asserted-by":"publisher","unstructured":"Maurer, U.M., Wolf, S.: The Diffie-Hellman protocol. Des. Codes Cryptography 19(2\u20133), 147\u2013171 (2000). \nhttps:\/\/doi.org\/10.1023\/A:1008302122286","DOI":"10.1023\/A:1008302122286"},{"key":"9_CR40","unstructured":"Meadows, C.: NRL protocol analyzer. J. Comput. Secur. 1(1) (1992)"},{"key":"9_CR41","doi-asserted-by":"publisher","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993\u2013999 (1978). \nhttps:\/\/doi.org\/10.1145\/359657.359659","DOI":"10.1145\/359657.359659"},{"issue":"3","key":"9_CR42","doi-asserted-by":"publisher","first-page":"197","DOI":"10.3233\/JCS-2001-9302","volume":"9","author":"LC Paulson","year":"2001","unstructured":"Paulson, L.C.: Relations between secrets: two formal analyses of the Yahalom protocol. J. Comput. Secur. 9(3), 197\u2013216 (2001)","journal-title":"J. Comput. Secur."},{"key":"9_CR43","unstructured":"Ramsdell, J.D., Guttman, J.D., Millen, J.K., O\u2019Hanlon, B.: An analysis of the CAVES attestation protocol using CPSA. arXiv preprint \narXiv:1207.0418\n\n (2012)"},{"key":"9_CR44","doi-asserted-by":"publisher","unstructured":"Ryan, P.Y.A., Schneider, S.A.: An attack on a recursive authentication protocol. A cautionary tale. Inf. Process. Lett. 65(1), 7\u201310 (1998). \nhttps:\/\/doi.org\/10.1016\/S0020-0190(97)00180-4","DOI":"10.1016\/S0020-0190(97)00180-4"},{"key":"9_CR45","doi-asserted-by":"crossref","unstructured":"Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: 2012 IEEE 25th Computer Security Foundations Symposium, pp. 78\u201394, June 2012","DOI":"10.1109\/CSF.2012.25"},{"key":"9_CR46","unstructured":"Sherman, A.T., et al.: PAL GitHub repository, June 2020. \nhttps:\/\/github.com\/egolaszewski\/UMBC-Protocol-Analysis-Lab"},{"key":"9_CR47","unstructured":"Steiner, J.G., Neuman, B.C., Schiller, J.I.: Kerberos: an authentication service for open network systems. In: Proceedings Winter USENIX Conference, pp. 191\u2013202 (1988)"},{"key":"9_CR48","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/11596981_22","volume-title":"Computational Intelligence and Security","author":"Q Tang","year":"2005","unstructured":"Tang, Q., Mitchell, C.J.: On the security of some password-based key agreement schemes. In: Hao, Y., et al. (eds.) CIS 2005. LNCS (LNAI), vol. 3802, pp. 149\u2013154. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11596981_22"},{"key":"9_CR49","doi-asserted-by":"publisher","unstructured":"Taylor, D., Wu, T., Mavrogiannopoulos, N., Perrin, T.: RFC 5054, Using the secure remote password (SRP) protocol for TLS authentication. Technical report, RFC Editor, November 2007. \nhttps:\/\/doi.org\/10.17487\/rfc5054","DOI":"10.17487\/rfc5054"},{"key":"9_CR50","doi-asserted-by":"publisher","unstructured":"Wu, T.: RFC 2944, Telnet Authentication: SRP. Technical report, RFC Editor, September 2000. \nhttps:\/\/doi.org\/10.17487\/rfc2944","DOI":"10.17487\/rfc2944"},{"key":"9_CR51","unstructured":"Wu, T.: The secure remote password protocol. In: Proceedings of the Internet Society on Network and Distributed System Security (1998)"},{"key":"9_CR52","doi-asserted-by":"crossref","unstructured":"Wu, T.: The SRP Authentication and Key Exchange System, RFC 2945, September 2000","DOI":"10.17487\/rfc2945"},{"key":"9_CR53","unstructured":"Wu, T.: SRP-6: Improvements and Refinements to the Secure Remote Password Protocol, October 2002"},{"issue":"1","key":"9_CR54","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1109\/LCOMM.2003.822506","volume":"8","author":"M Zhang","year":"2004","unstructured":"Zhang, M.: Analysis of the SPEKE password-authenticated key exchange protocol. IEEE Commun. Lett. 8(1), 63\u201365 (2004). \nhttps:\/\/doi.org\/10.1109\/LCOMM.2003.822506","journal-title":"IEEE Commun. Lett."}],"container-title":["Lecture Notes in Computer Science","Logic, Language, and Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-62077-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T12:08:26Z","timestamp":1603886906000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-62077-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030620769","9783030620776"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-62077-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"28 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}