{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:38Z","timestamp":1781238938687,"version":"3.54.1"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319961415","type":"print"},{"value":"9783319961422","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96142-2_26","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T15:55:08Z","timestamp":1532102108000},"page":"430-446","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":44,"title":["Continuous Formal Verification of Amazon s2n"],"prefix":"10.1007","author":[{"given":"Andrey","family":"Chudnov","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nathan","family":"Collins","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Byron","family":"Cook","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joey","family":"Dodds","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Brian","family":"Huffman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Colm","family":"MacC\u00e1rthaigh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stephen","family":"Magill","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eric","family":"Mertens","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eric","family":"Mullen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Serdar","family":"Tasiran","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aaron","family":"Tomb","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Eddy","family":"Westbrook","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., Barbosa, M., Barthe, G., Blot, A., Gr\u00e9goire, B., Laporte, V., Oliveira, T., Pacheco, H., Schmidt, B., Strub, P.: Jasmin: high-assurance and high-speed cryptography. In: Thuraisingham, B.M., Evans, D., Malkin, T., Xu, D. (eds.), Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, 30 October\u2013 03 November 2017, pp. 1807\u20131823. ACM (2017)","DOI":"10.1145\/3133956.3134078"},{"key":"26_CR2","unstructured":"Amazon.com, Inc., Amazon Simple Storage Service (s3). https:\/\/aws.amazon.com\/s3\/"},{"key":"26_CR3","unstructured":"Amazon.com, Inc. s2n. https:\/\/github.com\/awslabs\/s2n . Accessed Dec 2017"},{"key":"26_CR4","unstructured":"awslabs\/s2n - Travis CI. https:\/\/travis-ci.org\/awslabs\/s2n"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-642-54792-8_13","volume-title":"Principles of Security and Trust","author":"M Barbosa","year":"2014","unstructured":"Barbosa, M., Castro, D., Silva, P.F.: Compiling CAO: from cryptographic specifications to C implementations. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 240\u2013244. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_13"},{"key":"26_CR6","unstructured":"Beringer, L., Petcher, A., Katherine, Q.Y., Appel, A.W.: Verified correctness and security of OpenSSL HMAC. In: USENIX Security Symposium, pp. 207\u2013221 (2015)"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Beurdouche, B., Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.-Y., Zinzindohoue, J.K.: A messy state of the union: taming the composite state machines of TLS. In: 2015 IEEE Symposium on Security and Privacy (SP), pp. 535\u2013552. IEEE (2015)","DOI":"10.1109\/SP.2015.39"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.: Implementing TLS with verified cryptographic security, pp. 445\u2013459. IEEE, May 2013","DOI":"10.1109\/SP.2013.37"},{"key":"26_CR9","unstructured":"Bhargavan, K., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.-Y., Zanella-B\u00e8guelin, S.: Proving the TLS handshake secure (as it is). Cryptology ePrint Archive, Report 2014\/182 (2014). https:\/\/eprint.iacr.org\/2014\/182"},{"key":"26_CR10","unstructured":"Chudnov, A.: Missing branches in the handshake state machine, July 2017. https:\/\/github.com\/awslabs\/s2n\/pull\/551"},{"key":"26_CR11","unstructured":"de Ruiter, J., Poll, E.: Protocol state fuzzing of TLS implementations. In: 24th USENIX Security Symposium (USENIX Security 15), pp. 193\u2013206. USENIX Association, Washington, D.C. (2015)"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Delignat-Lavaud, A., Fournet, C., Kohlweiss, M., Protzenko, J., Rastogi, A., Swamy, N., Zanella-B\u00e9guelin, S., Bhargavan, K., Pan, J., Zinzindohou\u00e9, J.K.: Implementing and proving the TLS 1.3 record layer. In: 2017 IEEE Symposium on Security and Privacy (SP), pp. 463\u2013482. IEEE (2017)","DOI":"10.1109\/SP.2017.58"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Eastlake III, D.: Transport Layer Security (TLS) Extensions: Extension Definitions. RFC 6066, January 2011","DOI":"10.17487\/rfc6066"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Erk\u00f6k, L., Matthews, J.: Pragmatic equivalence and safety checking in Cryptol, p. 73. ACM Press (2008)","DOI":"10.1145\/1481848.1481860"},{"key":"26_CR15","unstructured":"Eronen, P., Tschofenig, H., Zhou, H., Salowey, J.A.: Transport Layer Security (TLS) Session Resumption without Server-Side State. RFC 5077, January 2008"},{"key":"26_CR16","unstructured":"Galois, Inc.: The software analysis workbench. https:\/\/saw.galois.com\/index.html"},{"key":"26_CR17","unstructured":"Gorelli, M.: Deductive verification of the s2n HMAC code. Master\u2019s thesis, Universtity of Oxford (2016)"},{"key":"26_CR18","unstructured":"Kaloper-Mer\u0161injak, D., Mehnert, H., Madhavapeddy, A., Sewell, P.: Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation. In: 24th USENIX Security Symposium (USENIX Security 2015), pp. 223\u2013238. USENIX Association, Washington, D.C. (2015)"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.: Continuous reasoning: scaling the impact of formal methods. In: Logic in Computer Science (LICS). (2018)","DOI":"10.1145\/3209108.3209109"},{"key":"26_CR20","unstructured":"Petcher, A., Morrisett, G.: The foundational cryptography framework. arXiv:1410.3735 [cs], October 2014. arXiv:1410.3735"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Rescorla, E., Dierks, T.: The Transport Layer Security (TLS) Protocol Version 1.2. RFC 5246, August 2008","DOI":"10.17487\/rfc5246"},{"key":"26_CR22","unstructured":"The Coq Development Team. The Coq proof assistant, version 8.7.1, December 2017"},{"key":"26_CR23","unstructured":"Trustinsoft. PolarSSL verification kit. https:\/\/trust-in-soft.com\/polarssl-verification-kit\/"},{"key":"26_CR24","unstructured":"Turner, J.M.: The keyed-Hash Message Authentication Code (HMAC). Federal Information Processing Standards Publication (2008)"},{"key":"26_CR25","doi-asserted-by":"crossref","unstructured":"Zinzindohou\u00e9, J.-K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: a verified modern cryptographic library. In: ACM Conference on Computer and Communications Security (CCS) (2017)","DOI":"10.1145\/3133956.3134043"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96142-2_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T23:21:00Z","timestamp":1571613660000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96142-2_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961415","9783319961422"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96142-2_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}