{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T10:25:22Z","timestamp":1725791122377},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642547911"},{"type":"electronic","value":"9783642547928"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54792-8_12","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T09:35:12Z","timestamp":1395394512000},"page":"220-239","source":"Crossref","is-referenced-by-count":8,"title":["Extending and Applying a Framework for the Cryptographic Verification of Java Programs"],"prefix":"10.1007","author":[{"given":"Ralf","family":"K\u00fcsters","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Scapin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tomasz","family":"Truderung","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00fcrgen","family":"Graf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Aizatulin, M., Gordon, A.D., J\u00fcrjens, J.: Extracting and verifying cryptographic models from C protocol code by symbolic execution. In: Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS 2011). ACM (2011)","DOI":"10.1145\/2046707.2046745"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Aizatulin, M., Gordon, A.D., J\u00fcrjens, J.: Computational verification of C protocol implementations by symbolic execution. In: ACM Conference on Computer and Communications Security (CCS 2012). ACM (2012)","DOI":"10.1145\/2382196.2382271"},{"key":"12_CR3","unstructured":"Asokan, N., Niemi, V., Laitinen, P.: On the Usefulness of Proof-of-Possession. In: Proceedings of the 2nd Annual PKI Research Workshop (2003)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/BFb0055718","volume-title":"Advances in Cryptology - CRYPTO \u201998","author":"M. Bellare","year":"1998","unstructured":"Bellare, M., Desai, A., Pointcheval, D., Rogaway, P.: Relations among Notions of Security for Public-Key Encryption Schemes. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol.\u00a01462, pp. 26\u201345. Springer, Heidelberg (1998)"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.D.: Modular verification of security protocol code by typing. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010). ACM (2010)","DOI":"10.1145\/1706299.1706350"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Kohlweiss, M., Pironti, A., Strub, P.-Y.: Implementing TLS with verified cryptographic security. In: IEEE Symposium on Security & Privacy, Oakland (2013)","DOI":"10.1109\/SP.2013.37"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: A Computationally Sound Mechanized Prover for Security Protocols. In: IEEE Symposium on Security and Privacy (S&P 2006). IEEE Computer Society (2006)","DOI":"10.1109\/SP.2006.1"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-642-36830-1_4","volume-title":"Principles of Security and Trust","author":"D. Cad\u00e9","year":"2013","unstructured":"Cad\u00e9, D., Blanchet, B.: Proved Generation of Implementations from Computationally Secure Protocol Specifications. In: Basin, D., Mitchell, J.C. (eds.) POST 2013. LNCS, vol.\u00a07796, pp. 63\u201382. Springer, Heidelberg (2013)"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Canetti, R.: Universally Composable Security: A New Paradigm for Cryptographic Protocols. In: Proceedings of the 42nd Annual Symposium on Foundations of Computer Science (FOCS 2001). IEEE Computer Society (2001)","DOI":"10.1109\/SFCS.2001.959888"},{"key":"12_CR10","unstructured":"Canetti, R.: Universally Composable Signature, Certification, and Authentication. In: Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW-17 2004). IEEE Computer Society (2004)"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Chaki, S., Datta, A.: ASPIER: An automated framework for verifying security protocol implementations. In: Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF 2009). IEEE Computer Society (2009)","DOI":"10.1109\/CSF.2009.20"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Fournet, C., Kohlweiss, M., Strub, P.-Y.: Modular code-based cryptographic verification. In: Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS 2011). ACM (2011)","DOI":"10.1145\/2046707.2046746"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security Policies and Security Models. In: Proceedings of IEEE Symposium on Security and Privacy (1982)","DOI":"10.1109\/SP.1982.10014"},{"issue":"2","key":"12_CR14","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1137\/0217017","volume":"17","author":"S. Goldwasser","year":"1988","unstructured":"Goldwasser, S., Micali, S., Rivest, R.L.: A digital signature scheme secure against adaptive chosen-message attacks. SIAM Journal on Computing\u00a017(2), 281\u2013308 (1988)","journal-title":"SIAM Journal on Computing"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-30579-8_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Goubault-Larrecq","year":"2005","unstructured":"Goubault-Larrecq, J., Parrennes, F.: Cryptographic protocol analysis on real C code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 363\u2013379. Springer, Heidelberg (2005)"},{"key":"12_CR16","unstructured":"Graf, J., Hecker, M., Mohr, M.: Using JOANA for Information Flow Control in Java Programs - A Practical Guide. In: Proceedings of the 6th Working Conference on Programming Languages (ATPS 2013). Lecture Notes in Informatics (LNI), vol.\u00a0215. Springer, Heidelberg (2013)"},{"issue":"6","key":"12_CR17","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/s10207-009-0086-1","volume":"8","author":"C. Hammer","year":"2009","unstructured":"Hammer, C., Snelting, G.: Flow-Sensitive, Context-Sensitive, and Object-sensitive Information Flow Control Based on Program Dependence Graphs. International Journal of Information Security\u00a08(6), 399\u2013422 (2009)","journal-title":"International Journal of Information Security"},{"issue":"4","key":"12_CR18","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G. Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A Machine-Checked Model for a Java-Like Language, Virtual Machine, and Compiler. ACM Trans. Program. Lang. Syst.\u00a028(4), 619\u2013695 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR19","unstructured":"K\u00fcsters, R.: Simulation-Based Security with Inexhaustible Interactive Turing Machines. In: Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW-19 2006). IEEE Computer Society (2006)"},{"key":"12_CR20","unstructured":"K\u00fcsters, R., Tuengerthal, M.: Joint State Theorems for Public-Key Encryption and Digital Signature Functionalities with Local Computation. Technical Report 2008\/006, Cryptology ePrint Archive (2008), \n                    \n                      http:\/\/eprint.iacr.org\/2008\/006"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Tuengerthal, M.: Universally Composable Symmetric Encryption. In: Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF 2009). IEEE Computer Society (2009)","DOI":"10.1109\/CSF.2009.18"},{"key":"12_CR22","unstructured":"K\u00fcsters, R., Scapin, E., Truderung, T., Graf, J.: Extending and Applying a Framework for the Cryptographic Verification of Java Programs. Cryptology ePrint Archive, Report 2014\/038 (2014), \n                    \n                      http:\/\/eprint.iacr.org\/2014\/038"},{"key":"12_CR23","unstructured":"K\u00fcsters, R., Scapin, E., Truderung, T., Graf, J.: A Java Implementation of a Cloud Storage System (2013), \n                    \n                      http:\/\/infsec.uni-trier.de\/publications\/software\/CloudStorage.zip"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T., Graf, J.: A Framework for the Cryptographic Verification of Java-like Programs. In: IEEE Computer Security Foundations Symposium, CSF 2012. IEEE Computer Society (2012)","DOI":"10.1109\/CSF.2012.9"},{"key":"12_CR25","unstructured":"K\u00fcsters, R., Truderung, T., Graf, J.: A Framework for the Cryptographic Verification of Java-like Programs. Cryptology ePrint Archive, Report 2012\/153 (2012), \n                    \n                      http:\/\/eprint.iacr.org\/2012\/153"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Tuengerthal, M.: Joint State Theorems for Public-Key Encryption and Digital Signature Functionalities with Local Computation. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008). IEEE Computer Society (2008)","DOI":"10.1109\/CSF.2008.18"},{"key":"12_CR27","unstructured":"K\u00fcsters, R., Tuengerthal, M.: The IITM Model: a Simple and Expressive Model for Universal Composability. Technical Report 2013\/025, Cryptology ePrint Archive (2013), \n                    \n                      http:\/\/eprint.iacr.org\/2013\/025"},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Nipkow, T., von Oheimb, D.: Java\n                    light\n                   is Type-Safe \u2014 Definitely. In: POPL (1998)","DOI":"10.1145\/268946.268960"},{"key":"12_CR29","unstructured":"Pfitzmann, B., Waidner, M.: A Model for Asynchronous Reactive Systems and its Application to Secure Message Transmission. In: IEEE Symposium on Security and Privacy. EEE Computer Society (2001)"}],"container-title":["Lecture Notes in Computer Science","Principles of Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54792-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T08:08:02Z","timestamp":1558858082000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54792-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642547911","9783642547928"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54792-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}