{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T20:18:00Z","timestamp":1740169080783,"version":"3.37.3"},"reference-count":32,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/OAPA.html"}],"funder":[{"DOI":"10.13039\/501100011665","name":"Deanship of Scientific Research, King Saud University","doi-asserted-by":"publisher","award":["RGP-214"],"award-info":[{"award-number":["RGP-214"]}],"id":[{"id":"10.13039\/501100011665","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2019]]},"DOI":"10.1109\/access.2019.2895261","type":"journal-article","created":{"date-parts":[[2019,1,25]],"date-time":"2019-01-25T20:21:38Z","timestamp":1548447698000},"page":"16550-16560","source":"Crossref","is-referenced-by-count":11,"title":["Formal Analysis of Language-Based Android Security Using Theorem Proving Approach"],"prefix":"10.1109","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0993-5964","authenticated-orcid":false,"given":"Wilayat","family":"Khan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Muhammad","family":"Kamran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aakash","family":"Ahmad","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7023-7172","authenticated-orcid":false,"given":"Farrukh Aslam","family":"Khan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abdelouahid","family":"Derhab","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"doi-asserted-by":"publisher","key":"ref32","DOI":"10.1145\/2666356.2594299"},{"doi-asserted-by":"publisher","key":"ref31","DOI":"10.1109\/EuroSP.2016.16"},{"doi-asserted-by":"publisher","key":"ref30","DOI":"10.14722\/ndss.2015.23089"},{"key":"ref10","first-page":"40","article-title":"Android security permissions–can we trust them?","author":"orthacker","year":"2011","journal-title":"Proc Int Conf Secur Privacy Mobile Inf Commun Syst"},{"key":"ref11","first-page":"12","article-title":"Permission re-delegation: Attacks and defenses","volume":"6","author":"felt","year":"2011","journal-title":"Proc Usenix Secur Symp"},{"year":"2009","author":"chaudhuri","article-title":"SCanDroid: Automated security certification of Android applications","key":"ref12"},{"doi-asserted-by":"publisher","key":"ref13","DOI":"10.1145\/1554339.1554341"},{"doi-asserted-by":"publisher","key":"ref14","DOI":"10.1145\/1328897.1328443"},{"doi-asserted-by":"publisher","key":"ref15","DOI":"10.1007\/s10817-011-9225-2"},{"doi-asserted-by":"publisher","key":"ref16","DOI":"10.1145\/1411203.1411212"},{"year":"2008","author":"benton","article-title":"A mechanized bisimulation for the nu-calculus","key":"ref17"},{"doi-asserted-by":"publisher","key":"ref18","DOI":"10.1007\/978-3-642-17164-2_25"},{"year":"2011","author":"van cuijk","article-title":"Enforcing a fine-grained network policy in Android","key":"ref19"},{"key":"ref28","first-page":"1","article-title":"Towards formal model-based analysis and testing of Android’s security mechanisms","author":"betarte","year":"2017","journal-title":"Proc Latin American Computing Conf (CLEI)"},{"year":"2018","journal-title":"Android","key":"ref4"},{"key":"ref27","first-page":"485","article-title":"Verifying Android’s permission model","author":"betarte","year":"2015","journal-title":"Proc Int Colloq Theoret Aspects Comput"},{"year":"2018","journal-title":"Apple App Store","key":"ref3"},{"doi-asserted-by":"publisher","key":"ref6","DOI":"10.1145\/2046707.2046779"},{"key":"ref29","first-page":"5","article-title":"TaintDroid: An information-flow tracking system for realtime privacy monitoring on smartphones","volume":"32","author":"enck","year":"2010","journal-title":"ACM Trans Comput Syst"},{"year":"2018","journal-title":"Global Mobile OS Market Share 2009–2017 by Quarter","key":"ref5"},{"doi-asserted-by":"publisher","key":"ref8","DOI":"10.1109\/MSP.2009.26"},{"year":"2018","journal-title":"Application Fundamentals","key":"ref7"},{"year":"2018","journal-title":"Android Apps on Google Play","key":"ref2"},{"year":"2010","author":"vennon","article-title":"Android market: Threat analysis of the Android market","key":"ref9"},{"doi-asserted-by":"publisher","key":"ref1","DOI":"10.1002\/wcm.1203"},{"year":"2017","journal-title":"The Coq Proof Assistant","key":"ref20"},{"doi-asserted-by":"publisher","key":"ref22","DOI":"10.1109\/JSAC.2002.806121"},{"key":"ref21","volume":"2283","author":"nipkow","year":"2002","journal-title":"Isabelle\/HOL A Proof Assistant for Higher-Order Logic"},{"doi-asserted-by":"publisher","key":"ref24","DOI":"10.1186\/s13673-018-0144-7"},{"key":"ref23","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/3-540-44577-3_6","article-title":"A language-based approach to security","author":"schneider","year":"2001","journal-title":"Informatics"},{"doi-asserted-by":"publisher","key":"ref26","DOI":"10.1109\/SocialCom.2010.140"},{"doi-asserted-by":"publisher","key":"ref25","DOI":"10.1109\/ICWMC.2009.21"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/8600701\/08626096.pdf?arnumber=8626096","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,27]],"date-time":"2022-01-27T08:21:29Z","timestamp":1643271689000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8626096\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"references-count":32,"URL":"https:\/\/doi.org\/10.1109\/access.2019.2895261","relation":{},"ISSN":["2169-3536"],"issn-type":[{"type":"electronic","value":"2169-3536"}],"subject":[],"published":{"date-parts":[[2019]]}}}