{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T17:42:20Z","timestamp":1743010940839,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031150760"},{"type":"electronic","value":"9783031150777"}],"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-15077-7_6","type":"book-chapter","created":{"date-parts":[[2022,8,22]],"date-time":"2022-08-22T05:02:57Z","timestamp":1661144577000},"page":"97-113","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Verifying the\u00a0SHA-3 Implementation from\u00a0OpenSSL with\u00a0the\u00a0Software Analysis Workbench"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0893-0096","authenticated-orcid":false,"given":"Parker","family":"Hanson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Winters","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2264-2958","authenticated-orcid":false,"given":"Eric","family":"Mercer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brett","family":"Decker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,23]]},"reference":[{"key":"6_CR1","doi-asserted-by":"publisher","unstructured":"Almeida, J.B., et al.: Machine-checked proofs for cryptographic standards: indifferentiability of sponge and secure high-assurance implementations of SHA-3. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, pp. 1607\u20131622. Association for Computing Machinery, New York (2019). https:\/\/doi.org\/10.1145\/3319535.3363211","DOI":"10.1145\/3319535.3363211"},{"key":"6_CR2","doi-asserted-by":"publisher","unstructured":"Barthe, G., et al.: High-assurance cryptography in the spectre era. In: 2021 IEEE Symposium on Security and Privacy (SP), pp. 1884\u20131901 (2021). https:\/\/doi.org\/10.1109\/SP40001.2021.00046","DOI":"10.1109\/SP40001.2021.00046"},{"key":"6_CR3","unstructured":"Beringer, L., Petcher, A., Ye, K.Q., Appel, A.W.: Verified correctness and security of OpenSSL HMAC. In: 24th USENIX Security Symposium (USENIX Security 15), pp. 207\u2013221. USENIX Association, Washington, D.C., August 2015. https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/beringer"},{"key":"6_CR4","unstructured":"Bond, B., et al.: Vale: verifying high-performance cryptographic assembly code. In: 26th USENIX Security Symposium (USENIX Security 2017), pp. 917\u2013934. USENIX Association, Vancouver, August 2017. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/bond"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Browning, S., Weaver, P.: Designing tunable, verifiable cryptographic hardware using Cryptol. In: Hardin, D. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 89\u2013143. Springer, Boston (2010). https:\/\/doi.org\/10.1007\/978-1-4419-1539-9_4","DOI":"10.1007\/978-1-4419-1539-9_4"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-319-96142-2_26","volume-title":"Computer Aided Verification","author":"A Chudnov","year":"2018","unstructured":"Chudnov, A., et al.: Continuous formal verification of Amazon s2n. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 430\u2013446. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_26"},{"key":"6_CR7","unstructured":"The Coq proof assistant. https:\/\/coq.inria.fr\/"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-030-76384-8_5","volume-title":"NASA Formal Methods","author":"B Decker","year":"2021","unstructured":"Decker, B., Winters, B., Mercer, E.: Towards verifying SHA256 in OpenSSL with the software analysis workbench. In: Dutle, A., Moscato, M.M., Titolo, L., Mu\u00f1oz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 72\u201378. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_5"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-319-48869-1_5","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"R Dockins","year":"2016","unstructured":"Dockins, R., Foltzer, A., Hendrix, J., Huffman, B., McNamee, D., Tomb, A.: Constructing semantic models of programs with the software analysis workbench. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 56\u201372. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_5"},{"key":"6_CR10","unstructured":"Easycrypt: Computer-aided cryptographic proofs. https:\/\/github.com\/EasyCrypt\/easycrypt"},{"key":"6_CR11","doi-asserted-by":"publisher","unstructured":"Erk\u00f6k, L., Carlsson, M., Wick, A.: Hardware\/software co-verification of cryptographic algorithms using Cryptol. In: 2009 Formal Methods in Computer-Aided Design, pp. 188\u2013191 (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351121","DOI":"10.1109\/FMCAD.2009.5351121"},{"key":"6_CR12","unstructured":"SHA-3 standard: permutation-based hash and extendable-output functions (2015). https:\/\/csrc.nist.gov\/publications\/detail\/fips\/202\/final. Accessed Jan 2020"},{"key":"6_CR13","unstructured":"F* programming language. https:\/\/www.fstar-lang.org\/"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer Aided Verification","author":"V Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519\u2013531. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_52"},{"key":"6_CR15","unstructured":"Isabelle. https:\/\/isabelle.in.tum.de\/"},{"key":"6_CR16","unstructured":"Jasmin. https:\/\/github.com\/jasmin-lang\/jasmin"},{"key":"6_CR17","doi-asserted-by":"publisher","unstructured":"Klenze, T., Sprenger, C., Basin, D.: Formal verification of secure forwarding protocols. In: 2021 IEEE 34th Computer Security Foundations Symposium (CSF), pp. 1\u201316 (2021). https:\/\/doi.org\/10.1109\/CSF51468.2021.00018","DOI":"10.1109\/CSF51468.2021.00018"},{"key":"6_CR18","doi-asserted-by":"publisher","unstructured":"Lewis, J., Martin, B.: Cryptol: high assurance, retargetable crypto development and validation. In: IEEE Military Communications Conference 2003, MILCOM 2003, vol. 2, pp. 820\u2013825 (2003). https:\/\/doi.org\/10.1109\/MILCOM.2003.1290218","DOI":"10.1109\/MILCOM.2003.1290218"},{"key":"6_CR19","unstructured":"Apache log4j vulnerability guidance. https:\/\/www.cisa.gov\/uscert\/apache-log4j-vulnerability-guidance"},{"key":"6_CR20","unstructured":"OpenSSL. https:\/\/openssl.org"},{"key":"6_CR21","doi-asserted-by":"publisher","unstructured":"Protzenko, J., et al.: Evercrypt: a fast, verified, cross-platform cryptographic provider. In: 2020 IEEE Symposium on Security and Privacy (SP), pp. 983\u20131002 (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00114","DOI":"10.1109\/SP40000.2020.00114"},{"key":"6_CR22","unstructured":"RHash. https:\/\/github.com\/rhash\/RHash"},{"key":"6_CR23","unstructured":"Verifying s2n HMAC with SAW. https:\/\/galois.com\/blog\/2016\/09\/verifying-s2n-hmac-with-saw\/"},{"key":"6_CR24","doi-asserted-by":"publisher","unstructured":"Selvakumar, D., Mervin, J., Pattanshetty, S., Vivian, D.: Formal verification and analysis of a pseudo random number generator. In: 2021 25th International Symposium on VLSI Design and Test (VDAT), pp. 1\u20136 (2021). https:\/\/doi.org\/10.1109\/VDAT53777.2021.9601109","DOI":"10.1109\/VDAT53777.2021.9601109"},{"key":"6_CR25","unstructured":"SHA-3 verification. https:\/\/github.com\/ericmercer\/sha3-verification"},{"key":"6_CR26","doi-asserted-by":"publisher","unstructured":"Smith, E., Dill, D.L.: Automatic formal verification of block cipher implementations. In: 2008 Formal Methods in Computer-Aided Design, pp. 1\u20137 (2008). https:\/\/doi.org\/10.1109\/FMCAD.2008.ECP.10","DOI":"10.1109\/FMCAD.2008.ECP.10"},{"key":"6_CR27","doi-asserted-by":"publisher","first-page":"7816","DOI":"10.1109\/ACCESS.2017.2697918","volume":"5","author":"D Wang","year":"2017","unstructured":"Wang, D., Jiang, Y., Song, H., He, F., Gu, M., Sun, J.: Verification of implementations of cryptographic hash functions. IEEE Access 5, 7816\u20137825 (2017). https:\/\/doi.org\/10.1109\/ACCESS.2017.2697918","journal-title":"IEEE Access"},{"key":"6_CR28","doi-asserted-by":"publisher","unstructured":"Ye, K.Q., Green, M., Sanguansin, N., Beringer, L., Petcher, A., Appel, A.W.: Verified correctness and security of MbedTLS HMAC-DRBG. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, pp. 2007\u20132020. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3133956.3133974","DOI":"10.1145\/3133956.3133974"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-15077-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,2]],"date-time":"2022-12-02T15:16:15Z","timestamp":1669994175000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-15077-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031150760","9783031150777"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-15077-7_6","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":"23 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 May 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 May 2022","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":"spin2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin2022chi.web.illinois.edu\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}