{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T23:08:28Z","timestamp":1781651308025,"version":"3.54.5"},"publisher-location":"Cham","reference-count":69,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030652760","type":"print"},{"value":"9783030652777","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-65277-7_8","type":"book-chapter","created":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T12:17:34Z","timestamp":1607343454000},"page":"151-202","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Verifpal: Cryptographic Protocol Analysis for the Real World"],"prefix":"10.1007","author":[{"given":"Nadim","family":"Kobeissi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Georgio","family":"Nicolas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mukesh","family":"Tiwari","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,12,8]]},"reference":[{"issue":"1","key":"8_CR1","doi-asserted-by":"publisher","first-page":"1:1","DOI":"10.1145\/3127586","volume":"65","author":"M Abadi","year":"2018","unstructured":"Abadi, M., Blanchet, B., Fournet, C.: The applied pi calculus: mobile values, new names, and secure communication. J. ACM 65(1), 1:1\u20131:41 (2018). https:\/\/doi.org\/10.1145\/3127586","journal-title":"J. ACM"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Amin, R., Islam, S.H., Karati, A., Biswas, G.: Design of an enhanced authentication protocol and its verification using AVISPA. In: 2016 3rd International Conference on Recent Advances in Information Technology (RAIT), pp. 404\u2013409. IEEE (2016)","DOI":"10.1109\/RAIT.2016.7507936"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-642-28756-5_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Armando","year":"2012","unstructured":"Armando, A., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 267\u2013282. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28756-5_19"},{"key":"8_CR4","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. 3576, pp. 281\u2013285. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_27"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Backes, M., Hritcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: IEEE Computer Security Foundations Symposium, pp. 195\u2013209. IEEE (2008)","DOI":"10.1109\/CSF.2008.26"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Baelde, D., Delaune, S., Moreau, S.: A method for proving unlinkability of stateful protocols. Ph.D. thesis, Irisa (2020)","DOI":"10.1109\/CSF49147.2020.00020"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Barbosa, M., et al.: SoK: computer-aided cryptography. In: IEEE Symposium on Security and Privacy (S&P). IEEE (2021)","DOI":"10.1109\/SP40001.2021.00008"},{"key":"8_CR8","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). https:\/\/doi.org\/10.1007\/978-3-642-15497-3_21"},{"key":"8_CR9","doi-asserted-by":"crossref","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, pp. 1383\u20131396. ACM (2018)","DOI":"10.1145\/3243734.3243846"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Basin, D., Radomirovic, S., Schmid, L.: Alethea: a provably secure random sample voting protocol. In: IEEE 31st Computer Security Foundations Symposium (CSF), pp. 283\u2013297. IEEE (2018)","DOI":"10.1109\/CSF.2018.00028"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-15205-4_1","volume-title":"Computer Science Logic","author":"D Basin","year":"2010","unstructured":"Basin, D., Cremers, C.: Degrees of security: protocol guarantees in the face of compromising adversaries. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 1\u201318. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15205-4_1"},{"issue":"2","key":"8_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1890028.1890031","volume":"33","author":"J Bengtson","year":"2011","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. ACM Trans. Program. Lang. Syst. (TOPLAS) 33(2), 1\u201345 (2011)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"8_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2013","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Beurdouche, B., et al.: A messy state of the union: taming the composite state machines of TLS. In: IEEE Symposium on Security and Privacy (S&P), pp. 535\u2013552. IEEE (2015)","DOI":"10.1109\/SP.2015.39"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: IEEE Symposium on Security and Privacy (S&P), pp. 483\u2013502. IEEE (2017)","DOI":"10.1109\/SP.2017.26"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/978-3-319-70972-7_32","volume-title":"Financial Cryptography and Data Security","author":"K Bhargavan","year":"2017","unstructured":"Bhargavan, K., Delignat-Lavaud, A., Kobeissi, N.: Formal modeling and verification for domain validation and ACME. In: Kiayias, A. (ed.) FC 2017. LNCS, vol. 10322, pp. 561\u2013578. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70972-7_32"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Lavaud, A.D., Fournet, C., Pironti, A., Strub, P.Y.: Triple handshakes and cookie cutters: breaking and fixing authentication over TLS. In: IEEE Symposium on Security and Privacy (S&P), pp. 98\u2013113. IEEE (2014)","DOI":"10.1109\/SP.2014.14"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Leurent, G.: On the practical (in-) security of 64-bit block ciphers: collision attacks on HTTP over TLS and OpenVPN. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 456\u2013467 (2016)","DOI":"10.1145\/2976749.2978423"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: CryptoVerif: computationally sound mechanized prover for cryptographic protocols. In: Dagstuhl Seminar on Applied Formal Protocol Verification, p. 117 (2007)","DOI":"10.1109\/SP.2006.1"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-28641-4_2","volume-title":"Principles of Security and Trust","author":"B Blanchet","year":"2012","unstructured":"Blanchet, B.: Security protocol verification: symbolic and computational models. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol. 7215, pp. 3\u201329. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28641-4_2"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-319-10082-1_3","volume-title":"Foundations of Security Analysis and Design VII","author":"B Blanchet","year":"2014","unstructured":"Blanchet, B.: Automatic verification of security protocols in the symbolic model: the verifier ProVerif. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 54\u201387. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10082-1_3"},{"issue":"1\u20132","key":"8_CR22","first-page":"1","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)","journal-title":"Found. Trends\u00ae Priv. Secur."},{"key":"8_CR23","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 (S&P), pp. 417\u2013431. IEEE (2008)","DOI":"10.1109\/SP.2008.12"},{"key":"8_CR24","unstructured":"Blum, J., et al.: E2E encryption for Zoom meetings (2020). https:\/\/github.com\/zoom\/zoom-e2e-whitepaper"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-319-68687-5_7","volume-title":"Electronic Voting","author":"A Bruni","year":"2017","unstructured":"Bruni, A., Drewsen, E., Sch\u00fcrmann, C.: Towards a mechanized proof of selene receipt-freeness and vote-privacy. In: Krimmer, R., Volkamer, M., Braun Binder, N., Kersting, N., Pereira, O., Sch\u00fcrmann, C. (eds.) E-Vote-ID 2017. LNCS, vol. 10615, pp. 110\u2013126. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68687-5_7"},{"issue":"1","key":"8_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0743-1066(85)90002-0","volume":"2","author":"AK Chandra","year":"1985","unstructured":"Chandra, A.K., Harel, D.: Horn clause queries and generalizations. J. Log. Program. 2(1), 1\u201315 (1985)","journal-title":"J. Log. Program."},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-642-36830-1_12","volume-title":"Principles of Security and Trust","author":"V Cheval","year":"2013","unstructured":"Cheval, V., Blanchet, B.: Proving more observational equivalences with ProVerif. In: Basin, D., Mitchell, J.C. (eds.) POST 2013. LNCS, vol. 7796, pp. 226\u2013246. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36830-1_12"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Cheval, V., Kremer, S., Rakotonirina, I.: DEEPSEC: deciding equivalence properties in security protocols theory and practice. Research report, INRIA, Nancy, May 2018. https:\/\/hal.inria.fr\/hal-01698177","DOI":"10.1109\/SP.2018.00033"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Cohn-Gordon, K., Cremers, C., Dowling, B., Garratt, L., Stebila, D.: A formal security analysis of the signal messaging protocol. In: 2017 IEEE European Symposium on Security and Privacy (EuroS&P), pp. 451\u2013466. IEEE (2017)","DOI":"10.1109\/EuroSP.2017.27"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Cohn-Gordon, K., Cremers, C., Garratt, L.: On post-compromise security. In: IEEE Computer Security Foundations Symposium (CSF), pp. 164\u2013178. IEEE (2016)","DOI":"10.1109\/CSF.2016.19"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-642-28641-4_7","volume-title":"Principles of Security and Trust","author":"V Cortier","year":"2012","unstructured":"Cortier, V., Wiedling, C.: A formal analysis of the norwegian E-voting protocol. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol. 7215, pp. 109\u2013128. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28641-4_7"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Cremers, C., Dehnel-Wild, M.: Component-based formal analysis of 5G-AKA: channel assumptions and session confusion. In: 2019 Network and Distributed System Security Symposium (NDSS) (2019)","DOI":"10.14722\/ndss.2019.23394"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Cremers, C., Hirschi, L.: Improving automated symbolic analysis of ballot secrecy for E-voting protocols: a method based on sufficient conditions. In: IEEE European Symposium on Security and Privacy (EuroS&P) (2019)","DOI":"10.1109\/EuroSP.2019.00052"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Cremers, C., Horvat, M., Hoyland, J., Scott, S., van der Merwe, T.: A comprehensive symbolic analysis of TLS 1.3. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 1773\u20131788. ACM (2017)","DOI":"10.1145\/3133956.3134063"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Cremers, C., Jackson, D.: Prime, order please! Revisiting small subgroup and invalid curve attacks on protocols using Diffie-Hellman. In: 2019 IEEE Computer Security Foundations Symposium (CSF) (2019)","DOI":"10.1109\/CSF.2019.00013"},{"key":"8_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-02002-5_5","volume-title":"Formal to Practical Security","author":"CJF Cremers","year":"2009","unstructured":"Cremers, C.J.F., Lafourcade, P., Nadeau, P.: Comparing state spaces in automatic security protocol analysis. In: Cortier, V., Kirchner, C., Okada, M., Sakurada, H. (eds.) Formal to Practical Security. LNCS, vol. 5458, pp. 70\u201394. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02002-5_5"},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"Cremers, C.: Feasibility of multi-protocol attacks. In: Proceedings of the First International Conference on Availability, Reliability and Security (ARES), pp. 287\u2013294. IEEE Computer Society, Vienna, April 2006. http:\/\/www.win.tue.nl\/~ecss\/downloads\/mpa-ares.pdf","DOI":"10.1109\/ARES.2006.63"},{"key":"8_CR38","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":"CJF 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. 5123, pp. 414\u2013418. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_38"},{"key":"8_CR39","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. 6879, pp. 315\u2013334. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23822-2_18"},{"key":"8_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"4","key":"8_CR41","doi-asserted-by":"publisher","first-page":"435","DOI":"10.3233\/JCS-2009-0340","volume":"17","author":"S Delaune","year":"2009","unstructured":"Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4), 435\u2013487 (2009)","journal-title":"J. Comput. Secur."},{"key":"8_CR42","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). https:\/\/doi.org\/10.1007\/978-3-540-71209-1_41"},{"issue":"2","key":"8_CR43","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"},{"key":"8_CR44","doi-asserted-by":"crossref","unstructured":"Donenfeld, J.A.: WireGuard: next generation kernel network tunnel. In: Network and Distributed System Security Symposium (NDSS) (2017)","DOI":"10.14722\/ndss.2017.23160"},{"key":"8_CR45","unstructured":"Donenfeld, J.A., Milner, K.: Formal verification of the WireGuard protocol. Technical report (2017)"},{"key":"8_CR46","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":"8_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-54862-8_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3\u2014a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13"},{"key":"8_CR48","unstructured":"Girol, G., Hirschi, L., Sasse, R., Jackson, D., Cremers, C., Basin, D.: A spectral analysis of noise: a comprehensive, automated, formal analysis of Diffie-Hellman protocols. In: 29th USENIX Security Symposium (USENIX Security 2020). USENIX Association, Boston, August 2020. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/girol"},{"key":"8_CR49","doi-asserted-by":"crossref","unstructured":"Hirschi, L., Baelde, D., Delaune, S.: A method for verifying privacy-type properties: the unbounded case. In: 2016 IEEE Symposium on Security and Privacy (SP), pp. 564\u2013581. IEEE (2016)","DOI":"10.1109\/SP.2016.40"},{"key":"8_CR50","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-1-4757-3472-0_16","volume-title":"The Origin of Concurrent Programming","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. In: Hansen, P.B. (ed.) The Origin of Concurrent Programming, pp. 413\u2013443. Springer, New York (1978). https:\/\/doi.org\/10.1007\/978-1-4757-3472-0_16"},{"key":"8_CR51","doi-asserted-by":"crossref","unstructured":"Jackson, D., Cremers, C., Cohn-Gordon, K., Sasse, R.: Seems legit: automated analysis of subtle attacks on protocols that use signatures. In: ACM CCS 2019 (2019)","DOI":"10.1145\/3319535.3339813"},{"key":"8_CR52","doi-asserted-by":"crossref","unstructured":"Jakobsen, J., Orlandi, C.: On the CCA (in) security of MTProto. In: Proceedings of the 6th Workshop on Security and Privacy in Smartphones and Mobile Devices, pp. 113\u2013116 (2016)","DOI":"10.1145\/2994459.2994468"},{"key":"8_CR53","unstructured":"Kobeissi, N.: An analysis of the protonmail cryptographic architecture. IACR Cryptology ePrint Archive 2018\/1121 (2018)"},{"key":"8_CR54","doi-asserted-by":"crossref","unstructured":"Kobeissi, N., Bhargavan, K., Blanchet, B.: Automated verification for secure messaging protocols and their implementations: a symbolic and computational approach. In: IEEE European Symposium on Security and Privacy (EuroS&P), pp. 435\u2013450. IEEE (2017)","DOI":"10.1109\/EuroSP.2017.38"},{"key":"8_CR55","doi-asserted-by":"crossref","unstructured":"Kobeissi, N., Nicolas, G., Bhargavan, K.: Noise explorer: fully automated modeling and verification for arbitrary noise protocols. In: IEEE European Symposium on Security and Privacy (EuroS&P) (2019)","DOI":"10.1109\/EuroSP.2019.00034"},{"key":"8_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-319-30303-1_9","volume-title":"Foundations and Practice of Security","author":"P Lafourcade","year":"2016","unstructured":"Lafourcade, P., Puys, M.: Performance evaluations of cryptographic protocols verification tools dealing with algebraic properties. In: Garcia-Alfaro, J., Kranakis, E., Bonfante, G. (eds.) FPS 2015. LNCS, vol. 9482, pp. 137\u2013155. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-30303-1_9"},{"key":"8_CR57","unstructured":"Lapiha, O.: A cryptographic investigation of secure scuttlebutt. Technical report, \u00c9cole Normale Sup\u00e9rieure (2019)"},{"key":"8_CR58","unstructured":"Lee, J., Choi, R., Kim, S., Kim, K.: Security analysis of end-to-end encryption in telegram. In: Simposio en Criptograf\u00eda Seguridad Inform\u00e1tica, Naha, Jap\u00f3n (2017). https:\/\/bit.ly\/36aX3TK"},{"key":"8_CR59","doi-asserted-by":"crossref","unstructured":"Lipp, B., Blanchet, B., Bhargavan, K.: A mechanised cryptographic proof of the WireGuard virtual private network protocol. In: IEEE European Symposium on Security and Privacy (EuroS&P) (2019)","DOI":"10.1109\/EuroSP.2019.00026"},{"key":"8_CR60","unstructured":"Miculan, M., Urban, C.: Formal analysis of Facebook connect single sign-on authentication protocol. In: SOFSEM, vol. 11, pp. 22\u201328. Citeseer (2011)"},{"key":"8_CR61","unstructured":"Millen, J.: A necessarily parallel attack. In: Workshop on Formal Methods and Security Protocols. Citeseer (1999)"},{"key":"8_CR62","unstructured":"Oak, P.: Kanto regional Pok\u00e9dex. Kanto Region J. Pok\u00e9mon Res. 19 (1996)"},{"key":"8_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-319-75650-9_5","volume-title":"Foundations and Practice of Security","author":"O Pereira","year":"2018","unstructured":"Pereira, O., Rochet, F., Wiedling, C.: Formal analysis of the FIDO 1.x protocol. In: Imine, A., Fernandez, J.M., Marion, J.-Y., Logrippo, L., Garcia-Alfaro, J. (eds.) FPS 2017. LNCS, vol. 10723, pp. 68\u201382. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-75650-9_5"},{"key":"8_CR64","doi-asserted-by":"crossref","unstructured":"Protzenko, J., Beurdouche, B., Merigoux, D., Bhargavan, K.: Formally verified cryptographic web applications in WebAssembly. In: IEEE Symposium on Security and Privacy (S&P). IEEE (2019)","DOI":"10.1109\/SP.2019.00064"},{"key":"8_CR65","doi-asserted-by":"crossref","unstructured":"Protzenko, J., et al.: Verified low-level programming embedded in F. In: 2017 Proceedings of the ACM on Programming Languages (ICFP), vol. 1 (2017)","DOI":"10.1145\/3110261"},{"key":"8_CR66","doi-asserted-by":"crossref","unstructured":"Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Chong, S. (ed.) IEEE Computer Security Foundations Symposium (CSF), Cambridge, MA, USA, 25\u201327 June 2012, pp. 78\u201394. IEEE (2012)","DOI":"10.1109\/CSF.2012.25"},{"key":"8_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-540-40956-4_3","volume-title":"Privacy Enhancing Technologies","author":"S Steinbrecher","year":"2003","unstructured":"Steinbrecher, S., K\u00f6psell, S.: Modelling unlinkability. In: Dingledine, R. (ed.) PET 2003. LNCS, vol. 2760, pp. 32\u201347. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-40956-4_3"},{"key":"8_CR68","unstructured":"Tronosco, C., et al.: Decentralized privacy-preserving proximity tracing, April 2020"},{"issue":"4","key":"8_CR69","doi-asserted-by":"publisher","first-page":"2595","DOI":"10.1007\/s11277-014-1745-8","volume":"79","author":"B Woo-Sik","year":"2014","unstructured":"Woo-Sik, B.: Formal verification of an RFID authentication protocol based on hash function and secret code. Wireless Pers. Commun. 79(4), 2595\u20132609 (2014). https:\/\/doi.org\/10.1007\/s11277-014-1745-8","journal-title":"Wireless Pers. Commun."}],"container-title":["Lecture Notes in Computer Science","Progress in Cryptology \u2013 INDOCRYPT 2020"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-65277-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,3]],"date-time":"2022-12-03T00:18:17Z","timestamp":1670026697000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-65277-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030652760","9783030652777"],"references-count":69,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-65277-7_8","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":"8 December 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"INDOCRYPT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Cryptology in India","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bangalore","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"India","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 December 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 December 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"indocrypt2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/indocrypt2020.iiitb.ac.in\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"84","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":"39","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":"3","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":"46% - 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.0","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":"4.3","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)"}}]}}