{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T15:46:37Z","timestamp":1781106397069,"version":"3.54.1"},"reference-count":13,"publisher":"IGI Global Scientific Publishing","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,10]]},"abstract":"<jats:p>This paper presents JavaSPI, a \u201cmodel-driven\u201d development framework that allows the user to reliably develop security protocol implementations in Java, starting from abstract models that can be verified formally. The main novelty of this approach stands in the use of Java as both a modeling language and the implementation language. The JavaSPI framework is validated by implementing a scenario of the SSL protocol. The JavaSPI implementation can successfully interoperate with OpenSSL, and has comparable execution time with the standard Java JSSE library.<\/jats:p>","DOI":"10.4018\/jsse.2011100103","type":"journal-article","created":{"date-parts":[[2011,11,16]],"date-time":"2011-11-16T07:47:28Z","timestamp":1321429648000},"page":"34-48","source":"Crossref","is-referenced-by-count":13,"title":["JavaSPI"],"prefix":"10.4018","volume":"2","author":[{"given":"Matteo","family":"Avalle","sequence":"first","affiliation":[{"name":"Politecnico di Torino, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alfredo","family":"Pironti","sequence":"additional","affiliation":[{"name":"INRIA, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Davide","family":"Pozza","sequence":"additional","affiliation":[{"name":"Teoresi Group, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Riccardo","family":"Sisto","sequence":"additional","affiliation":[{"name":"Politecnico di Torino, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"2432","reference":[{"key":"jsse.2011100103-0","unstructured":"Almeida, J., Bangerter, E., Barbosa, M., Krenn, S., Sadeghi, A., & Schneider, T. (2010). A certifying compiler for zero-knowledge proofs of knowledge based on sigma-protocols. In Proceedings of the European Symposium on Research in Computer Security (pp. 151-167)."},{"key":"jsse.2011100103-1","doi-asserted-by":"crossref","unstructured":"Backes, M., Maffei, M., & Unruh, D. (2010). Computationally sound verification of source code. In Proceedings of the 17th ACM Conference on Computer and Communications Security (pp. 387-398).","DOI":"10.1145\/1866307.1866351"},{"key":"jsse.2011100103-2","doi-asserted-by":"crossref","unstructured":"Balser, M., Reif, W., Schellhorn, G., Stenzel, K., & Thums, A. (2000). Formal system development with KIV. In Proceedings of the 3rd International Conference on Fundamental Approaches to Software Engineering: Held as Part of the European Joint Conferences on the Theory and Practice of Software (pp. 363-366).","DOI":"10.1007\/3-540-46428-X_25"},{"key":"jsse.2011100103-3","doi-asserted-by":"publisher","DOI":"10.1145\/1125808.1125810"},{"key":"jsse.2011100103-4","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Corin, R., Deni\u00e9lou, P., Fournet, C., & Leifer, J. (2009). Cryptographic protocol synthesis and verification for multiparty sessions. In Proceedings of the Computer Security Foundations Symposium (pp. 124-140).","DOI":"10.1109\/CSF.2009.26"},{"key":"jsse.2011100103-5","doi-asserted-by":"publisher","DOI":"10.1145\/1452044.1452049"},{"issue":"4","key":"jsse.2011100103-6","doi-asserted-by":"crossref","first-page":"363","DOI":"10.3233\/JCS-2009-0339","article-title":"Automatic verification of correspondences for security protocols.","volume":"17","author":"B.Blanchet","year":"2009","journal-title":"Journal of Computer Security"},{"key":"jsse.2011100103-7","doi-asserted-by":"crossref","unstructured":"Chaki, S., & Datta, A. (2009). ASPIER: An automated framework for verifying security protocol implementations. In Proceedings of the Computer Security Foundations Symposium (pp. 172-185).","DOI":"10.1109\/CSF.2009.20"},{"key":"jsse.2011100103-8","author":"J.J\u00fcrjens","year":"2005","journal-title":"Secure systems development with UML"},{"key":"jsse.2011100103-9","doi-asserted-by":"crossref","unstructured":"Kiyomoto, S., Ota, H., & Tanaka, T. (2008). A security protocol compiler generating C source codes. In Proceedings of the International Conference on Information Security and Assurance (pp. 20-25).","DOI":"10.1109\/ISA.2008.13"},{"key":"jsse.2011100103-10","unstructured":"O'Shea, N. (2008). Using Elyjah to analyse Java implementations of cryptographic protocols. In Proceedings of the Conference on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (pp. 221-226)."},{"key":"jsse.2011100103-11","doi-asserted-by":"crossref","unstructured":"Pironti, A., & Sisto, R. (2007). An experiment in interoperable cryptographic protocol implementation using automatic code generation. In Proceedings of the IEEE Symposium on Computers and Communications (pp. 839-844).","DOI":"10.1109\/ISCC.2007.4381508"},{"key":"jsse.2011100103-12","doi-asserted-by":"crossref","unstructured":"Song, D. X., Perrig, A., & Phan, D. (2001). AGVI - Automatic generation, verification, and implementation of security protocols. In Proceedings of the 13th International Conference on Computer Aided Verification (pp. 241-245).","DOI":"10.1007\/3-540-44585-4_21"}],"container-title":["International Journal of Secure Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=61152","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,19]],"date-time":"2019-02-19T11:33:11Z","timestamp":1550575991000},"score":1,"resource":{"primary":{"URL":"http:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/jsse.2011100103"}},"subtitle":["A Framework for Security Protocol Implementation"],"short-title":[],"issued":{"date-parts":[[2011,10]]},"references-count":13,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.4018\/jsse.2011100103","relation":{},"ISSN":["1947-3036","1947-3044"],"issn-type":[{"value":"1947-3036","type":"print"},{"value":"1947-3044","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,10]]}}}