{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,9]],"date-time":"2026-02-09T23:03:32Z","timestamp":1770678212881,"version":"3.49.0"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030294359","type":"print"},{"value":"9783030294366","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-29436-6_21","type":"book-chapter","created":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T16:04:02Z","timestamp":1566317042000},"page":"354-365","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Combining ProVerif and Automated Theorem Provers for Security Protocol Verification"],"prefix":"10.1007","author":[{"given":"Di Long","family":"Li","sequence":"first","affiliation":[]},{"given":"Alwen","family":"Tiu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,20]]},"reference":[{"issue":"1","key":"21_CR1","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/1044731.1044735","volume":"52","author":"M Abadi","year":"2005","unstructured":"Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. J. ACM 52(1), 102\u2013146 (2005). https:\/\/doi.org\/10.1145\/1044731.1044735","journal-title":"J. ACM"},{"key":"21_CR2","doi-asserted-by":"publisher","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2001, pp. 104\u2013115. ACM, New York (2001). https:\/\/doi.org\/10.1145\/360204.360213","DOI":"10.1145\/360204.360213"},{"key":"21_CR3","doi-asserted-by":"publisher","unstructured":"Basin, D., Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R., Stettler, V.: A formal analysis of 5G authentication. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, pp. 1383\u20131396. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3243734.3243846","DOI":"10.1145\/3243734.3243846"},{"key":"21_CR4","doi-asserted-by":"publisher","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of 14th IEEE Computer Security Foundations Workshop, 2001. pp. 82\u201396, June 2001. https:\/\/doi.org\/10.1109\/CSFW.2001.930138","DOI":"10.1109\/CSFW.2001.930138"},{"issue":"1\u20132","key":"21_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1561\/3300000004","volume":"1","author":"B Blanchet","year":"2016","unstructured":"Blanchet, B.: Modeling and verifying security protocols with the applied pi calculus and proVerif. Found. Trends\u00ae Priv. Secur. 1(1\u20132), 1\u2013135 (2016). https:\/\/doi.org\/10.1561\/3300000004","journal-title":"Found. Trends\u00ae Priv. Secur."},{"key":"21_CR6","unstructured":"Blanchet, B., Smyth, B., Cheval, V., Sylvestre, M.: ProVerif 2.00: automatic cryptographic protocol verifier, user manual and tutorial. Technical report (2018)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-540-77092-3_37","volume-title":"Embedded and Ubiquitous Computing","author":"H-Y Chien","year":"2007","unstructured":"Chien, H.-Y., Huang, C.-W.: A lightweight RFID protocol using substring. In: Kuo, T.-W., Sha, E., Guo, M., Yang, L.T., Shao, Z. (eds.) EUC 2007. LNCS, vol. 4808, pp. 422\u2013431. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-77092-3_37"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-32033-3_22","volume-title":"Term Rewriting and Applications","author":"H Comon-Lundh","year":"2005","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294\u2013307. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_22"},{"issue":"1","key":"21_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.3233\/jcs-2006-14101","volume":"14","author":"V Cortier","year":"2006","unstructured":"Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur. 14(1), 1\u201343 (2006). https:\/\/doi.org\/10.3233\/jcs-2006-14101","journal-title":"J. Comput. Secur."},{"key":"21_CR10","unstructured":"van Deursen, T., Radomirovic, S.: Attacks on RFID protocols. IACR Cryptology ePrint Archive 2008, 310 (2008). http:\/\/eprint.iacr.org\/2008\/310"},{"key":"21_CR11","doi-asserted-by":"publisher","unstructured":"Dierks, T., Rescorla, E.: The transport layer security (TLS) protocol version 1.2. Technical report, August 2008. https:\/\/doi.org\/10.17487\/rfc5246","DOI":"10.17487\/rfc5246"},{"issue":"2","key":"21_CR12","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.: On the security of public key protocols. IEEE Transact. Inf. Theory 29(2), 198\u2013208 (1983). https:\/\/doi.org\/10.1109\/TIT.1983.1056650","journal-title":"IEEE Transact. Inf. Theory"},{"key":"21_CR13","doi-asserted-by":"publisher","unstructured":"Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R.: Automated unbounded verification of stateful cryptographic protocols with exclusive or. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp. 359\u2013373, July 2018. https:\/\/doi.org\/10.1109\/CSF.2018.00033","DOI":"10.1109\/CSF.2018.00033"},{"key":"21_CR14","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). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_1"},{"key":"21_CR15","unstructured":"Escobar, S., Meadows, C.A., Meseguer, J.: Maude-NPA, Version 3.1. Technical report (2017)"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"21_CR17","doi-asserted-by":"publisher","unstructured":"Lowe, G.: A hierarchy of authentication specifications. In: Proceedings 10th Computer Security Foundations Workshop, pp. 31\u201343, June 1997. https:\/\/doi.org\/10.1109\/CSFW.1997.596782","DOI":"10.1109\/CSFW.1997.596782"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder Public-Key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147\u2013166. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61042-1_43"},{"key":"21_CR19","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. 8044, pp. 696\u2013701. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"},{"issue":"12","key":"21_CR20","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"RM Needham","year":"1978","unstructured":"Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993\u2013999 (1978). https:\/\/doi.org\/10.1145\/359657.359659","journal-title":"Commun. ACM"},{"key":"21_CR21","doi-asserted-by":"publisher","unstructured":"Reger, G.: Better proof output for vampire. In: Kovacs, L., Voronkov, A. (eds.) Proceedings of the 3rd Vampire Workshop, Vampire 2016. EPiC Series in Computing, vol. 44, pp. 46\u201360. EasyChair (2017). https:\/\/doi.org\/10.29007\/5dmz, https:\/\/easychair.org\/publications\/paper\/1DlL","DOI":"10.29007\/5dmz"},{"issue":"1","key":"21_CR22","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/S0020-0190(97)00180-4,","volume":"65","author":"P Ryan","year":"1998","unstructured":"Ryan, P., Schneider, S.: An attack on a recursive authentication protocol a cautionary tale. Inf. Process. Lett. 65(1), 7\u201310 (1998). https:\/\/doi.org\/10.1016\/S0020-0190(97)00180-4,. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S0020019097001804","journal-title":"Inf. Process. Lett."},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/11532231_24","volume-title":"Automated Deduction \u2013 CADE-20","author":"G Steel","year":"2005","unstructured":"Steel, G.: Deduction with XOR constraints in security API modelling. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 322\u2013336. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11532231_24"},{"issue":"4","key":"21_CR24","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reasoning 59(4), 483\u2013502 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9407-7","journal-title":"J. Autom. Reasoning"},{"key":"21_CR25","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.entcs.2005.11.052","volume":"155","author":"L Vigan\u00f2","year":"2006","unstructured":"Vigan\u00f2, L.: Automated security protocol analysis with the AVISPA tool. Electron. Notes Theor. Comput. Sci. 155, 61\u201386 (2006). https:\/\/doi.org\/10.1016\/j.entcs.2005.11.052. http:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066106001897 proceedings of the 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-319-08867-9_46","volume-title":"Computer Aided Verification","author":"A Voronkov","year":"2014","unstructured":"Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696\u2013710. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_46"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10"},{"issue":"1","key":"21_CR28","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1109\/2.108052","volume":"25","author":"TYC Woo","year":"1992","unstructured":"Woo, T.Y.C., Lam, S.S.: Authentication for distributed systems. Computer 25(1), 39\u201352 (1992). https:\/\/doi.org\/10.1109\/2.108052","journal-title":"Computer"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 27"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29436-6_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,11]],"date-time":"2022-07-11T21:55:14Z","timestamp":1657576514000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29436-6_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030294359","9783030294366"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29436-6_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"20 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Natal","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 August 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 August 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.mat.ufrn.br\/CADE-27\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}