{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T08:43:57Z","timestamp":1773305037646,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,7,10]],"date-time":"2023-07-10T00:00:00Z","timestamp":1688947200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DsbDtech, Engineering and Physical Sciences Research Council (EPSRC)","award":["Grants EP\/R012598\/1 and EP\/V000454\/1"],"award-info":[{"award-number":["Grants EP\/R012598\/1 and EP\/V000454\/1"]}]},{"name":"University of Bahrain"},{"DOI":"10.13039\/501100002409","name":"TimeTrust project, UK?s National Cyber Security Centre (NCSC)","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002409","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,7,10]]},"DOI":"10.1145\/3579856.3582812","type":"proceedings-article","created":{"date-parts":[[2023,7,5]],"date-time":"2023-07-05T14:52:13Z","timestamp":1688568733000},"page":"218-231","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Symbolic modelling of remote attestation protocols for device and app integrity on Android"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4959-6832","authenticated-orcid":false,"given":"Abdulla","family":"Aldoseri","sequence":"first","affiliation":[{"name":"School of Computer Science, University of Birmingham, UK and College of information technology, computer science department, Univerity oif Bahrain, Bahrain"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9381-1368","authenticated-orcid":false,"given":"Tom","family":"Chothia","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Birmingham, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3210-4504","authenticated-orcid":false,"given":"Jose","family":"Moreira","sequence":"additional","affiliation":[{"name":"Valory AG, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8524-5282","authenticated-orcid":false,"given":"David","family":"Oswald","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Birmingham, UK"}]}],"member":"320","published-online":{"date-parts":[[2023,7,10]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"key":"e_1_3_2_1_2_1","unstructured":"Abdulla Aldoseri Tom Chothia Jos\u00e9 Moreira and David Oswald. 2023. Android Remote attestation models repository. https:\/\/github.com\/Buhadod\/AndroidRemoteAttestationModels  Abdulla Aldoseri Tom Chothia Jos\u00e9 Moreira and David Oswald. 2023. Android Remote attestation models repository. https:\/\/github.com\/Buhadod\/AndroidRemoteAttestationModels"},{"key":"e_1_3_2_1_3_1","unstructured":"Android. 2019. About Dynamic Delivery. https:\/\/developer.android.com\/studio\/projects\/dynamic-delivery (Accessed on 12\/01\/2019).  Android. 2019. About Dynamic Delivery. https:\/\/developer.android.com\/studio\/projects\/dynamic-delivery (Accessed on 12\/01\/2019)."},{"key":"e_1_3_2_1_4_1","unstructured":"Android. 2021. Application Signing | Android Open Source Project. https:\/\/source.android.com\/security\/apksigning (Accessed on 11\/24\/2021).  Android. 2021. Application Signing | Android Open Source Project. https:\/\/source.android.com\/security\/apksigning (Accessed on 11\/24\/2021)."},{"key":"e_1_3_2_1_5_1","unstructured":"Android. 2021. Locking\/Unlocking the Bootloader. https:\/\/source.android.com\/devices\/bootloader\/locking_unlocking (Accessed on 11\/25\/2021).  Android. 2021. Locking\/Unlocking the Bootloader. https:\/\/source.android.com\/devices\/bootloader\/locking_unlocking (Accessed on 11\/25\/2021)."},{"key":"e_1_3_2_1_6_1","unstructured":"Android. 2021. Shrink obfuscate and optimize your app. https:\/\/developer.android.com\/studio\/build\/shrink-code (Accessed on 11\/26\/2021).  Android. 2021. Shrink obfuscate and optimize your app. https:\/\/developer.android.com\/studio\/build\/shrink-code (Accessed on 11\/26\/2021)."},{"key":"e_1_3_2_1_7_1","unstructured":"Android. 2021. Trusty TEE. https:\/\/source.android.com\/security\/trusty  Android. 2021. Trusty TEE. https:\/\/source.android.com\/security\/trusty"},{"key":"e_1_3_2_1_8_1","unstructured":"Android. 2021. Verified Boot | Android Open Source Project. https:\/\/source.android.com\/security\/verifiedboot (Accessed on 11\/25\/2021).  Android. 2021. Verified Boot | Android Open Source Project. https:\/\/source.android.com\/security\/verifiedboot (Accessed on 11\/25\/2021)."},{"key":"e_1_3_2_1_9_1","unstructured":"Android. 2021. Verifying hardware-backed key pairs with Key Attestation. https:\/\/developer.android.com\/training\/articles\/security-key-attestation  Android. 2021. Verifying hardware-backed key pairs with Key Attestation. https:\/\/developer.android.com\/training\/articles\/security-key-attestation"},{"key":"e_1_3_2_1_10_1","unstructured":"Android. 2022. Compatibility Test Suite | Android Open Source Project. https:\/\/source.android.com\/compatibility\/cts (Accessed on 05\/28\/2022).  Android. 2022. Compatibility Test Suite | Android Open Source Project. https:\/\/source.android.com\/compatibility\/cts (Accessed on 05\/28\/2022)."},{"key":"e_1_3_2_1_11_1","unstructured":"Android. 2022. Key and ID Attestation. https:\/\/source.android.com\/docs\/security\/keystore\/attestation (Accessed on 09\/01\/2022).  Android. 2022. Key and ID Attestation. https:\/\/source.android.com\/docs\/security\/keystore\/attestation (Accessed on 09\/01\/2022)."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660350"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2016.28"},{"key":"e_1_3_2_1_14_1","unstructured":"David Basin Cas Cremers Jannik Dreier Simon Meier Ralf Sasse and Benedikt Schmidt. 2021. Tamarin Prover (v. 1.6.1). https:\/\/tamarin-prover.github.io  David Basin Cas Cremers Jannik Dreier Simon Meier Ralf Sasse and Benedikt Schmidt. 2021. Tamarin Prover (v. 1.6.1). https:\/\/tamarin-prover.github.io"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jisa.2020.102463"},{"key":"e_1_3_2_1_16_1","unstructured":"CENSUS. 2017. Examining the value of SafetyNet Attestation as an Application Integrity Security Control. https:\/\/census-labs.com\/news\/2017\/11\/17\/examining-the-value-of-safetynet-attestation-as-an-application-integrity-security-control\/ (Accessed on 08\/15\/2019).  CENSUS. 2017. Examining the value of SafetyNet Attestation as an Application Integrity Security Control. https:\/\/census-labs.com\/news\/2017\/11\/17\/examining-the-value-of-safetynet-attestation-as-an-application-integrity-security-control\/ (Accessed on 08\/15\/2019)."},{"key":"e_1_3_2_1_17_1","volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Chen Zitai","year":"2021","unstructured":"Zitai Chen , Georgios Vasilakis , Kit Murdock , Edward Dean , David Oswald , and Flavio\u00a0 D Garcia . 2021 . { VoltPillager} : Hardware-based fault injection attacks against Intel { SGX} Enclaves using the { SVID} voltage scaling interface . In 30th USENIX Security Symposium (USENIX Security 21) . 699\u2013716. Zitai Chen, Georgios Vasilakis, Kit Murdock, Edward Dean, David Oswald, and Flavio\u00a0D Garcia. 2021. { VoltPillager} : Hardware-based fault injection attacks against Intel { SGX} Enclaves using the { SVID} voltage scaling interface. In 30th USENIX Security Symposium (USENIX Security 21). 699\u2013716."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-011-0124-7"},{"key":"e_1_3_2_1_19_1","unstructured":"R.\u00a0Housley W.\u00a0Polk D.\u00a0Cooper S. Santesson S. Farrell S.\u00a0Boeyen. 2008. rfc5280. https:\/\/datatracker.ietf.org\/doc\/html\/rfc5280 (Accessed on 11\/28\/2021).  R.\u00a0Housley W.\u00a0Polk D.\u00a0Cooper S. Santesson S. Farrell S.\u00a0Boeyen. 2008. rfc5280. https:\/\/datatracker.ietf.org\/doc\/html\/rfc5280 (Accessed on 11\/28\/2021)."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3460120.3484532"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_22_1","volume-title":"Android code protection via obfuscation techniques: past, present and future directions. arXiv preprint arXiv:1611.10231","author":"Faruki Parvez","year":"2016","unstructured":"Parvez Faruki , Hossein Fereidooni , Vijay Laxmi , Mauro Conti , and Manoj Gaur . 2016. Android code protection via obfuscation techniques: past, present and future directions. arXiv preprint arXiv:1611.10231 ( 2016 ). Parvez Faruki, Hossein Fereidooni, Vijay Laxmi, Mauro Conti, and Manoj Gaur. 2016. Android code protection via obfuscation techniques: past, present and future directions. arXiv preprint arXiv:1611.10231 (2016)."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-91859-0_9"},{"key":"e_1_3_2_1_24_1","unstructured":"Google. 2019. Android keystore system. https:\/\/developer.android.com\/training\/articles\/keystore (Accessed on 09\/16\/2019).  Google. 2019. Android keystore system. https:\/\/developer.android.com\/training\/articles\/keystore (Accessed on 09\/16\/2019)."},{"key":"e_1_3_2_1_25_1","unstructured":"Google. 2019. SafetyNet Attestation API. https:\/\/developer.android.com\/training\/safetynet\/attestation (Accessed on 07\/23\/2019).  Google. 2019. SafetyNet Attestation API. https:\/\/developer.android.com\/training\/safetynet\/attestation (Accessed on 07\/23\/2019)."},{"key":"e_1_3_2_1_26_1","unstructured":"Guardsquare nv. 2019. DexGuard: Android obfuscation and runtime-self protection (RASP). https:\/\/www.guardsquare.com\/en\/products\/dexguard  Guardsquare nv. 2019. DexGuard: Android obfuscation and runtime-self protection (RASP). https:\/\/www.guardsquare.com\/en\/products\/dexguard"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3458864.3466627"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.16"},{"key":"e_1_3_2_1_29_1","first-page":"54","article-title":"Android Application Protection against Static Reverse Engineering based on Multidexing.J","volume":"6","author":"Kim Nak\u00a0Young","year":"2016","unstructured":"Nak\u00a0Young Kim , Jaewoo Shim , Seong-je Cho, Minkyu Park , and Sangchul Han . 2016 . Android Application Protection against Static Reverse Engineering based on Multidexing.J . Internet Serv. Inf. Secur. 6 , 4 (2016), 54 \u2013 64 . Nak\u00a0Young Kim, Jaewoo Shim, Seong-je Cho, Minkyu Park, and Sangchul Han. 2016. Android Application Protection against Static Reverse Engineering based on Multidexing.J. Internet Serv. Inf. Secur. 6, 4 (2016), 54\u201364.","journal-title":"Internet Serv. Inf. Secur."},{"key":"e_1_3_2_1_30_1","unstructured":"John Kozyrakis. 2015. SafetyNet: Google\u2019s tamper detection for Android. https:\/\/koz.io\/inside-safetynet\/ (Accessed on 08\/05\/2019).  John Kozyrakis. 2015. SafetyNet: Google\u2019s tamper detection for Android. https:\/\/koz.io\/inside-safetynet\/ (Accessed on 08\/05\/2019)."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-160556"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046711"},{"key":"e_1_3_2_1_33_1","first-page":"40","article-title":"An Android Application Protection Scheme against Dynamic Reverse Engineering Attacks","volume":"7","author":"Lim Kyeonghwan","year":"2016","unstructured":"Kyeonghwan Lim , Younsik Jeong , Seong-je Cho, Minkyu Park , and Sangchul Han . 2016 . An Android Application Protection Scheme against Dynamic Reverse Engineering Attacks . JoWUA 7 , 3 (2016), 40 \u2013 52 . Kyeonghwan Lim, Younsik Jeong, Seong-je Cho, Minkyu Park, and Sangchul Han. 2016. An Android Application Protection Scheme against Dynamic Reverse Engineering Attacks. JoWUA 7, 3 (2016), 40\u201352.","journal-title":"JoWUA"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_3_2_1_35_1","volume-title":"Preventing piracy, reverse engineering, and tampering. computer 36, 7","author":"Naumovich Gleb","year":"2003","unstructured":"Gleb Naumovich and Nasir Memon . 2003. Preventing piracy, reverse engineering, and tampering. computer 36, 7 ( 2003 ), 64\u201371. Gleb Naumovich and Nasir Memon. 2003. Preventing piracy, reverse engineering, and tampering. computer 36, 7 (2003), 64\u201371."},{"key":"e_1_3_2_1_36_1","volume-title":"Android rooting: An arms race between evasion and detection. Security and Communication Networks 2017","author":"Nguyen\u00a0Vu Long","year":"2017","unstructured":"Long Nguyen\u00a0Vu , Ngoc-Tu Chau , Seongeun Kang , and Souhwan Jung . 2017. Android rooting: An arms race between evasion and detection. Security and Communication Networks 2017 ( 2017 ). Long Nguyen\u00a0Vu, Ngoc-Tu Chau, Seongeun Kang, and Souhwan Jung. 2017. Android rooting: An arms race between evasion and detection. Security and Communication Networks 2017 (2017)."},{"key":"e_1_3_2_1_37_1","volume-title":"VRASED: A Verified Hardware\/Software Co-Design for Remote Attestation. In 28th USENIX Security Symposium (USENIX Security 19)","author":"De\u00a0Oliveira Nunes Ivan","year":"2019","unstructured":"Ivan De\u00a0Oliveira Nunes , Karim Eldefrawy , Norrathep Rattanavipanon , Michael Steiner , and Gene Tsudik . 2019 . VRASED: A Verified Hardware\/Software Co-Design for Remote Attestation. In 28th USENIX Security Symposium (USENIX Security 19) . 1429\u20131446. Ivan De\u00a0Oliveira Nunes, Karim Eldefrawy, Norrathep Rattanavipanon, Michael Steiner, and Gene Tsudik. 2019. VRASED: A Verified Hardware\/Software Co-Design for Remote Attestation. In 28th USENIX Security Symposium (USENIX Security 19). 1429\u20131446."},{"key":"e_1_3_2_1_38_1","unstructured":"OWASP. 2017. Mobile Top 10 2016: M8: Code Tampering. https:\/\/www.owasp.org\/index.php\/Mobile_Top_10_2016-M8-Code_Tampering  OWASP. 2017. Mobile Top 10 2016: M8: Code Tampering. https:\/\/www.owasp.org\/index.php\/Mobile_Top_10_2016-M8-Code_Tampering"},{"key":"e_1_3_2_1_39_1","unstructured":"Shiv Sahni. 2019. Android Key Attestation. What the heck is Android Key\u2026 | by Shiv Sahni | InfoSec Write-ups. https:\/\/infosecwriteups.com\/android-key-attestation-581da703ac16 (Accessed on 02\/13\/2022).  Shiv Sahni. 2019. Android Key Attestation. What the heck is Android Key\u2026 | by Shiv Sahni | InfoSec Write-ups. https:\/\/infosecwriteups.com\/android-key-attestation-581da703ac16 (Accessed on 02\/13\/2022)."},{"key":"e_1_3_2_1_40_1","volume-title":"Knox: Device Health Attestation. https:\/\/docs.samsungknox.com\/whitepapers\/knox-platform\/attestation.htm (Accessed on 07\/31\/2019).","year":"2019","unstructured":"Samsung. 2019 . Knox: Device Health Attestation. https:\/\/docs.samsungknox.com\/whitepapers\/knox-platform\/attestation.htm (Accessed on 07\/31\/2019). Samsung. 2019. Knox: Device Health Attestation. https:\/\/docs.samsungknox.com\/whitepapers\/knox-platform\/attestation.htm (Accessed on 07\/31\/2019)."},{"key":"e_1_3_2_1_41_1","volume-title":"Knox: Root of Trust. https:\/\/docs.samsungknox.com\/whitepapers\/knox-platform\/hardware-backed-root-of-trust.htm","year":"2019","unstructured":"Samsung. 2019 . Knox: Root of Trust. https:\/\/docs.samsungknox.com\/whitepapers\/knox-platform\/hardware-backed-root-of-trust.htm Samsung. 2019. Knox: Root of Trust. https:\/\/docs.samsungknox.com\/whitepapers\/knox-platform\/hardware-backed-root-of-trust.htm"},{"key":"e_1_3_2_1_42_1","unstructured":"Samsung. 2021. Enhanced Attestation (v3). https:\/\/docs.samsungknox.com\/dev\/knox-attestation\/about-attestation.htm (Accessed on 11\/23\/2021).  Samsung. 2021. Enhanced Attestation (v3). https:\/\/docs.samsungknox.com\/dev\/knox-attestation\/about-attestation.htm (Accessed on 11\/23\/2021)."},{"key":"e_1_3_2_1_43_1","unstructured":"Samsung. 2021. Real-time Kernel Protection. https:\/\/docs.samsungknox.com\/admin\/whitepaper\/kpe\/real-time-kernel-protection.htm  Samsung. 2021. Real-time Kernel Protection. https:\/\/docs.samsungknox.com\/admin\/whitepaper\/kpe\/real-time-kernel-protection.htm"},{"key":"e_1_3_2_1_44_1","volume-title":"Tutorial: Attestation (v2). https:\/\/docs.samsungknox.com\/dev\/knox-attestation\/tutorial-v2.htm (Accessed on 11\/23\/2021).","year":"2021","unstructured":"Samsung. 2021 . Tutorial: Attestation (v2). https:\/\/docs.samsungknox.com\/dev\/knox-attestation\/tutorial-v2.htm (Accessed on 11\/23\/2021). Samsung. 2021. Tutorial: Attestation (v2). https:\/\/docs.samsungknox.com\/dev\/knox-attestation\/tutorial-v2.htm (Accessed on 11\/23\/2021)."},{"key":"e_1_3_2_1_45_1","unstructured":"Samsung. 2022. Knox Attestation. https:\/\/docs.samsungknox.com\/dev\/knox-attestation\/about-attestation.htm (Accessed on 08\/05\/2022).  Samsung. 2022. Knox Attestation. https:\/\/docs.samsungknox.com\/dev\/knox-attestation\/about-attestation.htm (Accessed on 08\/05\/2022)."},{"key":"e_1_3_2_1_46_1","volume-title":"Pioneer: Verifying Code Integrity and Enforcing Untampered Code Execution on Legacy Systems.","author":"Seshadri Arvind","year":"2005","unstructured":"Arvind Seshadri , Mark Luk , Elaine Shi , Adrian Perrig , and Leendert van Doorn\u00a0Pradeep Khosla . 2005 . Pioneer: Verifying Code Integrity and Enforcing Untampered Code Execution on Legacy Systems. (2005). Arvind Seshadri, Mark Luk, Elaine Shi, Adrian Perrig, and Leendert van Doorn\u00a0Pradeep Khosla. 2005. Pioneer: Verifying Code Integrity and Enforcing Untampered Code Execution on Legacy Systems. (2005)."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPADS.2017.00015"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2808117.2808126"},{"key":"e_1_3_2_1_49_1","volume-title":"International Symposium on Foundations and Practice of Security. Springer, 189\u2013204","author":"Tanner Simon","year":"2019","unstructured":"Simon Tanner , Ilian Vogels , and Roger Wattenhofer . 2019 . Protecting android apps from repackaging using native code . In International Symposium on Foundations and Practice of Security. Springer, 189\u2013204 . Simon Tanner, Ilian Vogels, and Roger Wattenhofer. 2019. Protecting android apps from repackaging using native code. In International Symposium on Foundations and Practice of Security. Springer, 189\u2013204."},{"key":"e_1_3_2_1_50_1","unstructured":"Jin-Hyuk\u00a0Jung Yuxue\u00a0Piao and Jeong\u00a0Hyun Yi. 2016. Server-based code obfuscation scheme for APK tamper detection. In Security Comm. Networks. https:\/\/onlinelibrary.wiley.com\/doi\/pdfdirect\/10.1002\/sec.936 (Accessed on 11\/26\/2021).  Jin-Hyuk\u00a0Jung Yuxue\u00a0Piao and Jeong\u00a0Hyun Yi. 2016. Server-based code obfuscation scheme for APK tamper detection. In Security Comm. Networks. https:\/\/onlinelibrary.wiley.com\/doi\/pdfdirect\/10.1002\/sec.936 (Accessed on 11\/26\/2021)."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-69471-9_27"}],"event":{"name":"ASIA CCS '23: ACM ASIA Conference on Computer and Communications Security","location":"Melbourne VIC Australia","acronym":"ASIA CCS '23","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the ACM Asia Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3579856.3582812","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:51:27Z","timestamp":1750182687000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3579856.3582812"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,7,10]]},"references-count":51,"alternative-id":["10.1145\/3579856.3582812","10.1145\/3579856"],"URL":"https:\/\/doi.org\/10.1145\/3579856.3582812","relation":{},"subject":[],"published":{"date-parts":[[2023,7,10]]},"assertion":[{"value":"2023-07-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}