{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T15:56:52Z","timestamp":1762876612501,"version":"3.45.0"},"reference-count":47,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Internet of Things"],"published-print":{"date-parts":[[2019,12]]},"DOI":"10.1016\/j.iot.2019.100092","type":"journal-article","created":{"date-parts":[[2019,8,18]],"date-time":"2019-08-18T09:29:34Z","timestamp":1566120574000},"page":"100092","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":5,"special_numbering":"C","title":["Deriving event data sharing in IoT systems using formal modelling and analysis"],"prefix":"10.1016","volume":"8","author":[{"given":"Paul","family":"Fremantle","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Aziz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/j.iot.2019.100092_bib0001","series-title":"How the Next Evolution of the Internet is Changing Everything, Whitepaper, Cisco Internet Business Solutions Group (IBSG)","article-title":"The internet of things","author":"Evans","year":"2011"},{"issue":"2","key":"10.1016\/j.iot.2019.100092_bib0002","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1109\/TDSC.2005.26","article-title":"Remote physical device fingerprinting","volume":"2","author":"Kohno","year":"2005","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"10.1016\/j.iot.2019.100092_bib0003","unstructured":"J. Wei, DDoS on Internet of Things\u2013a big alarm for the future, 2016, (http:\/\/www.cs.tufts.edu\/comp\/116\/archive\/fall2016\/jwei.pdf)."},{"key":"10.1016\/j.iot.2019.100092_bib0004","unstructured":"N.V. Database, Cve-2014-9222, 2014, (https:\/\/web.nvd.nist.gov\/view\/vuln\/detail?vulnId=CVE-2014-9222) (Accessed on 02\/02\/2017)."},{"key":"10.1016\/j.iot.2019.100092_bib0005","series-title":"2014 International Workshop on Secure Internet of Things","first-page":"10","article-title":"Federated identity and access management for the internet of things","author":"Fremantle","year":"2014"},{"key":"10.1016\/j.iot.2019.100092_bib0006","series-title":"The Semantic Web: ESWC 2015 Satellite Events","first-page":"367","article-title":"Web api management meets the internet of things","author":"Fremantle","year":"2015"},{"key":"10.1016\/j.iot.2019.100092_bib0007","series-title":"2016 Cloudification of the Internet of Things (CIoT)","first-page":"1","article-title":"OAuthing: privacy-enhancing federation for the Internet of Things","author":"Fremantle","year":"2016"},{"key":"10.1016\/j.iot.2019.100092_bib0008","series-title":"The Origin of Concurrent Programming","first-page":"413","article-title":"Communicating sequential processes","author":"Hoare","year":"1978"},{"year":"1985","series-title":"Communicating Sequential Processes","author":"Hoare","key":"10.1016\/j.iot.2019.100092_bib0009"},{"year":"2010","series-title":"Understanding Concurrent Systems","author":"Roscoe","key":"10.1016\/j.iot.2019.100092_bib0010"},{"key":"10.1016\/j.iot.2019.100092_bib0011","series-title":"Tools and Algorithms for the Construction and Analysis of Systems","first-page":"187","article-title":"FDR3 \u2014 A Modern Refinement Checker for CSP","volume":"8413","author":"Thomas Gibson-Robinson","year":"2014"},{"key":"10.1016\/j.iot.2019.100092_bib0012","series-title":"Technical Report","article-title":"The OAuth2.0 authorization protocol. 2011","author":"Hammer-Lahav","year":"2011"},{"key":"10.1016\/j.iot.2019.100092_bib0013","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1016\/j.jnca.2015.05.023","article-title":"Policy enforcement system for secure interoperable control in distributed smart grid systems","volume":"59","author":"Alcaraz","year":"2016","journal-title":"J. Netw. Comput. Appl."},{"key":"10.1016\/j.iot.2019.100092_bib0014","series-title":"Security Solutions and Applied Cryptography in Smart Grid Communications, IGI Global, USA","first-page":"137","article-title":"Secure interoperability in cyber-physical systems","author":"Alcaraz","year":"2017"},{"key":"10.1016\/j.iot.2019.100092_bib0015","doi-asserted-by":"crossref","unstructured":"C. Alcaraz, Secure Interconnection of IT-OT Networks in Industry 4.0, Springer International Publishing, Cham, pp. 201\u2013217.","DOI":"10.1007\/978-3-030-00024-0_11"},{"key":"10.1016\/j.iot.2019.100092_bib0016","unstructured":"Power systems management and associated information exchange Data and communications security Part 8: Role-based access control (Preview), Accessed: 24-06-2019(https:\/\/webstore.iec.ch\/preview\/info_iec62351-8%7Bed1.0%7Den.pdf)."},{"key":"10.1016\/j.iot.2019.100092_sbref0013","series-title":"Proceedings of 15th NIST-NSA National Computer Security Conference","first-page":"554","article-title":"Role-based access controls","author":"Ferraiolo","year":"1992"},{"issue":"2","key":"10.1016\/j.iot.2019.100092_bib0018","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1109\/2.485845","article-title":"Role-based access control models","volume":"29","author":"Sandhu","year":"1996","journal-title":"Computer"},{"issue":"4","key":"10.1016\/j.iot.2019.100092_bib0019","doi-asserted-by":"crossref","first-page":"601","DOI":"10.3233\/JCS-140503","article-title":"Discovering concrete attacks on website authorization by formal analysis1","volume":"22","author":"Bansal","year":"2014","journal-title":"J. Comput. Secur."},{"key":"10.1016\/j.iot.2019.100092_bib0020","series-title":"2011 International Conference on Communication Systems and Network Technologies (CSNT)","first-page":"655","article-title":"Formal verification of oauth 2.0 using alloy framework","author":"Pai","year":"2011"},{"year":"2004","series-title":"Alloy 3.0 Reference Manual","author":"Jackson","key":"10.1016\/j.iot.2019.100092_bib0021"},{"key":"10.1016\/j.iot.2019.100092_bib0022","unstructured":"T. Lodderstedt, M. McGloin, P. Hunt, Oauth 2.0 threat model and security considerations, 2013,"},{"key":"10.1016\/j.iot.2019.100092_bib0023","unstructured":"A. Banks, R. Gupta, MQ Telemetry Transport (MQTT) V3.1.1 Protocol Specification: Committee Specification Draft 02 \/ Public Review Draft 02, 2014,"},{"issue":"P1","key":"10.1016\/j.iot.2019.100092_bib0024","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/j.adhoc.2015.05.013","article-title":"A formal model and analysis of an iot protocol","volume":"36","author":"Aziz","year":"2016","journal-title":"Ad Hoc Netw."},{"key":"10.1016\/j.iot.2019.100092_bib0025","series-title":"8th IEEE International Workshop on Object-Oriented Real-Time Dependable Systems (WORDS 2003)","first-page":"304","article-title":"Modelling publish\/subscribe communication systems: towards a formal approach","author":"Baldoni","year":"2003"},{"key":"10.1016\/j.iot.2019.100092_bib0026","series-title":"Proceedings of the 2011 IEEE International Conference on Services Computing","first-page":"496","article-title":"A petri-net model for the publish-subscribe paradigm and its application for the verification of the bonjourGrid middleware","author":"Abidi","year":"2011"},{"key":"10.1016\/j.iot.2019.100092_bib0027","series-title":"Proceedings of the 35th Annual Hawaii International Conference on System Sciences (HICSS\u201902)-Volume 9 - Volume 9","first-page":"303","article-title":"Security issues and requirements for internet-scale publish-subscribe systems","author":"Wang","year":"2002"},{"key":"10.1016\/j.iot.2019.100092_bib0028","series-title":"Proceedings of the 10th International Conference on Model Checking Software","first-page":"166","article-title":"Model checking publish-subscribe systems","author":"Garlan","year":"2003"},{"key":"10.1016\/j.iot.2019.100092_bib0029","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/j.entcs.2004.08.069","article-title":"Model checking publish\/subscribe notification for thinkteam ®","volume":"133","author":"ter Beek","year":"2005","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.iot.2019.100092_bib0030","series-title":"2014 IEEE Network Operations and Management Symposium, NOMS 2014, Krakow, Poland, May 5-9, 2014","first-page":"1","article-title":"Improved reliability of large scale publish\/subscribe based moms using model checking","author":"Jia","year":"2014"},{"key":"10.1016\/j.iot.2019.100092_bib0031","series-title":"Proceedings of the 29th International Conference on Software Engineering","first-page":"199","article-title":"On accurate automatic verification of publish-subscribe architectures","author":"Baresi","year":"2007"},{"key":"10.1016\/j.iot.2019.100092_bib0032","series-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2007, 27th IFIP WG 6.1 International Conference, Tallinn, Estonia, June 27-29, 2007, Proceedings","first-page":"247","article-title":"Formal analysis of publish-subscribe systems by probabilistic timed automata","volume":"4574","author":"He","year":"2007"},{"key":"10.1016\/j.iot.2019.100092_bib0033","series-title":"Proceedings of the 4th International Conference on Quality of Software-Architectures: Models and Architectures","first-page":"119","article-title":"Quality prediction of service compositions through probabilistic model checking","author":"Gallotti","year":"2008"},{"key":"10.1016\/j.iot.2019.100092_bib0034","series-title":"Proceedings of the 6th International Conference on Integrated Formal Methods","first-page":"253","article-title":"Modelling and verification of the LMAC protocol for wireless sensor networks","author":"Fehnker","year":"2007"},{"key":"10.1016\/j.iot.2019.100092_bib0035","series-title":"Proceedings of the 5th International Conference on Ad-Hoc, Mobile, and Wireless Networks","first-page":"128","article-title":"Formal verification and simulation for performance analysis for probabilistic broadcast protocols","author":"Fehnker","year":"2006"},{"issue":"1","key":"10.1016\/j.iot.2019.100092_bib0036","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/j.tcs.2011.07.018","article-title":"Analysis of a clock synchronization protocol for wireless sensor networks","volume":"413","author":"Heidarian","year":"2012","journal-title":"Theor. Comput. Sci."},{"year":"2004","series-title":"Unified Modeling Language Reference Manual","author":"Rumbaugh","key":"10.1016\/j.iot.2019.100092_bib0037"},{"key":"10.1016\/j.iot.2019.100092_bib0038","series-title":"Technical Report","article-title":"OpenID Connect Core 1.0","author":"Sakimura","year":"2014"},{"key":"10.1016\/j.iot.2019.100092_bib0039","series-title":"Formal Methods and Testing","first-page":"1","article-title":"Model based testing with labelled transition systems","author":"Tretmans","year":"2008"},{"key":"10.1016\/j.iot.2019.100092_bib0040","unstructured":"N. Sakimura, J. Bradley, M. Jones, Final: OpenID Connect Dynamic Client Registration 1.0 Incorporating Errata Set 1, 2015, http:\/\/openid.net\/specs\/openid-connect-registration-1_0.html."},{"key":"10.1016\/j.iot.2019.100092_bib0041","unstructured":"J. Richer, Oauth token introspection, 2013,"},{"issue":"2","key":"10.1016\/j.iot.2019.100092_bib0042","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/0304-3975(94)00169-J","article-title":"A brief history of timed csp","volume":"138","author":"Davies","year":"1995","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.iot.2019.100092_bib0043","doi-asserted-by":"crossref","first-page":"e114","DOI":"10.7717\/peerj-cs.114","article-title":"A survey of secure middleware for the internet of things","volume":"3","author":"Fremantle","year":"2017","journal-title":"PeerJ Comput. Sci."},{"year":"2014","series-title":"Threat Modeling: Designing for Security","author":"Shostack","key":"10.1016\/j.iot.2019.100092_bib0044"},{"issue":"1","key":"10.1016\/j.iot.2019.100092_bib0045","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s00766-010-0115-7","article-title":"A privacy threat analysis framework: supporting the elicitation and fulfillment of privacy requirements","volume":"16","author":"Deng","year":"2011","journal-title":"Requir. Eng."},{"year":"2010","series-title":"Modeling in Event-B: System and Software Engineering","author":"Abrial","key":"10.1016\/j.iot.2019.100092_bib0046"},{"key":"10.1016\/j.iot.2019.100092_bib0047","first-page":"139","article-title":"A CSP Account of Event-B Refinement","volume":"vol. 55","author":"Derrick","year":"2011"}],"container-title":["Internet of Things"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2542660519301763?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2542660519301763?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T14:48:51Z","timestamp":1762872531000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2542660519301763"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12]]},"references-count":47,"alternative-id":["S2542660519301763"],"URL":"https:\/\/doi.org\/10.1016\/j.iot.2019.100092","relation":{},"ISSN":["2542-6605"],"issn-type":[{"type":"print","value":"2542-6605"}],"subject":[],"published":{"date-parts":[[2019,12]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Deriving event data sharing in IoT systems using formal modelling and analysis","name":"articletitle","label":"Article Title"},{"value":"Internet of Things","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.iot.2019.100092","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2019 Elsevier B.V. All rights reserved.","name":"copyright","label":"Copyright"}],"article-number":"100092"}}