{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:20:15Z","timestamp":1771024815153,"version":"3.50.1"},"reference-count":71,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100000082","name":"National Science Foundation of the United States","doi-asserted-by":"publisher","award":["DGE-1723707"],"award-info":[{"award-number":["DGE-1723707"]}],"id":[{"id":"10.13039\/100000082","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000104","name":"NASA","doi-asserted-by":"publisher","award":["NNX15AJ20H"],"award-info":[{"award-number":["NNX15AJ20H"]}],"id":[{"id":"10.13039\/100000104","id-type":"DOI","asserted-by":"publisher"}]},{"name":"anonymous reviewers for their valuable comments and helpful suggestions. We thank Khalid Alghamdi for his contribution to the conference version of this manuscript"},{"name":"proofreading of the early draft of this manuscript."}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Access"],"published-print":{"date-parts":[[2021]]},"DOI":"10.1109\/access.2019.2961918","type":"journal-article","created":{"date-parts":[[2019,12,25]],"date-time":"2019-12-25T00:34:38Z","timestamp":1577234078000},"page":"27038-27050","source":"Crossref","is-referenced-by-count":18,"title":["Iotverif: Automatic Verification of SSL\/TLS Certificate for IoT Applications"],"prefix":"10.1109","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6011-1998","authenticated-orcid":false,"given":"Anyi","family":"Liu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7721-0450","authenticated-orcid":false,"given":"Ali","family":"Alqazzaz","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5379-6311","authenticated-orcid":false,"given":"Hua","family":"Ming","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6180-0488","authenticated-orcid":false,"given":"Balakrishnan","family":"Dharmalingam","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref71","article-title":"On CTL model checking of the MQTT IoT protocol using the sweep-line method","author":"rodriguez","year":"2019","journal-title":"Proc Int Workshop Petri Nets Softw Eng"},{"key":"ref70","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21554-4_1"},{"key":"ref39","author":"pi","year":"2017","journal-title":"Raspberry Pi—Teach Learn and Make With Raspberry Pi"},{"key":"ref38","year":"2017","journal-title":"Arduino Yún"},{"key":"ref33","year":"2019","journal-title":"Google Play"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2593929.2593932"},{"key":"ref30","year":"2017","journal-title":"Ui\/application Exerciser Monkey"},{"key":"ref37","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","article-title":"NuSMV 2: An opensource tool for symbolic model checking","author":"cimatti","year":"2002","journal-title":"Proc 14th Int Conf Comput Aided Verification"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594299"},{"key":"ref35","year":"2017","journal-title":"Google play crawler"},{"key":"ref34","year":"2019","journal-title":"Amazon Appstore"},{"key":"ref60","author":"holzmann","year":"2011","journal-title":"The SPIN Model Checker Primer and Reference Manual"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1145\/1044731.1044735"},{"key":"ref61","first-page":"372","article-title":"CADP 2010: A toolbox for the construction and analysis of distributed processes","author":"garavel","year":"2011","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref63","first-page":"3","article-title":"Security protocol verification: Symbolic and computational models","author":"blanchet","year":"2012","journal-title":"Proc 1st Int Conf Princ Secur Trust"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/2889160.2889258"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(93)90094-K"},{"key":"ref27","year":"2017","journal-title":"Android Tcpdump"},{"key":"ref65","author":"blanchet","year":"2019","journal-title":"ProVerif Cryptographic protocol verifier in the formal model"},{"key":"ref66","doi-asserted-by":"crossref","first-page":"414","DOI":"10.1007\/978-3-540-70545-1_38","article-title":"The scyther tool: Verification, falsification, and analysis of security protocols","author":"cremers","year":"2008","journal-title":"Computer Aided Verification"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2857705.2857739"},{"key":"ref67","doi-asserted-by":"publisher","DOI":"10.1109\/TIFS.2019.2898841"},{"key":"ref68","first-page":"193","article-title":"Protocol state fuzzing of TLS implementations","author":"de ruiter","year":"2015","journal-title":"Proc 24th USENIX Secur Symp"},{"key":"ref69","first-page":"203","article-title":"ScriptGen: An automated script generation tool for honeyd","author":"leita","year":"2006","journal-title":"Proc 21st Annu Comput Secur Appl Conf (ACSAC)"},{"key":"ref2","year":"2019","journal-title":"The Future of IoT 4 Predictions About the Internet of Things"},{"key":"ref1","volume":"29","author":"vermesan","year":"2014","journal-title":"Internet of Things - From Research and Innovation to Market Deployment"},{"key":"ref20","author":"yuan","year":"2017","journal-title":"Getting to know MQTT"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.17487\/rfc7457"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.17487\/rfc5280"},{"key":"ref24","author":"tung","year":"2019","journal-title":"Google Builds List of Untrusted Digital Certificate Suppliers"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.17487\/rfc5746"},{"key":"ref26","year":"2017","journal-title":"MITM Tool and Framework"},{"key":"ref25","year":"2019","journal-title":"MyMQTT"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1145\/3038912.3052674"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/3292674"},{"key":"ref59","first-page":"854","article-title":"Linear temporal logic and linear dynamic logic on finite traces","author":"de giacomo","year":"2013","journal-title":"Proc 23rd Int Joint Conf Artif Intell"},{"key":"ref58","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.42"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1007\/s11276-014-0761-7"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1109\/JIOT.2017.2767291"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1109\/CSCS.2017.101"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1016\/j.adhoc.2015.01.006"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2015.2388550"},{"key":"ref52","author":"geng","year":"2017","journal-title":"Networking Protocols and Standards for Internet of Things"},{"key":"ref10","year":"2016","journal-title":"CVE-2016-2183"},{"key":"ref11","year":"2012","journal-title":"CVE-2012-4929"},{"key":"ref40","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2557833.2560576","article-title":"Execution and property specifications for JPF-Android","volume":"39","author":"van der merwe","year":"2014","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"key":"ref12","year":"2014","journal-title":"Cve-2014-0160"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382205"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2014.23205"},{"key":"ref15","author":"mettler","year":"2014","journal-title":"SSL vulnerabilities who listens when android applications talk?"},{"key":"ref16","author":"montelibano","year":"2015","journal-title":"How We Discovered Thousands of Vulnerable Android Apps in One Day"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/3176258.3176334"},{"key":"ref18","year":"2019","journal-title":"The Simple Text Oriented Messaging Protocol"},{"key":"ref19","year":"2019","journal-title":"IoT Developer Survey 2019 Results"},{"key":"ref4","year":"2014"},{"key":"ref3","year":"2017","journal-title":"MQTT V3 1 Protocol Specification"},{"key":"ref6","year":"2019","journal-title":"Eclipse Project"},{"key":"ref5","year":"2017","journal-title":"Java Message Service"},{"key":"ref8","year":"2014","journal-title":"CVE-2014-1295"},{"key":"ref7","year":"2017","journal-title":"Azure IoT SuiteIoT Cloud Solution"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393666"},{"key":"ref9","year":"2014","journal-title":"CVE-2014-3566"},{"key":"ref46","author":"cab\u00e9","year":"2018","journal-title":"Key Trends From the IoT Developer Survey"},{"key":"ref45","article-title":"Dynamic taint analysis for automatic detection, analysis, and signature generation of exploits on commodity software","author":"newsome","year":"2005","journal-title":"Proc Symp Network and Distributed System Security"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/2594368.2594390"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/2351676.2351717"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814303"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814282"},{"key":"ref44","first-page":"393","article-title":"Taintdroid: An information-flow tracking system for realtime privacy monitoring on smartphones","author":"enck","year":"2010","journal-title":"Proc 9th USENIX Conf Oper Syst Design Implement"},{"key":"ref43","year":"2017","journal-title":"CloudMQTT—A Globally Distributed MQTT Broker"}],"container-title":["IEEE Access"],"original-title":[],"link":[{"URL":"https:\/\/ieeexplore.ieee.org\/ielam\/6287639\/9312710\/8941131-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6287639\/9312710\/08941131.pdf?arnumber=8941131","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,8]],"date-time":"2022-04-08T18:53:42Z","timestamp":1649444022000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8941131\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"references-count":71,"URL":"https:\/\/doi.org\/10.1109\/access.2019.2961918","relation":{},"ISSN":["2169-3536"],"issn-type":[{"value":"2169-3536","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]}}}