{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,12]],"date-time":"2025-08-12T21:45:22Z","timestamp":1755035122959,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,10,24]],"date-time":"2016-10-24T00:00:00Z","timestamp":1477267200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["SFB 1223"],"award-info":[{"award-number":["SFB 1223"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Zurich Information Security Center"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,10,24]]},"DOI":"10.1145\/2976749.2978418","type":"proceedings-article","created":{"date-parts":[[2016,10,25]],"date-time":"2016-10-25T12:46:35Z","timestamp":1477399595000},"page":"717-730","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Computational Soundness for Dalvik Bytecode"],"prefix":"10.1145","author":[{"given":"Michael","family":"Backes","sequence":"first","affiliation":[{"name":"Saarland University & MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"K\u00fcnnemann","sequence":"additional","affiliation":[{"name":"Saarland University & MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Esfandiar","family":"Mohammadi","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,10,24]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Accessed","author":"Internet","year":"2015","unstructured":"Symantec, \" Internet security threat report , volume 20 ,\" Accessed : Oct 15, 2015 . {Online}. Available: http:\/\/www.symantec.com\/security_response\/publications\/threatreport.jsp Symantec, \"Internet security threat report, volume 20,\" Accessed: Oct 15, 2015. {Online}. Available: http:\/\/www.symantec.com\/security_response\/publications\/threatreport.jsp"},{"key":"e_1_3_2_1_2_1","volume-title":"Q2\/2015,\" Accessed","author":"Mobile","year":"2015","unstructured":"GData, \" Mobile malware report : Q2\/2015,\" Accessed : Oct 15, 2015 . {Online}. Available: https:\/\/public.gdatasoftware.com\/Presse\/Publikationen\/Malware_Reports\/G_DATA_MobileMWR_Q2_2015_EN.pdf GData, \"Mobile malware report: Q2\/2015,\" Accessed: Oct 15, 2015. {Online}. Available: https:\/\/public.gdatasoftware.com\/Presse\/Publikationen\/Malware_Reports\/G_DATA_MobileMWR_Q2_2015_EN.pdf"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2494522"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666620.2666631"},{"key":"e_1_3_2_1_5_1","volume-title":"ACM AsiaCCS","author":"Backes M.","year":"2016","unstructured":"M. Backes , S. Bugiel , E. Derr , S. Gerling , and C. Hammer , \" R-droid: In-depth application vetting for android with path-sensitive value analysis,\" in Proc . ACM AsiaCCS , 2016 . M. Backes, S. Bugiel, E. Derr, S. Gerling, and C. Hammer, \"R-droid: In-depth application vetting for android with path-sensitive value analysis,\" in Proc. ACM AsiaCCS, 2016."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1653662.1653672"},{"key":"e_1_3_2_1_7_1","unstructured":"S. Meiser \"Computational soundness of passively secure encryption in presence of active adversaries \" Master's thesis at Saarland University 2010.  S. Meiser \"Computational soundness of passively secure encryption in presence of active adversaries \" Master's thesis at Saarland University 2010."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382270"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36830-1_11"},{"key":"e_1_3_2_1_10_1","first-page":"42","volume-title":"3rd POST","author":"Backes M.","year":"2014","unstructured":"M. Backes , E. Mohammadi , and T. Ruffing , \" Computational Soundness Results for ProVerif,\" in Proc . 3rd POST , 2014 , pp. 42 -- 62 . M. Backes, E. Mohammadi, and T. Ruffing, \"Computational Soundness Results for ProVerif,\" in Proc. 3rd POST, 2014, pp. 42--62."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.35"},{"key":"e_1_3_2_1_12_1","volume-title":"Technical report: Computational soundness for dalvik bytecode,\" arXiv:1608.04362","author":"Backes M.","year":"2016","unstructured":"M. Backes , R. K\u00fcnnemann , and E. Mohammadi , \" Technical report: Computational soundness for dalvik bytecode,\" arXiv:1608.04362 , 2016 . M. Backes, R. K\u00fcnnemann, and E. Mohammadi, \"Technical report: Computational soundness for dalvik bytecode,\" arXiv:1608.04362, 2016."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2011.24"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866351"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2013.11.037"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.60"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1554339.1554341"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1662658.1662659"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.04.028"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328479"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537311_32"},{"key":"e_1_3_2_1_22_1","first-page":"159","volume-title":"of 12th ESOP","author":"Laud P.","year":"2003","unstructured":"P. Laud , \" Handling encryption in an analysis for secure information flow,\" in Proc. of 12th ESOP , 2003 , pp. 159 -- 173 . P. Laud, \"Handling encryption in an analysis for secure information flow,\" in Proc. of 12th ESOP, 2003, pp. 159--173."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/948109.948140"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_12"},{"key":"e_1_3_2_1_25_1","first-page":"361","volume-title":"Proc. 4th ISPEC","author":"Galindo D.","year":"2008","unstructured":"D. Galindo , F. D. Garcia , and P. van Rossum , \" Computational Soundness of Non-Malleable Commitments ,\" in Proc. 4th ISPEC , 2008 , pp. 361 -- 376 . D. Galindo, F. D. Garcia, and P. van Rossum, \"Computational Soundness of Non-Malleable Commitments,\" in Proc. 4th ISPEC, 2008, pp. 361--376."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_9"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046717"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516711"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455770.1455786"},{"key":"e_1_3_2_1_30_1","first-page":"254","volume-title":"5rd POS","author":"Shao J.","year":"2016","unstructured":"J. Shao , Y. Qin , and D. Feng , \" Computational Soundness Results for Stateful Applied Pi Calculus,\" in Proc . 5rd POS , 2016 , pp. 254 -- 275 . J. Shao, Y. Qin, and D. Feng, \"Computational Soundness Results for Stateful Applied Pi Calculus,\" in Proc. 5rd POS, 2016, pp. 254--275."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382271"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_11"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660276"},{"key":"e_1_3_2_1_34_1","first-page":"71","volume-title":"CRYPTO","author":"Barthe G.","year":"2011","unstructured":"G. Barthe , B. Gr\u00e9goire , S. Heraud , and S.-Z. B\u00e9guelin , \" Computer-Aided Security Proofs for the Working Cryptographer,\" in Proc . CRYPTO , 2011 , pp. 71 -- 90 . G. Barthe, B. Gr\u00e9goire, S. Heraud, and S.-Z. B\u00e9guelin, \"Computer-Aided Security Proofs for the Working Cryptographer,\" in Proc. CRYPTO, 2011, pp. 71--90."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"e_1_3_2_1_36_1","first-page":"503","volume-title":"25th ESOP","author":"Lochbihler A.","year":"2016","unstructured":"A. Lochbihler , \"Probabilistic functions and cryptographic oracles in higher order logic,\" in Proc . 25th ESOP , 2016 , pp. 503 -- 531 . A. Lochbihler, \"Probabilistic functions and cryptographic oracles in higher order logic,\" in Proc. 25th ESOP, 2016, pp. 503--531."}],"event":{"name":"CCS'16: 2016 ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Vienna Austria","acronym":"CCS'16"},"container-title":["Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2976749.2978418","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2976749.2978418","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:49:54Z","timestamp":1750218594000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2976749.2978418"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,24]]},"references-count":36,"alternative-id":["10.1145\/2976749.2978418","10.1145\/2976749"],"URL":"https:\/\/doi.org\/10.1145\/2976749.2978418","relation":{},"subject":[],"published":{"date-parts":[[2016,10,24]]},"assertion":[{"value":"2016-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}