{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T17:35:08Z","timestamp":1785605708836,"version":"3.56.0"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031664557","type":"print"},{"value":"9783031664564","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,29]],"date-time":"2024-09-29T00:00:00Z","timestamp":1727568000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,9,29]],"date-time":"2024-09-29T00:00:00Z","timestamp":1727568000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-66456-4_19","type":"book-chapter","created":{"date-parts":[[2024,9,28]],"date-time":"2024-09-28T06:01:58Z","timestamp":1727503318000},"page":"346-366","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formal Verification Techniques for\u00a0Post-quantum Cryptography: A Systematic Review"],"prefix":"10.1007","author":[{"given":"Yuexi","family":"Xu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhenyuan","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Naipeng","family":"Dong","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Veronika","family":"Kuchta","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhe","family":"Hou","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dongxi","family":"Liu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,9,29]]},"reference":[{"key":"19_CR1","unstructured":"Proverif. https:\/\/bblanche.gitlabpages.inria.fr\/proverif\/"},{"key":"19_CR2","unstructured":"The squirrel prover. https:\/\/github.com\/squirrel-prover\/squirrel-prover\/"},{"key":"19_CR3","unstructured":"Tamarin prover. https:\/\/tamarin-prover.com\/"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Abinaya, M., Prabakeran, S.: Lightweight block cipher for resource constrained IoT environment-an survey, performance, cryptanalysis and research challenges. In: ICICNIS, pp. 347\u2013365 (2022)","DOI":"10.1007\/978-981-19-5845-8_25"},{"key":"19_CR5","unstructured":"Abohashima, Z., Elhosen, M., Houssein, E.H., Mohamed, W.M.: Classification with quantum machine learning: a survey. arXiv preprint arXiv:2006.12270 (2020)"},{"key":"19_CR6","unstructured":"Alnahawi, N., M\u00fcller, J., Oupick\u00fd, J., Wiesmaier, A.: SoK: post-quantum TLS Handshake. Cryptology ePrint Archive (2023)"},{"key":"19_CR7","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/s00165-012-0269-9","volume":"26","author":"M Avalle","year":"2014","unstructured":"Avalle, M., Pironti, A., Sisto, R.: Formal verification of security protocol implementations: a survey. Formal Aspects Comput. 26, 99\u2013123 (2014)","journal-title":"Formal Aspects Comput."},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Baelde, D., Delaune, S., Jacomme, C., Koutsos, A., Moreau, S.: An interactive prover for protocol verification in the computational model. In: S &P (2021)","DOI":"10.1109\/SP40001.2021.00078"},{"key":"19_CR9","unstructured":"Bagane, P.A., Kotrappa, S.: Bibliometric survey for cryptanalysis of block ciphers towards cyber security. Library Philosophy and Practice, pp. 1\u201318 (2020)"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Bana, G., Comon-Lundh, H.: A computationally complete symbolic attacker for equivalence properties. In: CCS, pp. 609\u2013620 (2014)","DOI":"10.1145\/2660267.2660276"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Barbosa, M., et al.: SOK: computer-aided cryptography. In: S &P (2021)","DOI":"10.1109\/SP40001.2021.00008"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Barbosa, M., et al.: EasyPQC: verifying post-quantum cryptography. In: CCS, pp. 2564\u20132586 (2021)","DOI":"10.1145\/3460120.3484567"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Barthe, G., Daubignard, M., Kapron, B., Lakhnech, Y.: Computational indistinguishability logic. In: CCS, pp. 375\u2013386 (2010)","DOI":"10.1145\/1866307.1866350"},{"key":"19_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Barthe, G., Fan, X., Gancher, J., Gr\u00e9goire, B., Jacomme, C., Shi, E.: Symbolic proofs for lattice-based cryptography. In: CCS, pp. 538\u2013555 (2018)","DOI":"10.1145\/3243734.3243825"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Annual Cryptology Conference (2011)","DOI":"10.1007\/978-3-642-22792-9_5"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Lakhnech, Y., Zanella\u00a0B\u00e9guelin, S.: Beyond provable security verifiable IND-CCA security of OAEP. In: Cryptographers\u2019 Track at the RSA Conference, pp. 180\u2013196 (2011)","DOI":"10.1007\/978-3-642-19074-2_13"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella\u00a0B\u00e9guelin, S.: Formal certification of code-based cryptographic proofs. In: POPL, pp. 90\u2013101 (2009)","DOI":"10.1145\/1480881.1480894"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Barthe, G., Hedin, D., B\u00e9guelin, S.Z., Gr\u00e9goire, B., Heraud, S.: A machine-checked formalization of sigma-protocols. In: CSF, pp. 246\u2013260 (2010)","DOI":"10.1109\/CSF.2010.24"},{"key":"19_CR20","unstructured":"Bellare, M., Rogaway, P.: Code-based game-playing proofs and the security of triple encryption. Cryptology ePrint Archive, Paper 2004\/331 (2004)"},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"Bellare, M., Rogaway, P.: The security of triple encryption and a framework for code-based game-playing proofs. In: EUROCRYPT 2006, pp. 409\u2013426 (2006)","DOI":"10.1007\/11761679_25"},{"key":"19_CR22","unstructured":"Blanchet, B.: CryptoVerif: a computationally-sound security protocol verifier. Technical Report (2017)"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Boneh, D., Dagdelen, \u00d6., Fischlin, M., Lehmann, A., Schaffner, C., Zhandry, M.: Random oracles in a quantum world. In: ASIACRYPT, pp. 41\u201369 (2011)","DOI":"10.1007\/978-3-642-25385-0_3"},{"key":"19_CR24","unstructured":"Chareton, C., Bardin, S., Lee, D., Valiron, B., Vilmart, R., Xu, Z.: Formal methods for quantum programs: a survey. arXiv preprint arXiv:2109.06493 (2021)"},{"key":"19_CR25","unstructured":"Ciulei, A.T., Cre\u021bu, M.C., Simion, E.: Preparation for post-quantum era: a survey about blockchain schemes from a post-quantum perspective. Cryptology ePrint Archive (2022)"},{"key":"19_CR26","unstructured":"Corin, R., den Hartog, J.: A probabilistic hoare-style logic for game-based cryptographic proofs (extended version). Cryptology ePrint Archive, Paper 2005\/467 (2005). https:\/\/eprint.iacr.org\/2005\/467"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Courant, J., Daubignard, M., Ene, C., Lafourcade, P., Lakhnech, Y.: Towards automated proofs for asymmetric encryption schemes in the random oracle model. In: CCS, pp. 371\u2013380 (2008)","DOI":"10.1145\/1455770.1455817"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Cremers, C., Fontaine, C., Jacomme, C.: A logic and an interactive prover for the computational post-quantum security of protocols. In: S &P, pp. 125\u2013141 (2022)","DOI":"10.1109\/SP46214.2022.9833800"},{"issue":"2","key":"19_CR29","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":"19_CR30","doi-asserted-by":"publisher","first-page":"21091","DOI":"10.1109\/ACCESS.2020.2968985","volume":"8","author":"TM Fernandez-Carames","year":"2020","unstructured":"Fernandez-Carames, T.M., Fraga-Lamas, P.: Towards post-quantum blockchain: a review on blockchain cryptography resistant to quantum computing attacks. IEEE Access 8, 21091\u201321116 (2020)","journal-title":"IEEE Access"},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"Gagn\u00e9, M., Lafourcade, P., Lakhnech, Y.: Automated security proofs for almost-universal hash for MAC verification. In: ESORICS, vol.\u00a08134, pp. 291\u2013308 (2013)","DOI":"10.1007\/978-3-642-40203-6_17"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Gagn\u00e9, M., Lafourcade, P., Lakhnech, Y., Safavi-Naini, R.: Automated security proof for symmetric encryption modes. In: Annual Asian Computing Science Conference, vol.\u00a05913, pp. 39\u201353 (2009)","DOI":"10.1007\/978-3-642-10622-4_4"},{"key":"19_CR33","first-page":"181","volume":"2005","author":"S Halevi","year":"2005","unstructured":"Halevi, S.: A plausible approach to computer-aided cryptographic proofs. IACR Cryptol. ePrint Arch. 2005, 181 (2005)","journal-title":"IACR Cryptol. ePrint Arch."},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Hasija, T., Ramkumar, K., Kaur, A., Mittal, S., Singh, B.: A survey on NIST selected third round candidates for post quantum cryptography. In: ICCES (2022)","DOI":"10.1109\/ICCES54183.2022.9835864"},{"key":"19_CR35","unstructured":"Herman, D., et al.: A survey of quantum computing for finance. arXiv:2201.02773 (2022)"},{"key":"19_CR36","unstructured":"Hoang, V.T., Katz, J., Malozemoff, A.J.: Automated analysis and synthesis of authenticated encryption schemes. IACR Cryptol. ePrint Arch, p.\u00a0624 (2015). http:\/\/eprint.iacr.org\/2015\/624"},{"key":"19_CR37","doi-asserted-by":"publisher","first-page":"107233","DOI":"10.1016\/j.comnet.2020.107233","volume":"174","author":"K Hofer-Schmitz","year":"2020","unstructured":"Hofer-Schmitz, K., Stojanovi\u0107, B.: Towards formal verification of IoT protocols: a review. Comput. Netw. 174, 107233 (2020)","journal-title":"Comput. Netw."},{"key":"19_CR38","unstructured":"Kfoury, A.: Hoare logic and variations: probabilistic, relational, probabilistic+ relational (2018). https:\/\/www.cs.bu.edu\/faculty\/kfoury\/UNI-Teaching\/CS512\/AK_Documents\/Hoare_Logic\/main-post.pdf"},{"key":"19_CR39","doi-asserted-by":"crossref","unstructured":"Kumari, S., Singh, M., Singh, R., Tewari, H.: Post-quantum cryptography techniques for secure communication in resource-constrained internet of things devices: a comprehensive survey. Softw. Pract. Experience 52(10), 2047\u20132076 (2022)","DOI":"10.1002\/spe.3121"},{"key":"19_CR40","doi-asserted-by":"publisher","first-page":"77894","DOI":"10.1109\/ACCESS.2019.2921624","volume":"7","author":"J Liu","year":"2019","unstructured":"Liu, J., Liu, Z.: A survey on security verification of blockchain smart contracts. IEEE Access 7, 77894\u201377904 (2019)","journal-title":"IEEE Access"},{"key":"19_CR41","doi-asserted-by":"crossref","unstructured":"Malozemoff, A.J., Katz, J., Green, M.D.: Automated analysis and synthesis of block-cipher modes of operation. IACR Cryptol. ePrint Arch, p.\u00a0774 (2014)","DOI":"10.1109\/CSF.2014.18"},{"key":"19_CR42","unstructured":"Mnkash, S.H.: Survey of different cryptography methods. Resmilitaris 12(2), 495\u2013516 (2022)"},{"key":"19_CR43","unstructured":"NIST: Round 4 submissions - post-quantum cryptography: CSRC. https:\/\/csrc.nist.gov\/Projects\/post-quantum-cryptography\/round-4-submissions. Accessed 20 Oct 2023"},{"key":"19_CR44","unstructured":"NIST: selected algorithms 2022 - post-quantum cryptography: CSRC. https:\/\/csrc.nist.gov\/Projects\/post-quantum-cryptography\/selected-algorithms-2022. Accessed 20 Oct 2023"},{"key":"19_CR45","doi-asserted-by":"crossref","unstructured":"Parida, N.K., Jatoth, C., Reddy, V.D., Hussain, M.M., Faizi, J.: Post-quantum distributed ledger technology: a systematic survey. Sci. Rep. 13(1), 20729 (2023)","DOI":"10.1038\/s41598-023-47331-1"},{"key":"19_CR46","doi-asserted-by":"crossref","unstructured":"Ramezani, S.B., Sommers, A., Manchukonda, H.K., Rahimi, S., Amirlatifi, A.: Machine learning algorithms in quantum computing: a survey. In: IJCNN (2020)","DOI":"10.1109\/IJCNN48605.2020.9207714"},{"key":"19_CR47","unstructured":"Shannon, K., Towe, E., Tonguz, O.K.: On the use of quantum entanglement in secure communications: a survey. arXiv preprint arXiv:2003.07907 (2020)"},{"issue":"1","key":"19_CR48","doi-asserted-by":"publisher","first-page":"577","DOI":"10.1109\/COMST.2015.2459691","volume":"18","author":"KA Shim","year":"2015","unstructured":"Shim, K.A.: A survey of public-key cryptographic primitives in wireless sensor networks. IEEE Commun. Surv. Tutorials 18(1), 577\u2013601 (2015)","journal-title":"IEEE Commun. Surv. Tutorials"},{"key":"19_CR49","unstructured":"Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. IACR Cryptol. ePrint Arch, p.\u00a0332 (2004)"},{"key":"19_CR50","unstructured":"Sieber, K.: The foundations of program verification (2013)"},{"key":"19_CR51","doi-asserted-by":"crossref","unstructured":"Song, F.: A note on quantum security for post-quantum cryptography. In: Post-Quantum Cryptography, pp. 246\u2013265 (2014)","DOI":"10.1007\/978-3-319-11659-4_15"},{"key":"19_CR52","doi-asserted-by":"crossref","unstructured":"Sosnowski, M., et al.: The performance of post-quantum TLS 1.3. In: CoNEXT (2023)","DOI":"10.1145\/3624354.3630585"},{"issue":"4","key":"19_CR53","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1007\/s10207-022-00587-6","volume":"21","author":"TG Tan","year":"2022","unstructured":"Tan, T.G., Szalachowski, P., Zhou, J.: Challenges of post-quantum digital signing in real-world applications: a survey. Int. J. Inf. Secur. 21(4), 937\u2013952 (2022)","journal-title":"Int. J. Inf. Secur."},{"issue":"2","key":"19_CR54","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1049\/ise2.12101","volume":"17","author":"A Wang","year":"2023","unstructured":"Wang, A., Xiao, D., Yu, Y.: Lattice-based cryptosystems in standardisation processes: a survey. IET Inf. Secur. 17(2), 227\u2013243 (2023)","journal-title":"IET Inf. Secur."},{"key":"19_CR55","doi-asserted-by":"crossref","unstructured":"Zanella-B\u00e9guelin, S., Barthe, G., Gr\u00e9goire, B., Olmedo, F.: Formally certifying the security of digital signature schemes. In: S &P, pp. 237\u2013250 (2009)","DOI":"10.1109\/SP.2009.17"},{"key":"19_CR56","doi-asserted-by":"crossref","unstructured":"Zeydan, E., Turk, Y., Aksoy, B., Ozturk, S.B.: Recent advances in post-quantum cryptography for networks: a survey. In: MobiSecServ, pp.\u00a01\u20138 (2022)","DOI":"10.1109\/MobiSecServ50855.2022.9727214"}],"container-title":["Lecture Notes in Computer Science","Engineering of Complex Computer Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66456-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,5]],"date-time":"2025-04-05T17:30:11Z","timestamp":1743874211000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66456-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,29]]},"ISBN":["9783031664557","9783031664564"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66456-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,29]]},"assertion":[{"value":"29 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICECCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Engineering of Complex Computer Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Limassol","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cyprus","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"iceccs2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cyprusconferences.org\/iceccs2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}