{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:38:50Z","timestamp":1742913530398,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031067877"},{"type":"electronic","value":"9783031067884"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-06788-4_42","type":"book-chapter","created":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:03:27Z","timestamp":1656889407000},"page":"500-512","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formal Verification of\u00a0Security Protocols: ProVerif and\u00a0Extensions"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6337-0728","authenticated-orcid":false,"given":"Jiangyuan","family":"Yao","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3391-8582","authenticated-orcid":false,"given":"Chunxiang","family":"Xu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2026-9288","authenticated-orcid":false,"given":"Deshun","family":"Li","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4180-8949","authenticated-orcid":false,"given":"Shengjun","family":"Lin","sequence":"additional","affiliation":[]},{"given":"Xingcan","family":"Cao","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,7,4]]},"reference":[{"key":"42_CR1","doi-asserted-by":"crossref","unstructured":"Aizatulin, M., Gordon, A.D., J\u00fcrjens, J.: Extracting and verifying cryptographic models from c protocol code by symbolic execution. In: Proceedings of the 18th ACM Conference on Computer and Communications Security, pp. 331\u2013340 (2011)","DOI":"10.1145\/2046707.2046745"},{"issue":"1","key":"42_CR2","first-page":"229","volume":"68","author":"A Akhter","year":"2021","unstructured":"Akhter, A., Shah, A., Ahmed, M., Moustafa, N., Cavusoglu, U., Zengin, A.: A secured message transmission protocol for vehicular ad hoc networks. Comput. Mater. Contin. 68(1), 229\u2013246 (2021)","journal-title":"Comput. Mater. Contin."},{"key":"42_CR3","doi-asserted-by":"publisher","unstructured":"Arapinis, M., Ritter, E., Ryan, M.D.: StatVerif: verification of stateful processes. In: 2011 IEEE 24th Computer Security Foundations Symposium, pp. 33\u201347 (2011). https:\/\/doi.org\/10.1109\/CSF.2011.10","DOI":"10.1109\/CSF.2011.10"},{"key":"42_CR4","doi-asserted-by":"publisher","unstructured":"Avalle, M., Pironti, A., Sisto, R., Pozza, D.: The Java SPI framework for security protocol implementation. In: 2011 Sixth International Conference on Availability, Reliability and Security, pp. 746\u2013751 (2011). https:\/\/doi.org\/10.1109\/ARES.2011.117","DOI":"10.1109\/ARES.2011.117"},{"key":"42_CR5","doi-asserted-by":"publisher","unstructured":"Bansal, C., Bhargavan, K., Maffeis, S.: Discovering concrete attacks on website authorization by formal analysis. In: 2012 IEEE 25th Computer Security Foundations Symposium, pp. 247\u2013262 (2012). https:\/\/doi.org\/10.1109\/CSF.2012.27","DOI":"10.1109\/CSF.2012.27"},{"key":"42_CR6","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., Fournet, C., Gordon, A., Tse, S.: Verified interoperable implementations of security protocols. In: 19th IEEE Computer Security Foundations Workshop (CSFW 2006), pp. 14\u2013152 (2006). https:\/\/doi.org\/10.1109\/CSFW.2006.32","DOI":"10.1109\/CSFW.2006.32"},{"key":"42_CR7","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: 2017 IEEE Symposium on Security and Privacy (SP), pp. 483\u2013502. IEEE (2017)","DOI":"10.1109\/SP.2017.26"},{"key":"42_CR8","doi-asserted-by":"crossref","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)","DOI":"10.1561\/3300000004"},{"key":"42_CR9","doi-asserted-by":"publisher","unstructured":"Blanchet, B.: Symbolic and computational mechanized verification of the arinc823 avionic protocols. In: 2017 IEEE 30th Computer Security Foundations Symposium (CSF), pp. 68\u201382 (2017). https:\/\/doi.org\/10.1109\/CSF.2017.7","DOI":"10.1109\/CSF.2017.7"},{"key":"42_CR10","unstructured":"Blanchet, B., Smyth, B., Cheval, V., Sylvestre, M.: ProVerif 2.02 pl1: automatic cryptographic protocol verifier, user manual and tutorial (2020)"},{"key":"42_CR11","doi-asserted-by":"publisher","unstructured":"Cheval, V., Cortier, V., Turuani, M.: A little more conversation, a little less action, a lot more satisfaction: global states in ProVerif. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp. 344\u2013358 (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00032","DOI":"10.1109\/CSF.2018.00032"},{"issue":"2","key":"42_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 Trans. Inf. Theory 29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"13","key":"42_CR13","doi-asserted-by":"publisher","first-page":"1608","DOI":"10.3390\/electronics10131608","volume":"10","author":"EKK Edris","year":"2021","unstructured":"Edris, E.K.K., Aiash, M., Loo, J.: Formal verification of authentication and service authorization protocols in 5G-enabled device-to-device communications using ProVerif. Electronics 10(13), 1608 (2021)","journal-title":"Electronics"},{"issue":"3","key":"42_CR14","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1016\/j.eij.2020.01.001","volume":"21","author":"E Elemam","year":"2020","unstructured":"Elemam, E., Bahaa-Eldin, A.M., Shaker, N.H., Sobh, M.: Formal verification for a PMQTT protocol. Egypt. Inform. J. 21(3), 169\u2013182 (2020)","journal-title":"Egypt. Inform. J."},{"key":"42_CR15","doi-asserted-by":"crossref","unstructured":"Feng, H., Li, H., Pan, X., Zhao, Z., Cactilab, T.: A formal analysis of the FIDO UAF protocol. In: Proceedings of the Network and Distributed Systems Security (NDSS) Symposium, pp. 1\u201315 (2021)","DOI":"10.14722\/ndss.2021.24363"},{"key":"42_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-30579-8_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J Goubault-Larrecq","year":"2005","unstructured":"Goubault-Larrecq, J., Parrennes, F.: Cryptographic protocol analysis on real C code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 363\u2013379. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30579-8_24"},{"key":"42_CR17","doi-asserted-by":"crossref","unstructured":"Guirat, I.B., Halpin, H.: Formal verification of the W3C web authentication protocol. In: 5th Annual Symposium and Bootcamp on Hot Topics in the Science of Security, HoTSoS 2018, pp. 1\u201310. ACM (2018)","DOI":"10.1145\/3190619.3190640"},{"key":"42_CR18","doi-asserted-by":"publisher","first-page":"2300","DOI":"10.1109\/TIFS.2021.3053371","volume":"16","author":"S Han","year":"2021","unstructured":"Han, S., et al.: Log-based anomaly detection with robust feature extraction and online learning. IEEE Trans. Inf. Forensics Secur. 16, 2300\u20132311 (2021). https:\/\/doi.org\/10.1109\/TIFS.2021.3053371","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"issue":"2","key":"42_CR19","doi-asserted-by":"publisher","first-page":"347","DOI":"10.32604\/iasc.2021.012401","volume":"27","author":"R Jayamala","year":"2021","unstructured":"Jayamala, R., Valarmathi, A.: An enhanced decentralized virtual machine migration approach for energy-aware cloud data centers. Intell. Autom. Soft Comput. 27(2), 347\u2013358 (2021)","journal-title":"Intell. Autom. Soft Comput."},{"key":"42_CR20","doi-asserted-by":"publisher","unstructured":"Kobeissi, N., Nicolas, G., Bhargavan, K.: Noise explorer: fully automated modeling and verification for arbitrary noise protocols. In: 2019 IEEE European Symposium on Security and Privacy (EuroS P), pp. 356\u2013370 (2019). https:\/\/doi.org\/10.1109\/EuroSP.2019.00034","DOI":"10.1109\/EuroSP.2019.00034"},{"issue":"3\u20134","key":"42_CR21","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/s10817-010-9188-8","volume":"46","author":"R K\u00fcsters","year":"2011","unstructured":"K\u00fcsters, R., Truderung, T.: Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach. J. Autom. Reason. 46(3\u20134), 325\u2013352 (2011)","journal-title":"J. Autom. Reason."},{"key":"42_CR22","doi-asserted-by":"publisher","unstructured":"K\u00fcsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In: 2009 22nd IEEE Computer Security Foundations Symposium, pp. 157\u2013171 (2009). https:\/\/doi.org\/10.1109\/CSF.2009.17","DOI":"10.1109\/CSF.2009.17"},{"key":"42_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-642-12459-4_13","volume-title":"Formal Aspects in Security and Trust","author":"P Lafourcade","year":"2010","unstructured":"Lafourcade, P., Terrade, V., Vigier, S.: Comparison of cryptographic verification tools dealing with algebraic properties. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol. 5983, pp. 173\u2013185. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12459-4_13"},{"key":"42_CR24","doi-asserted-by":"crossref","unstructured":"May, M.J., Lux, K.D., Gunter, C.A.: WSEmail: a retrospective on a system for secure internet messaging based on web services. arXiv preprint arXiv:1908.02108 (2019)","DOI":"10.1007\/s11761-019-00283-9"},{"key":"42_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-662-49635-0_12","volume-title":"Principles of Security and Trust","author":"S M\u00f6dersheim","year":"2016","unstructured":"M\u00f6dersheim, S., Bruni, A.: AIF-$$\\omega $$: set-based protocol abstraction with countable families. In: Piessens, F., Vigan\u00f2, L. (eds.) POST 2016. LNCS, vol. 9635, pp. 233\u2013253. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49635-0_12"},{"issue":"2","key":"42_CR26","first-page":"607","volume":"59","author":"Z Qu","year":"2019","unstructured":"Qu, Z., Wu, S., Liu, W., Wang, X.: Analysis and improvement of steganography protocol based on bell states in noise environment. Comput. Mater. Contin. 59(2), 607\u2013624 (2019)","journal-title":"Comput. Mater. Contin."},{"key":"42_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-030-29436-6_21","volume-title":"Automated Deduction \u2013 CADE 27","author":"DL Li","year":"2019","unstructured":"Li, D.L., Tiu, A.: Combining ProVerif and automated theorem provers for security protocol verification. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 354\u2013365. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_21"},{"issue":"6","key":"42_CR28","doi-asserted-by":"publisher","first-page":"2458","DOI":"10.1109\/TNET.2019.2951925","volume":"27","author":"H Zhang","year":"2019","unstructured":"Zhang, H., et al.: Da&fd-deadline-aware and flow duration-based rate control for mixed flows in DCNs. IEEE\/ACM Trans. Netw. 27(6), 2458\u20132471 (2019). https:\/\/doi.org\/10.1109\/TNET.2019.2951925","journal-title":"IEEE\/ACM Trans. Netw."},{"key":"42_CR29","doi-asserted-by":"publisher","first-page":"23674","DOI":"10.1109\/ACCESS.2020.2969474","volume":"8","author":"J Zhang","year":"2020","unstructured":"Zhang, J., Yang, L., Cao, W., Wang, Q.: Formal analysis of 5G EAP-TLS authentication protocol using ProVerif. IEEE Access 8, 23674\u201323688 (2020). https:\/\/doi.org\/10.1109\/ACCESS.2020.2969474","journal-title":"IEEE Access"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-06788-4_42","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,13]],"date-time":"2022-07-13T12:27:39Z","timestamp":1657715259000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-06788-4_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031067877","9783031067884"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-06788-4_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"4 July 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICAIS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Artificial Intelligence and Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Qinghai","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 July 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"incodldos2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.icaisconf.com\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"CMT","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1124","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"115","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"53","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}