{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,7]],"date-time":"2026-04-07T07:02:55Z","timestamp":1775545375622,"version":"3.50.1"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2018,3,1]],"date-time":"2018-03-01T00:00:00Z","timestamp":1519862400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2018,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Designing and coding security protocols is an error prone task. Several flaws are found in protocol implementations and specifications every year. Formal methods can alleviate this problem by backing implementations with rigorous proofs about their behavior. However, formally-based development typically requires domain specific knowledge available only to few experts and the development of abstract formal models that are far from real implementations. This paper presents a Java-based protocol design and implementation framework, where the user can write a security protocol symbolic model in Java, using a well defined subset of the language that corresponds to applied\n            <jats:italic>\u03c0<\/jats:italic>\n            -calculus. This Java model can be symbolically executed in the Java debugger, formally verified with ProVerif, and further refined to an interoperable Java implementation of the protocol. Soundness theorems are provided to prove that, under some reasonable assumptions, a simulation relation relates the Java refined implementation to the symbolic model verified by ProVerif, so that, for the usual security properties, a property verified by ProVerif on the symbolic model is preserved in the Java refined implementation. The applicability of the framework is evaluated by developing an extensive case study on the popular SSL protocol.\n          <\/jats:p>","DOI":"10.1007\/s00165-017-0449-8","type":"journal-article","created":{"date-parts":[[2017,12,12]],"date-time":"2017-12-12T12:51:12Z","timestamp":1513083072000},"page":"279-317","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formally sound implementations of security protocols with JavaSPI"],"prefix":"10.1145","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3142-2383","authenticated-orcid":false,"given":"Riccardo","family":"Sisto","sequence":"first","affiliation":[{"name":"Dipartimento di Automatica e Informatica, Politecnico di Torino, Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piergiuseppe","family":"Bettassa Copet","sequence":"additional","affiliation":[{"name":"Dipartimento di Automatica e Informatica, Politecnico di Torino, Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matteo","family":"Avalle","sequence":"additional","affiliation":[{"name":"Dipartimento di Automatica e Informatica, Politecnico di Torino, Turin, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alfredo","family":"Pironti","sequence":"additional","affiliation":[{"name":"IOActive, Madrid, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Almeida JB Bangerter E Barbosa M Krenn S Sadeghi AR Schneider T (2010) A certifying compiler for zero-knowledge proofs of knowledge based on \u03a3-protocols. In: 15th European conference on research in computer security (ESORICS 2010). Lecture notes in computer science vol 6345. Springer Berlin pp 151\u2013167","DOI":"10.1007\/978-3-642-15497-3_10"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Almeida JB Barbosa M Barthe G Dupressoir F (2013) Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. In: 2013 ACM SIGSAC conference on computer and communications security (CCS 2013) ACM pp 1217\u20131230","DOI":"10.1145\/2508859.2516652"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Avanesov T Chevalier Y Mekki MA Rusinowitch M (2012) Web services verification and prudent implementation. In: Data privacy management and autonomous spontaneus security. Lecture notes in computer science vol 7122. Springer Berlin pp 173\u2013189","DOI":"10.1007\/978-3-642-28879-1_12"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/373243.360213"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Al Fardan NJ Paterson KG (2013) Lucky thirteen: breaking the TLS and DTLS record protocols. In: 2013 IEEE symposium on security and privacy (S & P 2013) IEEE pp 526\u2013540","DOI":"10.1109\/SP.2013.42"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Aizatulin M Gordon AD J\u00fcrjens J (2012) Computational verification of C protocol implementations by symbolic execution. In: 2012 ACM conference on computer and communications security (CCS 2012) ACM pp 712\u2013723","DOI":"10.1145\/2382196.2382271"},{"key":"e_1_2_1_2_7_2","unstructured":"Apple goto fail bug (2014) CVE-2014-1266. https:\/\/web.nvd.nist.gov\/view\/vuln\/detail?vulnId=CVE-2014-1266"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.4018\/jsse.2011100103"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0269-9"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Avalle M Pironti A Sisto R Pozza D (2011) The JavaSPI framework for security protocol implementation. In: 6th international conference on availability reliability and security (ARES 2011) IEEE Computer Society pp 746\u2013751","DOI":"10.1109\/ARES.2011.117"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Albrecht MR Paterson KG Watson G (2009) Plaintext recovery attacks against ssh. In: IEEE symposium on security and privacy (S & P 2009) IEEE pp 16\u201326","DOI":"10.1109\/SP.2009.5"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Bhargavan K Corin R Deni\u00e9lou PM Fournet C Leifer JJ (2009) Cryptographic protocol synthesis and verification for multiparty sessions. In: 22nd IEEE computer security foundations symposium (CSF 2009) IEEE Computer Society pp 124\u2013140","DOI":"10.1109\/CSF.2009.26"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Bettassa Copet P Pironti A Pozza D Sisto R Vivoli P (2012) Visual model-driven design verification and implementation of security protocols. In: IEEE 14th international symposium on high-assurance systems engineering (HASE 2012) IEEE pp 62\u201365","DOI":"10.1109\/HASE.2012.23"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/1125808.1125810"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1452044.1452049"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Blanchet B (2001) An efficient cryptographic protocol verifier based on prolog rules. In: 14th IEEE workshop on computer security foundations (CSF 2001) IEEE Computer Society pp 82\u201396","DOI":"10.1109\/CSFW.2001.930138"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.5555\/1576303.1576304"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Bhargavan K Lavaud AD Fournet C Pironti A Strub PY (2014) Triple handshakes and cookie cutters: breaking and fixing authentication over TLS. In: IEEE symposium on security and privacy (S & P 2014) IEEE pp 98\u2013113","DOI":"10.1109\/SP.2014.14"},{"key":"e_1_2_1_2_19_2","unstructured":"Bierman G Parkinson M Pitts A (2003) MJ: an imperative core calculus for Java and Java with effects. Technical report 563 Cambridge University Computer Laboratory"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Cade D Blanchet B (2012) From computationally-proved protocol specifications to implementations. In: 7th international conference on availability reliability and security (ARES 2012) IEEE Computer Society pp 65\u201374","DOI":"10.1109\/ARES.2012.63"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-140508"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_2_23_2","unstructured":"GnuTLS certificate verification issue (2014) CVE-2014-0092. https:\/\/web.nvd.nist.gov\/view\/vuln\/detail?vulnId=CVE-2014-0092"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Gorrieri R Versari C (2015) Transition systems and behavioral equivalences. Springer Berlin pp 21\u201379","DOI":"10.1007\/978-3-319-21491-7_2"},{"key":"e_1_2_1_2_25_2","unstructured":"Heartbleed bug (2014) CVE-2014-0160. https:\/\/web.nvd.nist.gov\/view\/vuln\/detail?vulnId=CVE-2014-0160"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.481514"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"J\u00fcrjens J (2001) Secrecy-preserving refinement. In: Fiadeiro J Zave P (eds) International symposium on formal methods Europe (FME). Lecture notes in computer science vol 2021. Springer Berlin pp 135\u2013152","DOI":"10.1007\/3-540-45251-6_8"},{"key":"e_1_2_1_2_28_2","volume-title":"Secure systems development with UML","author":"J\u00fcrjens J","year":"2005"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Kiyomoto S Ota H Tanaka T (2008) A security protocol compiler generating C source codes. In: Information security and assurance IEEE pp 20\u201325","DOI":"10.1109\/ISA.2008.13"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Montrieux L J\u00fcrjens J Haley CB Yu Y Schobbens PY Toussaint H (2010) Tool support for code generation from a umlsec property. In: IEEE\/ACM international conference on automated software engineering (ASE 2010) ACM pp 357\u2013358","DOI":"10.1145\/1858996.1859074"},{"key":"e_1_2_1_2_31_2","unstructured":"O\u2019Shea N (2008) Using elyjah to analyse Java implementations of cryptographic protocols. In: Joint workshop on foundations of computer security automated reasoning for security protocol analysis and issues in the theory of security pp 221\u2013226"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Pironti A Sisto R (2007) An experiment in interoperable cryptographic protocol implementation using automatic code generation. In IEEE Symposium on computers and communications pages 839\u2013844. IEEE","DOI":"10.1109\/ISCC.2007.4381508"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0267-y"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Rescorla E Ray M Dispensa S Oskov N (2010) Transport layer security (TLS) renegotiation indication extension. RFC 5746","DOI":"10.17487\/rfc5746"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Song DX Perrig A Phan D (2001) AGVI: automatic generation verification and implementation of security protocols. In: 13th international conference on computer aided verification (CAV 2001). Lecture notes in computer science vol 2102. Springer Berlin pp 241\u2013245","DOI":"10.1007\/3-540-44585-4_21"},{"key":"e_1_2_1_2_36_2","unstructured":"The Legion of Bouncy Castle. Bouncy castle crypto API. https:\/\/www.bouncycastle.org\/java.html"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0449-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0449-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0449-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0449-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:54:56Z","timestamp":1641538496000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0449-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,3]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,3]]}},"alternative-id":["10.1007\/s00165-017-0449-8"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0449-8","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,3]]}}}