{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:09:16Z","timestamp":1750219756754,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,29]],"date-time":"2023-10-29T00:00:00Z","timestamp":1698537600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,10,29]]},"DOI":"10.1145\/3623652.3623667","type":"proceedings-article","created":{"date-parts":[[2023,10,27]],"date-time":"2023-10-27T23:00:42Z","timestamp":1698447642000},"page":"29-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Automated Security Analysis for Real-World IoT Devices"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0642-6008","authenticated-orcid":false,"given":"Lelio","family":"Brun","sequence":"first","affiliation":[{"name":"National Institute of Informatics, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8300-4650","authenticated-orcid":false,"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-2480-0525","authenticated-orcid":false,"given":"Yasushi","family":"Ono","sequence":"additional","affiliation":[{"name":"Institute of Information Security, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-230X","authenticated-orcid":false,"given":"Taro","family":"Sekiyama","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,10,29]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2023. OP-TEE. Trusted Firmware."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127586"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360213"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","unstructured":"A. Armando D. Basin Y. Boichut Y. Chevalier L. Compagna J. Cuellar P.\u00a0Hankes Drielsma P.\u00a0C. He\u00e1m O. Kouchnarenko J. Mantovani S. M\u00f6dersheim D. von Oheimb M. Rusinowitch J. Santiago M. Turuani L. Vigan\u00f2 and L. Vigneron. 2005. The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In Computer Aided Verification(CAV\u201905) Kousha Etessami and Sriram\u00a0K. Rajamani (Eds.). Springer Berlin Heidelberg 281\u2013285. https:\/\/doi.org\/10.1007\/11513988_27","DOI":"10.1007\/11513988_27"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.26"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2001.930138"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.7"},{"key":"e_1_3_2_1_8_1","volume-title":"Proceedings of the 2018 USENIX Conference on Usenix Annual Technical Conference(USENIX ATC \u201918)","author":"Celik Berkay","year":"2018","unstructured":"Z.\u00a0Berkay Celik, Patrick McDaniel, and Gang Tan. 2018. SOTERIA: Automated IoT Safety and Security Analysis. In Proceedings of the 2018 USENIX Conference on Usenix Annual Technical Conference(USENIX ATC \u201918). USENIX Association, USA, 147\u2013158."},{"key":"e_1_3_2_1_9_1","volume-title":"31st USENIX Security Symposium (USENIX Security 22)","author":"Cheval Vincent","year":"2022","unstructured":"Vincent Cheval, Charlie Jacomme, Steve Kremer, and Robert K\u00fcnnemann. 2022. SAPIC+: Protocol Verifiers of the World, Unite!. In 31st USENIX Security Symposium (USENIX Security 22)(USENIX\u201922). USENIX Association, Boston, MA, 3935\u20133952."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00033"},{"key":"e_1_3_2_1_11_1","unstructured":"Cas Cremers David Basin Jannik Dreier Simon Meier Ralf Sasse and Benedikt Schmidt. 2021. Tamarin Prover."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23394"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134063"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/3489212.3489213"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"volume-title":"Foundations of Security Analysis and Design V: FOSAD 2007\/2008\/2009 Tutorial Lectures","author":"Escobar Santiago","key":"e_1_3_2_1_16_1","unstructured":"Santiago Escobar, Catherine Meadows, and Jos\u00e9 Meseguer. 2009. Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties. In Foundations of Security Analysis and Design V: FOSAD 2007\/2008\/2009 Tutorial Lectures, Alessandro Aldini, Gilles Barthe, and Roberto Gorrieri (Eds.). Springer, Berlin, Heidelberg, 1\u201350."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/IoTDI54339.2022.00017"},{"key":"e_1_3_2_1_18_1","unstructured":"Trusted Firmware. 2023. OP-TEE documentation. https:\/\/optee.readthedocs.io\/en\/3.22.0\/"},{"key":"e_1_3_2_1_19_1","unstructured":"GlobalPlatform. 2010. TEE Client API Specification. https:\/\/globalplatform.org\/specs-library\/tee-client-api-specification\/"},{"key":"e_1_3_2_1_20_1","unstructured":"GlobalPlatform. 2020. Secure Channel Protocol \u201903\u2019. https:\/\/globalplatform.org\/specs-library\/secure-channel-protocol-03-amendment-d-v1-2\/"},{"key":"e_1_3_2_1_21_1","unstructured":"GlobalPlatform. 2021. TEE Internal Core API Specification. https:\/\/globalplatform.org\/specs-library\/tee-internal-core-api-specification\/"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3577020"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2020.107233"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.16"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3134600.3134624"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.38"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.18"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"e_1_3_2_1_29_1","volume-title":"Undecidability of Bounded Security Protocols. In Workshop on Formal Methods and Security Protocols.","author":"Mitchell J","year":"1999","unstructured":"J Mitchell, A Scedrov, N Durgin, and P Lincoln. 1999. Undecidability of Bounded Security Protocols. In Workshop on Formal Methods and Security Protocols."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/CIC.2016.065"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3281411.3281440"},{"key":"e_1_3_2_1_32_1","unstructured":"NXP. 2021. SE050 APDU Specification. https:\/\/www.nxp.com\/docs\/en\/application-note\/AN12413.pdf"},{"key":"e_1_3_2_1_33_1","volume-title":"Proceedings of the 14th Conference on USENIX Security Symposium -","volume":"8","author":"Ou Xinming","year":"2005","unstructured":"Xinming Ou, Sudhakar Govindavajhala, and Andrew\u00a0W. Appel. 2005. MulVAL: A Logic-Based Network Security Analyzer. In Proceedings of the 14th Conference on USENIX Security Symposium - Volume 14(SSYM\u201905). USENIX Association, USA, 8."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","unstructured":"Mohamed Sabt Mohammed Achemlal and Abdelmadjid Bouabdallah. 2015. Trusted Execution Environment: What It Is and What It Is Not. In 2015 IEEE Trustcom\/BigDataSE\/ISPA(TrustCom\u201915 Vol.\u00a01). 57\u201364. https:\/\/doi.org\/10.1109\/Trustcom.2015.357","DOI":"10.1109\/Trustcom.2015.357"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.25"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Carlton Shepherd Ghada Arfaoui Iakovos Gurulian Robert\u00a0P. Lee Konstantinos Markantonakis Raja\u00a0Naeem Akram Damien Sauveron and Emmanuel Conchon. 2016. Secure and Trusted Execution: Past Present and Future - A Critical Review in the Context of the Internet of Things and Cyber-Physical Systems. In 2016 IEEE Trustcom\/BigDataSE\/ISPA(TrustCom\u201916). 168\u2013177. https:\/\/doi.org\/10.1109\/TrustCom.2016.0060","DOI":"10.1109\/TrustCom.2016.0060"},{"key":"e_1_3_2_1_37_1","unstructured":"The\u00a0Tamarin Team. 2023. Tamarin-Prover Manual. https:\/\/tamarin-prover.github.io\/manual\/master\/tex\/tamarin-manual.pdf"},{"key":"e_1_3_2_1_38_1","unstructured":"Atmark Techno. 2023. Armadillo-IoT\u30b2\u30fc\u30c8\u30a6\u30a7\u30a4 G4 \u30bb\u30ad\u30e5\u30ea\u30c6\u30a3\u30ac\u30a4\u30c9. https:\/\/manual.atmark-techno.com\/armadillo-iot-g4\/armadillo-base-os-security-guide_ja-1.3.1\/"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2014.7001385"}],"event":{"name":"HASP '23: Hardware and Architectural Support for Security and Privacy 2023","acronym":"HASP '23","location":"Toronto Canada"},"container-title":["Proceedings of the 12th International Workshop on Hardware and Architectural Support for Security and Privacy"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3623652.3623667","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3623652.3623667","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:00Z","timestamp":1750178220000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3623652.3623667"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,29]]},"references-count":39,"alternative-id":["10.1145\/3623652.3623667","10.1145\/3623652"],"URL":"https:\/\/doi.org\/10.1145\/3623652.3623667","relation":{},"subject":[],"published":{"date-parts":[[2023,10,29]]},"assertion":[{"value":"2023-10-29","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}