{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T18:23:48Z","timestamp":1740162228271,"version":"3.37.3"},"reference-count":58,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T00:00:00Z","timestamp":1558742400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T00:00:00Z","timestamp":1558742400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001729","name":"Stiftelsen f\u00f6r Strategisk Forskning","doi-asserted-by":"publisher","award":["PROSPER"],"award-info":[{"award-number":["PROSPER"]}],"id":[{"id":"10.13039\/501100001729","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001858","name":"VINNOVA","doi-asserted-by":"publisher","award":["HASPOC"],"award-info":[{"award-number":["HASPOC"]}],"id":[{"id":"10.13039\/501100001858","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100009527","name":"Myndigheten f\u00f6r Samh\u00e4llsskydd och Beredskap","doi-asserted-by":"publisher","award":["CERCES"],"award-info":[{"award-number":["CERCES"]}],"id":[{"id":"10.13039\/100009527","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Cryptogr Eng"],"published-print":{"date-parts":[[2019,9]]},"DOI":"10.1007\/s13389-019-00216-4","type":"journal-article","created":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T14:03:47Z","timestamp":1558793027000},"page":"243-261","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["On the verification of system-level information flow properties for virtualized execution platforms"],"prefix":"10.1007","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4889-8326","authenticated-orcid":false,"given":"Christoph","family":"Baumann","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3434-5640","authenticated-orcid":false,"given":"Oliver","family":"Schwarz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5432-6442","authenticated-orcid":false,"given":"Mads","family":"Dam","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,5,25]]},"reference":[{"issue":"5","key":"216_CR1","doi-asserted-by":"publisher","first-page":"1543","DOI":"10.1145\/186025.186058","volume":"16","author":"M Abadi","year":"1994","unstructured":"Abadi, M., Lamport, L.: An old-fashioned recipe for real time. ACM Trans. Program. Lang. Syst. 16(5), 1543\u20131571 (1994). \n                    https:\/\/doi.org\/10.1145\/186025.186058","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"216_CR2","doi-asserted-by":"crossref","unstructured":"Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software verification for weak memory via program transformation. In: European Symposium on Programming, pp. 512\u2013532. Springer (2013)","DOI":"10.1007\/978-3-642-37036-6_28"},{"issue":"2","key":"216_CR3","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/2627752","volume":"36","author":"J Alglave","year":"2014","unstructured":"Alglave, J., Maranget, L., Tautschnig, M.: Herding cats: modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. (TOPLAS) 36(2), 7 (2014)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"216_CR4","doi-asserted-by":"crossref","unstructured":"Alkassar, E., Hillebrand, M.A., Paul, W.J., Petrova, E.: Automated verification of a small hypervisor. In: Proceedings of VSTTE, LNCS, vol. 6217, pp. 40\u201354. Springer (2010)","DOI":"10.1007\/978-3-642-15057-9_3"},{"key":"216_CR5","doi-asserted-by":"publisher","unstructured":"Alur, R., Dang, T., Esposito, J., Fierro, R., Hur, Y., Ivan\u010di\u0107, F., Kumar, V., Lee, I., Mishra, P., Pappas, G., Sokolsky, O.: Hierarchical hybrid modeling of embedded systems. In: Embedded Software (EMSOFT), pp. 14\u201331. Springer (2001). \n                    https:\/\/doi.org\/10.1007\/3-540-45449-7_2","DOI":"10.1007\/3-540-45449-7_2"},{"key":"216_CR6","doi-asserted-by":"crossref","unstructured":"Barthe, G., Betarte, G., Campo, J.D., Luna, C.: Formally verifying isolation and availability in an idealized model of virtualization. In: Formal Methods, pp. 231\u2013245 (2011)","DOI":"10.1007\/978-3-642-21437-0_19"},{"key":"216_CR7","doi-asserted-by":"publisher","unstructured":"Barthe, G., Betarte, G., Campo, J.D., Luna, C.: Cache-leakage resilient os isolation in an idealized model of virtualization. In: Proceedings of CSF\u201912, pp. 186\u2013197. IEEE (2012). \n                    https:\/\/doi.org\/10.1109\/CSF.2012.17","DOI":"10.1109\/CSF.2012.17"},{"key":"216_CR8","doi-asserted-by":"crossref","unstructured":"Baumann, C., N\u00e4slund, M., Gehrmann, C., Schwarz, O., Thorsen, H.: A high assurance virtualization platform for ARMv8. In: European Conference on Networks and Communications (EuCNC), pp. 210\u2013214 (2016)","DOI":"10.1109\/EuCNC.2016.7561034"},{"key":"216_CR9","unstructured":"Baumann, C., Schwarz, O., Dam, M.: GitHub repository of formal artifacts and technical documentation. \n                    https:\/\/github.com\/rauhbein\/haspocproofs\n                    \n                  . Accessed 23 May 2019"},{"key":"216_CR10","unstructured":"Bellard, F.: QEMU, a fast and portable dynamic translator. In: USENIX Annual Technical Conference, FREENIX Track, vol.\u00a041, p.\u00a046 (2005)"},{"issue":"2","key":"216_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2024716.2024718","volume":"39","author":"N Binkert","year":"2011","unstructured":"Binkert, N., Beckmann, B., Black, G., Reinhardt, S.K., Saidi, A., Basu, A., Hestness, J., Hower, D.R., Krishna, T., Sardashti, S., Sen, R., Sewell, K., Shoaib, M., Vaish, N., Hill, M.D., Wood, D.A.: The gem5 simulator. SIGARCH Comput. Archit. News 39(2), 1\u20137 (2011). \n                    https:\/\/doi.org\/10.1145\/2024716.2024718","journal-title":"SIGARCH Comput. Archit. News"},{"key":"216_CR12","doi-asserted-by":"crossref","unstructured":"Bolignano, P., Jensen, T., Siles, V.: Modeling and abstraction of memory management in a hypervisor. In: FASE\/ETAPS, pp. 214\u2013230. Springer (2016)","DOI":"10.1007\/978-3-662-49665-7_13"},{"key":"216_CR13","doi-asserted-by":"publisher","unstructured":"Chen, H., Wu, X.N., Shao, Z., Lockerman, J., Gu, R.: Toward compositional verification of interruptible OS kernels and device drivers. In: Proceedings of Programming Language Design and Implementation, PLDI\u201916, pp. 431\u2013447. ACM (2016). \n                    https:\/\/doi.org\/10.1145\/2908080.2908101","DOI":"10.1145\/2908080.2908101"},{"key":"216_CR14","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/j.scico.2014.06.011","volume":"97","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97, 333\u2013348 (2015)","journal-title":"Sci. Comput. Program."},{"key":"216_CR15","doi-asserted-by":"crossref","unstructured":"Dam, M., Guanciale, R., Khakpour, N., Nemati, H., Schwarz, O.: Formal verification of information flow security for a simple ARM-based separation kernel. In: Proceedings of Computer and Communications Security, CCS\u201913, pp. 223\u2013234. ACM (2013)","DOI":"10.1145\/2508859.2516702"},{"key":"216_CR16","doi-asserted-by":"crossref","unstructured":"Feiertag, R.J., Neumann, P.G.: The foundations of a provably secure operating system (PSOS). In: National Computer Conference, pp. 329\u2013334. AFIPS Press (1979)","DOI":"10.1109\/MARK.1979.8817256"},{"key":"216_CR17","doi-asserted-by":"crossref","unstructured":"Fox, A.C.J.: Improved tool support for machine-code decompilation in HOL4. In: Interactive Theorem Proving (ITP), pp. 187\u2013202 (2015)","DOI":"10.1007\/978-3-319-22102-1_12"},{"issue":"1","key":"216_CR18","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1109\/54.350695","volume":"12","author":"DD Gajski","year":"1995","unstructured":"Gajski, D.D., Vahid, F.: Specification and design of embedded hardware\u2013software systems. IEEE Des. Test Comput. 12(1), 53\u201367 (1995). \n                    https:\/\/doi.org\/10.1109\/54.350695","journal-title":"IEEE Des. Test Comput."},{"issue":"1","key":"216_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s13389-016-0141-6","volume":"8","author":"Q Ge","year":"2018","unstructured":"Ge, Q., Yarom, Y., Cock, D., Heiser, G.: A survey of microarchitectural timing attacks and countermeasures on contemporary hardware. J. Cryptogr. Eng. 8(1), 1\u201327 (2018)","journal-title":"J. Cryptogr. Eng."},{"key":"216_CR20","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: Security and Privacy, 1982 IEEE Symposium on, pp. 11\u201311. IEEE (1982)"},{"key":"216_CR21","doi-asserted-by":"crossref","unstructured":"Gu, L., Vaynberg, A., Ford, B., Shao, Z., Costanzo, D.: CertiKOS: a certified kernel for secure cloud computing. In: Proceedings of the Second Asia-Pacific Workshop on Systems, APSys\u201911, p.\u00a03. ACM (2011)","DOI":"10.1145\/2103799.2103803"},{"key":"216_CR22","unstructured":"Gu, R., Shao, Z., Chen, H., Wu, X., Kim, J., Sj\u00f6berg, V., Costanzo, D.: CertiKOS: An extensible architecture for building certified concurrent OS kernels. In: Operating Systems Design and Implementation, pp. 653\u2013669. USENIX Association (2016)"},{"key":"216_CR23","doi-asserted-by":"publisher","unstructured":"Guanciale, R., Nemati, H., Baumann, C., Dam, M.: Cache storage channels: alias-driven attacks and verified countermeasures. In: Security and Privacy, pp. 38\u201355 (2016). \n                    https:\/\/doi.org\/10.1109\/SP.2016.11","DOI":"10.1109\/SP.2016.11"},{"issue":"6","key":"216_CR24","doi-asserted-by":"publisher","first-page":"793","DOI":"10.3233\/JCS-160558","volume":"24","author":"R Guanciale","year":"2016","unstructured":"Guanciale, R., Nemati, H., Dam, M., Baumann, C.: Provably secure memory isolation for linux on ARM. J. Comput. Secur. 24(6), 793\u2013837 (2016). \n                    https:\/\/doi.org\/10.3233\/JCS-160558","journal-title":"J. Comput. Secur."},{"key":"216_CR25","unstructured":"HASPOC Project. \n                    http:\/\/haspoc.sics.se\/\n                    \n                  . Accessed 23 May 2019"},{"key":"216_CR26","unstructured":"Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad apps: end-to-end security via automated full-system verification. In: Operating Systems Design and Implementation, pp. 165\u2013181. USENIX Association (2014)"},{"key":"216_CR27","unstructured":"He, N., Kroening, D., Wahl, T., Lau, K.K., Taweel, F., Tran, C., R\u00fcmmer, P., Sharma, S.: Component-based design and verification in X-MAN. In: Proceedings of Embedded Real Time Software and Systems (2012)"},{"key":"216_CR28","doi-asserted-by":"crossref","unstructured":"Heule, S., Schkufza, E., Sharma, R., Aiken, A.: Stratified synthesis: automatically learning the x86-64 instruction set. In: ACM SIGPLAN Notices, vol.\u00a051, pp. 237\u2013250. ACM (2016)","DOI":"10.1145\/2980983.2908121"},{"key":"216_CR29","doi-asserted-by":"crossref","unstructured":"Inci, M.S., Gulmezoglu, B., Irazoqui, G., Eisenbarth, T., Sunar, B.: Cache attacks enable bulk key recovery on the cloud. In: International Conference on Cryptographic Hardware and Embedded Systems, pp. 368\u2013388. Springer (2016)","DOI":"10.1007\/978-3-662-53140-2_18"},{"issue":"4","key":"216_CR30","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1145\/138873.138876","volume":"10","author":"RE Kessler","year":"1992","unstructured":"Kessler, R.E., Hill, M.D.: Page placement algorithms for large real-indexed caches. ACM Trans. Comput. Syst. (TOCS) 10(4), 338\u2013359 (1992)","journal-title":"ACM Trans. Comput. Syst. (TOCS)"},{"key":"216_CR31","doi-asserted-by":"crossref","unstructured":"Khakpour, N., Schwarz, O., Dam, M.: Machine assisted proof of ARMv7 instruction level isolation properties. In: Certified Programs and Proofs, pp. 276\u2013291. Springer (2013)","DOI":"10.1007\/978-3-319-03545-1_18"},{"issue":"1","key":"216_CR32","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/2560537","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T.C., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2 (2014). \n                    https:\/\/doi.org\/10.1145\/2560537","journal-title":"ACM Trans. Comput. Syst."},{"key":"216_CR33","doi-asserted-by":"crossref","unstructured":"Kocher, P., Genkin, D., Gruss, D., Haas, W., Hamburg, M., Lipp, M., Mangard, S., Prescher, T., Schwarz, M., Yarom, Y.: Spectre attacks: exploiting speculative execution. arXiv preprint \n                    arXiv:1801.01203\n                    \n                   (2018)","DOI":"10.1109\/SP.2019.00002"},{"key":"216_CR34","unstructured":"Lipp, M., Schwarz, M., Gruss, D., Prescher, T., Haas, W., Fogh, A., Horn, J., Mangard, S., Kocher, P., Genkin, D., Yarom, Y.: Meltdown: reading kernel memory from user space. In: 27th USENIX Security Symposium (USENIX Security 18), pp. 973\u2013990 (2018)"},{"issue":"12","key":"216_CR35","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975)","journal-title":"Commun. ACM"},{"key":"216_CR36","doi-asserted-by":"crossref","unstructured":"Nemati, H., Baumann, C., Guanciale, R., Dam, M.: Formal verification of integrity-preserving countermeasures against cache storage side-channels. In: International Conference on Principles of Security and Trust (POST 2018), pp. 109\u2013133. Springer (2018)","DOI":"10.1007\/978-3-319-89722-6_5"},{"key":"216_CR37","doi-asserted-by":"publisher","unstructured":"Nemati, H., Guanciale, R., Dam, M.: Trustworthy virtualization of the ARMv7 memory subsystem. In: SOFSEM, pp. 578\u2013589. Springer (2015). \n                    https:\/\/doi.org\/10.1007\/978-3-662-46078-8_48","DOI":"10.1007\/978-3-662-46078-8_48"},{"key":"216_CR38","volume-title":"Badusb\u2013On Accessories that Turn Evil","author":"K Nohl","year":"2014","unstructured":"Nohl, K., Lell, J.: Badusb\u2013On Accessories that Turn Evil. Black Hat USA, Las Vegas (2014)"},{"key":"216_CR39","doi-asserted-by":"crossref","unstructured":"Paul, W.J., Schmaltz, S., Shadrin, A.: Completing the automated verification of a small hypervisor\u2014assembler code verification. In: SEFM, Lecture Notes in Computer Science, vol. 7504, pp. 188\u2013202. Springer (2012)","DOI":"10.1007\/978-3-642-33826-7_13"},{"issue":"POPL","key":"216_CR40","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/3158107","volume":"2","author":"C Pulte","year":"2017","unstructured":"Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S., Sewell, P.: Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8. Proc. ACM Program. Lang. 2(POPL), 19 (2017)","journal-title":"Proc. ACM Program. Lang."},{"key":"216_CR41","doi-asserted-by":"crossref","unstructured":"Reid, A.: Trustworthy specifications of ARMv8-A and v8-M system level architecture. In: Proceedings of Formal Methods in Computer-Aided Design (FMCAD), pp. 161\u2013168. IEEE (2016)","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"216_CR42","unstructured":"RISC-V Foundation: RISC-V\u2014The Free and Open RISC Instruction Set Architecture. \n                    https:\/\/riscv.org\/\n                    \n                  . Accessed 23 May 2019"},{"key":"216_CR43","doi-asserted-by":"publisher","unstructured":"Rowson, J.A., Sangiovanni-Vincentelli, A.: Interface-based design. In: Proceedings of the 34th Annual Design Automation Conference, DAC\u201997, pp. 178\u2013183. ACM (1997). \n                    https:\/\/doi.org\/10.1145\/266021.266060","DOI":"10.1145\/266021.266060"},{"key":"216_CR44","volume-title":"Noninterference, Transitivity, and Channel-Control Security Policies","author":"J Rushby","year":"1992","unstructured":"Rushby, J.: Noninterference, Transitivity, and Channel-Control Security Policies. SRI International, Computer Science Laboratory, Menlo Park (1992)"},{"key":"216_CR45","doi-asserted-by":"crossref","unstructured":"Sang, F.L., Lacombe, E., Nicomette, V., Deswarte, Y.: Exploiting an I\/OMMU vulnerability. In: 2010 5th International Conference on Malicious and Unwanted Software pp. 7\u201314. IEEE (2010)","DOI":"10.1109\/MALWARE.2010.5665798"},{"key":"216_CR46","doi-asserted-by":"publisher","unstructured":"Schwarz, O., Dam, M.: Formal verification of secure user mode device execution with DMA. In: Hardware and Software: Verification and Testing (HVC), No. 8855 in Lecture Notes in Computer Science, pp. 236\u2013251 (2014). \n                    https:\/\/doi.org\/10.1007\/978-3-319-13338-6_18","DOI":"10.1007\/978-3-319-13338-6_18"},{"key":"216_CR47","doi-asserted-by":"crossref","unstructured":"Schwarz, O., Dam, M.: Automatic derivation of platform noninterference properties. In: International Conference on Software Engineering and Formal Methods, pp. 27\u201344. Springer, Cham (2016)","DOI":"10.1007\/978-3-319-41591-8_3"},{"key":"216_CR48","unstructured":"Seaborn, M., Dullien, T.: Exploiting the DRAM rowhammer bug to gain kernel privileges. In: Black Hat 15 (2015). \n                    https:\/\/googleprojectzero.blogspot.com\/2015\/03\/exploiting-dram-rowhammer-bug-to-gain.html\n                    \n                  . Accessed 23 May 2019"},{"key":"216_CR49","unstructured":"Sewell, P., Vitek, J.: Secure composition of insecure components. In: Computer Security Foundations, CSFW\u201999, p. 136. IEEE Computer Society (1999)"},{"key":"216_CR50","doi-asserted-by":"publisher","unstructured":"Sewell, T.A.L., Myreen, M.O., Klein, G.: Translation validation for a verified OS kernel. In: Programming Language Design and Implementation, pp. 471\u2013482 (2013). \n                    https:\/\/doi.org\/10.1145\/2491956.2462183","DOI":"10.1145\/2491956.2462183"},{"key":"216_CR51","doi-asserted-by":"publisher","unstructured":"Stewin, P., Bystrov, I.: Understanding DMA malware. In: Detection of Intrusions and Malware, and Vulnerability Assessment (DIMVA), pp. 21\u201341 (2012). \n                    https:\/\/doi.org\/10.1007\/978-3-642-37300-8_2","DOI":"10.1007\/978-3-642-37300-8_2"},{"key":"216_CR52","unstructured":"Syeda, H., Klein, G.: Reasoning about translation lookaside buffers. In: LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPiC Series in Computing, vol. 46, pp. 490\u2013508. EasyChair (2017)"},{"key":"216_CR53","doi-asserted-by":"crossref","unstructured":"Vafeiadis, V.: Program verification under weak memory consistency using separation logic. In: International Conference on Computer Aided Verification, pp. 30\u201346. Springer (2017)","DOI":"10.1007\/978-3-319-63387-9_2"},{"key":"216_CR54","unstructured":"Vasudevan, A., Chaki, S., Maniatis, P., Jia, L., Datta, A.: \u00fcberSpark: enforcing verifiable object abstractions for automated compositional security analysis of a hypervisor. In: 25th USENIX Security Symposium (USENIX Security 16). USENIX Association (2016)"},{"key":"216_CR55","unstructured":"Weisse, O., Van\u00a0Bulck, J., Minkin, M., Genkin, D., Kasikci, B., Piessens, F., Silberstein, M., Strackx, R., Wenisch, T.F., Yarom, Y.: Foreshadow-NG: breaking the virtual memory abstraction with transient out-of-order execution. Technical Report (2018)"},{"issue":"7","key":"216_CR56","doi-asserted-by":"publisher","first-page":"966","DOI":"10.1109\/TCAD.2009.2013287","volume":"28","author":"R Wilhelm","year":"2009","unstructured":"Wilhelm, R., Grund, D., Reineke, J., Schlickling, M., Pister, M., Ferdinand, C.: Memory hierarchies, pipelines, and buses for future architectures in time-critical embedded systems. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 28(7), 966 (2009)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"216_CR57","volume-title":"Subverting the Xen hypervisor","author":"R Wojtczuk","year":"2008","unstructured":"Wojtczuk, R.: Subverting the Xen hypervisor. Black Hat USA, Las Vegas (2008)"},{"issue":"5","key":"216_CR58","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1016\/j.jss.2006.08.015","volume":"80","author":"F Xie","year":"2007","unstructured":"Xie, F., Yang, G., Song, X.: Component-based hardware\/software co-verification for building trustworthy embedded systems. J. Syst. Softw. 80(5), 643\u2013654 (2007). \n                    https:\/\/doi.org\/10.1016\/j.jss.2006.08.015","journal-title":"J. Syst. Softw."}],"container-title":["Journal of Cryptographic Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s13389-019-00216-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s13389-019-00216-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s13389-019-00216-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,23]],"date-time":"2020-05-23T23:14:32Z","timestamp":1590275672000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s13389-019-00216-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,5,25]]},"references-count":58,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,9]]}},"alternative-id":["216"],"URL":"https:\/\/doi.org\/10.1007\/s13389-019-00216-4","relation":{},"ISSN":["2190-8508","2190-8516"],"issn-type":[{"type":"print","value":"2190-8508"},{"type":"electronic","value":"2190-8516"}],"subject":[],"published":{"date-parts":[[2019,5,25]]},"assertion":[{"value":"31 January 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 May 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 May 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}