{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T23:10:17Z","timestamp":1771888217838,"version":"3.50.1"},"reference-count":77,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2017,12,19]],"date-time":"2017-12-19T00:00:00Z","timestamp":1513641600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int. J. Inf. Secur."],"published-print":{"date-parts":[[2018,11]]},"DOI":"10.1007\/s10207-017-0398-5","type":"journal-article","created":{"date-parts":[[2017,12,19]],"date-time":"2017-12-19T13:22:57Z","timestamp":1513689777000},"page":"719-738","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":58,"title":["Talos: no more ransomware victims with formal methods"],"prefix":"10.1007","volume":"17","author":[{"given":"Aniello","family":"Cimitile","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Mercaldo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vittoria","family":"Nardone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonella","family":"Santone","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Corrado Aaron","family":"Visaggio","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,19]]},"reference":[{"issue":"4","key":"398_CR1","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/s11416-011-0152-x","volume":"7","author":"B Anderson","year":"2011","unstructured":"Anderson, B., Quist, D., Neil, J., Storlie, C., Lane, T.: Graph-based malware detection using dynamic analysis. J. Comput. Virol. 7(4), 247\u2013258 (2011)","journal-title":"J. Comput. Virol."},{"key":"398_CR2","doi-asserted-by":"crossref","unstructured":"Andronio, N., Zanero, S., Maggi, F.: Heldroid: Dissecting and detecting mobile ransomware. In: International Workshop on Recent Advances in Intrusion Detection, pp. 382\u2013404. Springer (2015)","DOI":"10.1007\/978-3-319-26362-5_18"},{"issue":"2","key":"398_CR3","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/s11416-014-0215-x","volume":"11","author":"C Annachhatre","year":"2015","unstructured":"Annachhatre, C., Austin, T.H., Stamp, M.: Hidden markov models for malware classification. J. Comput. Virol. Hacking Tech. 11(2), 59\u201373 (2015)","journal-title":"J. Comput. Virol. Hacking Tech."},{"key":"398_CR4","doi-asserted-by":"crossref","unstructured":"Arp, D., Spreitzenbarth, M., Huebner, M., Gascon, H., Rieck, K.: Drebin: efficient and explainable detection of android malware in your pocket. In: Proceedings of 21th Annual Network and Distributed System Security Symposium (NDSS), IEEE (2014)","DOI":"10.14722\/ndss.2014.23247"},{"issue":"2","key":"398_CR5","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/s11416-008-0105-1","volume":"5","author":"S Attaluri","year":"2009","unstructured":"Attaluri, S., McGhee, S., Stamp, M.: Profile hidden markov models and metamorphic virus detection. J. Comput. Virol. 5(2), 151\u2013169 (2009)","journal-title":"J. Comput. Virol."},{"issue":"2","key":"398_CR6","first-page":"48","volume":"6","author":"S Aurangzeb","year":"2017","unstructured":"Aurangzeb, S., Aleem, M., Iqbal, M.A., Islam, M.A.: Ransomware: a survey and trends. J. Inf. Assur. Secur. 6(2), 48\u201358 (2017)","journal-title":"J. Inf. Assur. Secur."},{"key":"398_CR7","doi-asserted-by":"crossref","unstructured":"Battista, P., Mercaldo, F., Nardone, V., Santone, A., Visaggio, C.: Identification of android malware families with model checking. In: International Conference on Information Systems Security and Privacy, SCITEPRESS (2016)","DOI":"10.5220\/0005809205420547"},{"issue":"1","key":"398_CR8","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/s11416-006-0012-2","volume":"2","author":"U Bayer","year":"2006","unstructured":"Bayer, U., Moser, A., Kruegel, C., Kirda, E.: Dynamic analysis of malicious code. J. Comput. Virol. 2(1), 67\u201377 (2006)","journal-title":"J. Comput. Virol."},{"key":"398_CR9","doi-asserted-by":"crossref","unstructured":"Burguera, I., Zurutuza, U., Nadjm-Tehrani, S.: Crowdroid: behavior-based malware detection system for android. In: Proceedings of the 1st ACM Workshop on Security and Privacy in Smartphones and Mobile Devices, ACM, pp. 15\u201326 (2011)","DOI":"10.1145\/2046614.2046619"},{"key":"398_CR10","doi-asserted-by":"crossref","unstructured":"Canfora, G., De Lorenzo, A., Medvet, E., Mercaldo, F., Visaggio, C.A.: Effectiveness of opcode ngrams for detection of multi family android malware. In: 2015 10th International Conference on Availability, Reliability and Security (ARES), IEEE, pp. 333\u2013340 (2015)","DOI":"10.1109\/ARES.2015.57"},{"key":"398_CR11","doi-asserted-by":"crossref","unstructured":"Canfora, G., Di Sorbo, A., Mercaldo, F., Visaggio, C. A.: Obfuscation techniques against signature-based detection: a case study. In: 2015 Mobile Systems Technologies Workshop (MST), IEEE, pp. 21\u201326 (2015)","DOI":"10.1109\/MST.2015.8"},{"key":"398_CR12","doi-asserted-by":"crossref","unstructured":"Canfora, G., Medvet, E., Mercaldo, F., Visaggio, C.A.: Detecting android malware using sequences of system calls. In: Proceedings of the 3rd International Workshop on Software Development Lifecycle for Mobile, ACM, pp. 13\u201320 (2015)","DOI":"10.1145\/2804345.2804349"},{"key":"398_CR13","doi-asserted-by":"crossref","unstructured":"Canfora, G., Mercaldo, F., Moriano, G., Visaggio, C.A.: Composition-malware: building android malware at run time. In: 2015 10th International Conference on Availability, Reliability and Security (ARES), IEEE, pp. 318\u2013326 (2015)","DOI":"10.1109\/ARES.2015.64"},{"key":"398_CR14","doi-asserted-by":"crossref","unstructured":"Canfora, G., Mercaldo, F., Visaggio, C.A.: A classifier of malicious android applications. In: 2013 Eighth International Conference on Availability, Reliability and Security (ARES), IEEE, pp. 607\u2013614 (2013)","DOI":"10.1109\/ARES.2013.80"},{"key":"398_CR15","doi-asserted-by":"crossref","unstructured":"Canfora, G., Mercaldo, F., Visaggio, C.A.: Evaluating op-code frequency histograms in malware and third-party mobile applications. In: E-Business and Telecommunications, Springer, pp. 201\u2013222 (2015)","DOI":"10.1007\/978-3-319-30222-5_10"},{"key":"398_CR16","doi-asserted-by":"crossref","unstructured":"Canfora, G., Mercaldo, F., Visaggio, C.A.: Mobile malware detection using op-code frequency histograms. In: Proceedings of International Conference on Security and Cryptography (SECRYPT) (2015)","DOI":"10.5220\/0005537800270038"},{"key":"398_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.cose.2016.04.009","volume":"61","author":"G Canfora","year":"2016","unstructured":"Canfora, G., Mercaldo, F., Visaggio, C.A.: An hmm and structural entropy based detector for android malware: an empirical study. Comput. Secur. 61, 1\u201318 (2016)","journal-title":"Comput. Secur."},{"issue":"2","key":"398_CR18","doi-asserted-by":"crossref","first-page":"137","DOI":"10.3233\/JCS-150540","volume":"24","author":"H Carter","year":"2015","unstructured":"Carter, H., Mood, B., Traynor, P., Butler, K.R.B.: Secure outsourced garbled circuit evaluation for mobile devices. J. Comput. Secur. 24(2), 137\u2013180 (2015)","journal-title":"J. Comput. Secur."},{"key":"398_CR19","unstructured":"Chenette, S.: The ultimate deobfuscator. In: Proceedings of the ToorConX Conference (2008)"},{"key":"398_CR20","doi-asserted-by":"crossref","unstructured":"Christodorescu, M., Jha, S.: Static analysis of executables to detect malicious patterns. Technical Report, DTIC Document (2006)","DOI":"10.21236\/ADA449067"},{"key":"398_CR21","doi-asserted-by":"crossref","unstructured":"Christodorescu, M., Jha, S., Seshia, S.A., Song, D., Bryant, R.E.: Semantics-aware malware detection. In: 2005 IEEE Symposium on Security and Privacy (S&P\u201905), IEEE, pp. 32\u201346 (2005)","DOI":"10.1109\/SP.2005.20"},{"key":"398_CR22","doi-asserted-by":"crossref","unstructured":"Cimitile, A., Mercaldo, F., Martinelli, F., Nardone, V., Santone, A., Vaglini, G.: Model checking for mobile android malware evolution. In: Proceedings of the 5th International FME Workshop on Formal Methods in Software Engineering, FormaliSE \u201917, Piscataway, NJ, USA, IEEE Press, pp. 24\u201330 (2017)","DOI":"10.1109\/FormaliSE.2017.4"},{"key":"398_CR23","volume-title":"Model Checking","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"398_CR24","volume-title":"CAV. Lecture Notes in Computer Science","author":"R Cleaveland","year":"1996","unstructured":"Cleaveland, R., Sims, S.: The NCSU concurrency workbench. In: Alur, R., Henzinger, T.A. (eds.) CAV. Lecture Notes in Computer Science, vol. 1102. Springer, Berlin (1996)"},{"issue":"6","key":"398_CR25","doi-asserted-by":"crossref","first-page":"793","DOI":"10.1142\/S0218488512400247","volume":"20","author":"SDC Vimercati di","year":"2012","unstructured":"di Vimercati, S.D.C., Foresti, S., Livraga, G., Samarati, P.: Data privacy: definitions and techniques. Int. J. Uncertain. Fuzziness Knowl. Based Syst. 20(6), 793\u2013818 (2012)","journal-title":"Int. J. Uncertain. Fuzziness Knowl. Based Syst."},{"key":"398_CR26","doi-asserted-by":"crossref","unstructured":"Dworkin, M.: Recommendation for block cipher modes of operation. http:\/\/csrc.nist.gov\/publications\/nistpubs\/800-38a\/sp800-38a.pdf (2001)","DOI":"10.6028\/NIST.SP.800-38a"},{"issue":"2","key":"398_CR27","doi-asserted-by":"crossref","first-page":"998","DOI":"10.1109\/COMST.2014.2386139","volume":"17","author":"P Faruki","year":"2015","unstructured":"Faruki, P., Bharmal, A., Laxmi, V., Ganmoor, V., Gaur, M.S., Conti, M., Rajarajan, M.: Android security: a survey of issues, malware penetration, and defenses. Commun. Surv. Tutor. IEEE 17(2), 998\u20131022 (2015)","journal-title":"Commun. Surv. Tutor. IEEE"},{"key":"398_CR28","unstructured":"Feinstein, B., Peck, D., SecureWorks, I.: Caffeine monkey: automated collection, detection and analysis of malicious javascript. In: Black Hat, USA (2007)"},{"key":"398_CR29","unstructured":"FIPS. Advanced encryption standard. http:\/\/csrc.nist.gov\/publications\/fips\/fips197\/fips-197.pdf (2001)"},{"key":"398_CR30","unstructured":"Ford, S., Cova, M., Kruegel, C., Vigna, G.: Analyzing and detecting malicious flash advertisements. In: Proceedings of the Computer Security Applications Conference, 2009. ACSAC\u201909. Annual. pp. 363\u2013372. IEEE (2009)"},{"issue":"1","key":"398_CR31","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1016\/j.ins.2006.03.008","volume":"177","author":"ND Francesco","year":"2007","unstructured":"Francesco, N.D., Santone, A., Vaglini, G.: A user-friendly interface to specify temporal properties of concurrent systems. Inf. Sci. 177(1), 299\u2013311 (2007)","journal-title":"Inf. Sci."},{"issue":"4","key":"398_CR32","first-page":"18","volume":"8","author":"M Gharacheh","year":"2016","unstructured":"Gharacheh, M., Derhami, V., Hashemi, S., Fard, S.M.H.: Detection of metamorphic malware based on hmm: a hierarchical approach. Int. J. Intell. Syst. Appl. 8(4), 18 (2016)","journal-title":"Int. J. Intell. Syst. Appl."},{"key":"398_CR33","doi-asserted-by":"crossref","unstructured":"Hallaraker, O., Vigna, G.: Detecting malicious javascript code in mozilla. In: 10th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS\u201905), IEEE, pp. 85\u201394 (2005)","DOI":"10.1109\/ICECCS.2005.35"},{"key":"398_CR34","unstructured":"Hampton, N., Baig, Z.A.: Ransomware: emergence of the cyber-extortion menace In: Proceedings of the 13th Australian Information Security Management Conference, 2015. pp. 47\u201356. SRI Security Research Institute, Edith Cowan University (2015)"},{"key":"398_CR35","unstructured":"Hartstein, B.: Jsunpack: an automatic javascript unpacker. In: ShmooCon Convention (2009)"},{"key":"398_CR36","doi-asserted-by":"crossref","unstructured":"Jackson, W.: An introduction to the android application development platform. In: Android Apps for Absolute Beginners, Springer, pp. 61\u201399 (2014)","DOI":"10.1007\/978-1-4842-0019-3_3"},{"key":"398_CR37","doi-asserted-by":"crossref","unstructured":"Jacob, G., Filiol, E., Debar, H.: Formalization of viruses and malware through process algebras. In: International Conference on Availability, Reliability and Security (ARES 2010), IEEE (2010)","DOI":"10.1109\/ARES.2010.59"},{"key":"398_CR38","unstructured":"Jang, J., Woo, M., Brumley, D.: Towards automatic software lineage inference. In: USENIX Security, pp. 81\u201396 (2013)"},{"key":"398_CR39","unstructured":"Kaspersky. Mobile malware evolution 2016. https:\/\/securelist.com\/files\/2017\/02\/Mobile_report_2016.pdf"},{"key":"398_CR40","volume-title":"Detecting Malicious Code by Model Checking","author":"J Kinder","year":"2005","unstructured":"Kinder, J., Katzenbeisser, S., Schallhart, C., Veith, H.: Detecting Malicious Code by Model Checking. Springer, Berlin (2005)"},{"key":"398_CR41","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"398_CR42","doi-asserted-by":"crossref","unstructured":"Li, J., Xu, M., Zheng, N., Xu, J.: Malware obfuscation detection via maximal patterns. In: Third International Symposium on Intelligent Information Technology Application, IITA 2009, vol 2, IEEE, pp. 324\u2013328 (2009)","DOI":"10.1109\/IITA.2009.109"},{"key":"398_CR43","doi-asserted-by":"crossref","unstructured":"Likarish, P., Jung, E., Jo, I.: Obfuscated malicious javascript detection using classification techniques. In: MALWARE, Citeseer, pp. 47\u201354 (2009)","DOI":"10.1109\/MALWARE.2009.5403020"},{"key":"398_CR44","doi-asserted-by":"crossref","unstructured":"Liu, X., Liu, J.: A two-layered permission-based android malware detection scheme. In: 2014 2nd IEEE International Conference on Mobile Cloud Computing, Services, and Engineering (MobileCloud), IEEE, pp. 142\u2013148 (2014)","DOI":"10.1109\/MobileCloud.2014.22"},{"key":"398_CR45","doi-asserted-by":"crossref","unstructured":"Maier, D., M\u00fcller, T., Protsenko, M.: Divide-and-conquer: why android malware cannot be stopped. In: 2014 Ninth International Conference on Availability, Reliability and Security (ARES), IEEE, pp. 30\u201339 (2014)","DOI":"10.1109\/ARES.2014.12"},{"key":"398_CR46","doi-asserted-by":"crossref","unstructured":"Mercaldo, F., Nardone, V., Santone, A.: Ransomware inside out. In: 2016 11th International Conference on Availability, Reliability and Security (ARES), IEEE, pp. 628\u2013637 (2016)","DOI":"10.1109\/ARES.2016.35"},{"key":"398_CR47","doi-asserted-by":"crossref","unstructured":"Mercaldo, F., Nardone, V., Santone, A., Visaggio, C.A.: Download malware? No, thanks. How formal methods can block update attacks. In: 2016 IEEE\/ACM 4th FME Workshop on Formal Methods in Software Engineering (FormaliSE), IEEE (2016)","DOI":"10.1145\/2897667.2897673"},{"key":"398_CR48","doi-asserted-by":"crossref","unstructured":"Mercaldo, F., Nardone, V., Santone, A., Visaggio, C.A.: Hey malware, I can find you! In: 25th IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE Workshops 2016, Paris, June 13\u201315 (2016)","DOI":"10.1109\/WETICE.2016.67"},{"key":"398_CR49","doi-asserted-by":"crossref","unstructured":"Mercaldo, F., Nardone, V., Santone, A., Visaggio, C.A.: Ransomware steals your phone formal methods rescue it. In: International Conference on Formal Techniques for Distributed Objects, Components, and Systems, Springer, pp. 212\u2013221 (2016)","DOI":"10.1007\/978-3-319-39570-8_14"},{"key":"398_CR50","doi-asserted-by":"crossref","unstructured":"Mercaldo, F., Visaggio, C.A., Canfora, G., Cimitile, A.: Mobile malware detection in the real world. In: Proceedings of the 38th International Conference on Software Engineering Companion, ACM, pp. 744\u2013746 (2016)","DOI":"10.1145\/2889160.2892656"},{"key":"398_CR51","unstructured":"MGREffitas: In-the-wild ransomware protection comparative analysis 2016 q3. https:\/\/www.mrg-effitas.com\/wp-content\/uploads\/2016\/07\/Zemana_ransomware_detection.pdf"},{"key":"398_CR52","series-title":"PHI Series in Computer Science","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)"},{"key":"398_CR53","doi-asserted-by":"crossref","unstructured":"Moser, A., Kruegel, C., Kirda, E.: Limits of static analysis for malware detection. In: Twenty-Third Annual Computer Security Applications Conference, ACSAC 2007, IEEE, pp. 421\u2013430 (2007)","DOI":"10.1109\/ACSAC.2007.21"},{"issue":"1","key":"398_CR54","first-page":"111","volume":"9","author":"SK Muttoo","year":"2017","unstructured":"Muttoo, S.K., Badhani, S.: Android malware detection: state of the art. Int. J. Inf. Technol. 9(1), 111\u2013117 (2017)","journal-title":"Int. J. Inf. Technol."},{"key":"398_CR55","doi-asserted-by":"crossref","unstructured":"Oh, H.-S., Yeo, J.H., Moon, S.-M.: Bytecode-to-c ahead-of-time compilation for android Dalvik virtual machine. In: Proceedings of the 2015 Design, Automation and Test in Europe Conference and Exhibition, EDA Consortium, pp. 1048\u20131053 (2015)","DOI":"10.7873\/DATE.2015.0927"},{"issue":"5","key":"398_CR56","first-page":"25","volume":"30","author":"MD Preda","year":"2008","unstructured":"Preda, M.D., Christodorescu, M., Jha, S., Debray, S.: A semantics-based approach to malware detection. ACM Trans. Progr. Lang. Syst. (TOPLAS) 30(5), 25 (2008)","journal-title":"ACM Trans. Progr. Lang. Syst. (TOPLAS)"},{"issue":"6","key":"398_CR57","doi-asserted-by":"crossref","first-page":"855","DOI":"10.3233\/JCS-2009-0345","volume":"17","author":"MD Preda","year":"2009","unstructured":"Preda, M.D., Giacobazzi, R.: Semantics-based code obfuscation by abstract interpretation. J. Comput. Secur. 17(6), 855\u2013908 (2009)","journal-title":"J. Comput. Secur."},{"key":"398_CR58","doi-asserted-by":"crossref","unstructured":"Rastogi, V., Chen, Y., Jiang, X.: Droidchameleon: evaluating android anti-malware against transformation attacks. In: Proceedings of the 8th ACM SIGSAC Symposium on Information, Computer and Communications Security, ACM, pp. 329\u2013334 (2013)","DOI":"10.1145\/2484313.2484355"},{"issue":"1","key":"398_CR59","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1109\/TIFS.2013.2290431","volume":"9","author":"V Rastogi","year":"2014","unstructured":"Rastogi, V., Chen, Y., Jiang, X.: Catch me if you can: evaluating android anti-malware against transformation attacks. IEEE Trans. Inf. Forensics Secur. 9(1), 99\u2013108 (2014)","journal-title":"IEEE Trans. Inf. Forensics Secur."},{"issue":"5","key":"398_CR60","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1109\/JIOT.2014.2361608","volume":"1","author":"K Ren","year":"2014","unstructured":"Ren, K., Samarati, P., Gruteser, M., Ning, P., Liu, Y.: Guest editorial special issue on security for iot: the state of the art. IEEE Internet Things J. 1(5), 369\u2013371 (2014)","journal-title":"IEEE Internet Things J."},{"key":"398_CR61","doi-asserted-by":"crossref","unstructured":"Rieck, K., Holz, T., Willems, C., D\u00fcssel, P., Laskov, P.: Learning and classification of malware behavior. In: International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment, Springer, pp. 108\u2013125 (2008)","DOI":"10.1007\/978-3-540-70542-0_6"},{"issue":"4","key":"398_CR62","doi-asserted-by":"crossref","first-page":"639","DOI":"10.3233\/JCS-2010-0410","volume":"19","author":"K Rieck","year":"2011","unstructured":"Rieck, K., Trinius, P., Willems, C., Holz, T.: Automatic analysis of malware behavior using machine learning. J. Comput. Secur. 19(4), 639\u2013668 (2011)","journal-title":"J. Comput. Secur."},{"key":"398_CR63","unstructured":"RSA. Pkcs #1 v2.2: Rsa cryptography standard. https:\/\/www.emc.com\/collateral\/white-papers\/h11300-pkcs-1v2-2-rsa-cryptography-standard-wp.pdf (2012)"},{"key":"398_CR64","doi-asserted-by":"publisher","unstructured":"Saracino, A., Sgandurra, D., Dini, G., Martinelli, F.: MADAM: effective and efficient behavior-based android malware detection and prevention. IEEE Trans. Dependable Secure Comput. PP(99), 1\u20131 (2017). https:\/\/doi.org\/10.1109\/TDSC.2016.2536605","DOI":"10.1109\/TDSC.2016.2536605"},{"key":"398_CR65","volume-title":"Efficient Malware Detection Using Model-Checking","author":"F Song","year":"2001","unstructured":"Song, F., Touili, T.: Efficient Malware Detection Using Model-Checking. Springer, Berlin (2001)"},{"key":"398_CR66","doi-asserted-by":"crossref","unstructured":"Song, F., Touili, T.: Pommade: pushdown model-checking for malware detection. In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ACM (2013)","DOI":"10.1145\/2491411.2494599"},{"key":"398_CR67","volume-title":"Model-Checking for Android Malware Detection","author":"F Song","year":"2014","unstructured":"Song, F., Touili, T.: Model-Checking for Android Malware Detection. Springer, Berlin (2014)"},{"key":"398_CR68","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.pmcj.2016.03.003","volume":"32","author":"J Song","year":"2016","unstructured":"Song, J., Han, C., Wang, K., Zhao, J., Ranjan, R., Wang, L.: An integrated static detection and analysis framework for android. Pervasive Mob. Comput. 32, 1\u201311 (2016)","journal-title":"Pervasive Mob. Comput."},{"key":"398_CR69","unstructured":"Song, S., Kim, B., Lee, S.: The effective ransomware prevention technique using process monitoring on android platform. Mob. Inf. Syst. 2016, 1\u20139 (2016)"},{"key":"398_CR70","unstructured":"Sophos: The current state of ransomware. https:\/\/www.sophos.com\/en-us\/medialibrary\/PDFs\/technical"},{"key":"398_CR71","doi-asserted-by":"crossref","unstructured":"Spreitzenbarth, M., Echtler, F., Schreck, T., Freling, F.C., Hoffmann, J.: Mobilesandbox: looking deeper into android applications. In: 28th International ACM Symposium on Applied Computing (SAC), ACM (2013)","DOI":"10.1145\/2480362.2480701"},{"key":"398_CR72","first-page":"2","volume-title":"Concurrency: Theory, Language, And Architecture (LNCS)","author":"C Stirling","year":"1989","unstructured":"Stirling, C.: An introduction to modal and temporal logics for CCS. In: Yonezawa, A., Ito, T. (eds.) Concurrency: Theory, Language, And Architecture (LNCS), pp. 2\u201320. Springer, Berlin (1989)"},{"key":"398_CR73","doi-asserted-by":"crossref","unstructured":"Sung, A.H., Xu, J., Chavez, P., Mukkamala, S.: Static analyzer of vicious executables (save). In: 20th Annual Computer Security Applications Conference, IEEE, pp. 326\u2013334 (2004)","DOI":"10.1109\/CSAC.2004.37"},{"issue":"4","key":"398_CR74","first-page":"58","volume":"47","author":"DJ Tan","year":"2015","unstructured":"Tan, D.J., Chua, T.-W., Thing, V.L., et al.: Securing android: a survey, taxonomy, and challenges. ACM Comput. Surv. (CSUR) 47(4), 58 (2015)","journal-title":"ACM Comput. Surv. (CSUR)"},{"issue":"2","key":"398_CR75","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1109\/MSP.2007.45","volume":"5","author":"C Willems","year":"2007","unstructured":"Willems, C., Holz, T., Freiling, F.: Toward automated dynamic malware analysis using cwsandbox. IEEE Secur. Priv. 5(2), 32\u201339 (2007)","journal-title":"IEEE Secur. Priv."},{"key":"398_CR76","doi-asserted-by":"crossref","unstructured":"Yang, T., Yang, Y., Qian, K., Lo, D.C.-T., Qian, Y., Tao, L.: Automated detection and analysis for android ransomware. In: 7th International Symposium on Cyberspace Safety and Security (CSS), IEEE, pp. 1338\u20131343 (2015)","DOI":"10.1109\/HPCC-CSS-ICESS.2015.39"},{"key":"398_CR77","doi-asserted-by":"crossref","unstructured":"Zheng, M., Lee, P.P., Lui, J.C.: Adam: an automatic and extensible platform to stress test android anti-virus systems. In: International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment, Springer, pp. 82\u2013101 (2012)","DOI":"10.1007\/978-3-642-37300-8_5"}],"container-title":["International Journal of Information Security"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10207-017-0398-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-017-0398-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10207-017-0398-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,29]],"date-time":"2025-06-29T00:34:34Z","timestamp":1751157274000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10207-017-0398-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,19]]},"references-count":77,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2018,11]]}},"alternative-id":["398"],"URL":"https:\/\/doi.org\/10.1007\/s10207-017-0398-5","relation":{},"ISSN":["1615-5262","1615-5270"],"issn-type":[{"value":"1615-5262","type":"print"},{"value":"1615-5270","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,19]]}}}