{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T19:40:16Z","timestamp":1779392416228,"version":"3.53.1"},"reference-count":55,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"4","license":[{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"name":"Royal Academy of Engineering and UKRI","award":["EP\/V026763\/1"],"award-info":[{"award-number":["EP\/V026763\/1"]}]},{"name":"Royal Academy of Engineering and UKRI","award":["EP\/V026801\/2"],"award-info":[{"award-number":["EP\/V026801\/2"]}]},{"name":"FAIR-SPACE Hub","award":["EP\/R026092"],"award-info":[{"award-number":["EP\/R026092"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Dependable and Secure Comput."],"published-print":{"date-parts":[[2024,7]]},"DOI":"10.1109\/tdsc.2023.3345543","type":"journal-article","created":{"date-parts":[[2023,12,21]],"date-time":"2023-12-21T20:16:45Z","timestamp":1703189805000},"page":"4048-4065","source":"Crossref","is-referenced-by-count":5,"title":["Security-Minded Verification of Cooperative Awareness Messages"],"prefix":"10.1109","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7708-3877","authenticated-orcid":false,"given":"Marie","family":"Farrell","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Manchester, Manchester, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4661-000X","authenticated-orcid":false,"given":"Matthew","family":"Bradbury","sequence":"additional","affiliation":[{"name":"School of Computing, Communications, Lancaster University, Lancaster, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6666-6954","authenticated-orcid":false,"given":"Rafael C.","family":"Cardoso","sequence":"additional","affiliation":[{"name":"Department of Computing Science, University of Aberdeen, Aberdeen, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0875-3862","authenticated-orcid":false,"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Manchester, Manchester, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1426-1896","authenticated-orcid":false,"given":"Louise A.","family":"Dennis","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Manchester, Manchester, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4610-9533","authenticated-orcid":false,"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Manchester, Manchester, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6701-3354","authenticated-orcid":false,"given":"Al Tariq","family":"Sheik","sequence":"additional","affiliation":[{"name":"WMG, University of Warwick, Coventry, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9833-5930","authenticated-orcid":false,"given":"Hu","family":"Yuan","sequence":"additional","affiliation":[{"name":"School of Computer Science, Mathematics, Kingston University, London, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4715-212X","authenticated-orcid":false,"given":"Carsten","family":"Maple","sequence":"additional","affiliation":[{"name":"WMG, University of Warwick, Coventry, U.K."}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/AERO47225.2020.9172563"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30446-1_25"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/3342355"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/WD.2013.6686514"},{"key":"ref5","article-title":"Intelligent transport systems (ITS); vehicular communications; basic set of applications; part 2: Specification of cooperative awareness basic service","year":"2019"},{"key":"ref6","volume-title":"Computer Security: Principles and Practice","author":"Stallings","year":"2012"},{"key":"ref7","article-title":"The threats to our products","author":"Kohnfelder","year":"1999"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.6028\/nist.sp.800-30r1"},{"key":"ref9","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"Holzmann","year":"2003"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98938-9_10"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1002\/9781119991472"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91908-9_25"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_6"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-68063-7_10"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22969-0_4"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-16722-6_12"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/11423348_14"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.1998.683155"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/32.713329"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91271-4_13"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-12988-0_2"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW.2018.00033"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-16874-2_1"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/NOTERE.2011.5957992"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW.2013.60"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27375-9_7"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijproman.2012.09.011"},{"key":"ref31","article-title":"Intelligent transport systems (ITS); vehicular communications; basic set of applications; definitions","year":"2009"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.6028\/NIST.SP.800-150"},{"key":"ref33","article-title":"Intelligent transport systems (ITS); security; threat, vulnerability and risk analysis (TVRA)","year":"2017"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/AERO47225.2020.9172785"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2018.12.002"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/CSAC.1999.816013"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/TITS.2011.2161469"},{"key":"ref38","first-page":"336","article-title":"The use of formal methods for trusted digital signature devices","volume-title":"Proc. Florida Artif. Intell. Res. Soc. Conf","author":"Langenstein"},{"key":"ref39","article-title":"Intelligent transport systems (ITS); security; trust and privacy management","year":"2019"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04431-1_15"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.348.3"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44267-4_6"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1109\/TMC.2010.133"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.4108\/ICST.SIMUTOOLS2008.3027"},{"key":"ref46","article-title":"IoT transport and mobility demonstrator: Cyber security testing on national infrastructure","author":"Maple","year":"2019"},{"key":"ref47","first-page":"1","article-title":"Free-fall: Hacking Tesla from wireless to CAN bus","volume-title":"Proc. Black Hat USA","author":"Nie"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/APCC.2014.7092849"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_29"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-76384-8_4"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1007\/BF00291051"},{"key":"ref54","volume-title":"On the Refinement Calculus","author":"Morgan","year":"1988"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1177\/0278364919883338"}],"container-title":["IEEE Transactions on Dependable and Secure Computing"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8858\/10592103\/10368348.pdf?arnumber=10368348","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,17]],"date-time":"2024-07-17T04:48:51Z","timestamp":1721191731000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10368348\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7]]},"references-count":55,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.1109\/tdsc.2023.3345543","relation":{},"ISSN":["1545-5971","1941-0018","2160-9209"],"issn-type":[{"value":"1545-5971","type":"print"},{"value":"1941-0018","type":"electronic"},{"value":"2160-9209","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,7]]}}}