{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T17:43:42Z","timestamp":1770918222864,"version":"3.50.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030304454","type":"print"},{"value":"9783030304461","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-30446-1_25","type":"book-chapter","created":{"date-parts":[[2019,9,8]],"date-time":"2019-09-08T19:03:18Z","timestamp":1567969398000},"page":"471-490","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages"],"prefix":"10.1007","author":[{"given":"Marie","family":"Farrell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Bradbury","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Louise A.","family":"Dennis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hu","family":"Yuan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carsten","family":"Maple","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,9,9]]},"reference":[{"key":"25_CR1","unstructured":"Intelligent Transport Systems (ITS): Vehicular Communications, Basic Set of Applications. Part 2: Specification of Cooperative Awareness Basic Service. Standard Draft ETSI EN 302 637\u20132, European Telecommunications Standards Institute, November 2018. V1.4.0 (2018\u201308)"},{"issue":"6","key":"25_CR2","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/BF00291051","volume":"25","author":"R-J Back","year":"1988","unstructured":"Back, R.-J.: A calculus of refinements for program derivations. Acta Informatica 25(6), 593\u2013624 (1988)","journal-title":"Acta Informatica"},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). \n                      https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"25_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84628-770-1","volume-title":"Principles of the Spin model checker","author":"M Ben-Ari","year":"2008","unstructured":"Ben-Ari, M.: Principles of the Spin model checker. Springer, Cham (2008). \n                      https:\/\/doi.org\/10.1007\/978-1-84628-770-1"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Bittl, S., Gonzalez, A.A., Myrtus, M., Beckmann, H., Sailer, S., Eissfeller, B.: Emerging attacks on VANET security based on GPS time spoofing. In: IEEE Conference on Communications and Network Security, pp. 344\u2013352. IEEE (2015)","DOI":"10.1109\/CNS.2015.7346845"},{"key":"25_CR6","series-title":"Lecture Notes in Electrical Engineering","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-981-13-1328-8_49","volume-title":"Advanced Multimedia and Ubiquitous Engineering","author":"J Choi","year":"2019","unstructured":"Choi, J., Jin, S.: Security threats in connected car environment and proposal of in-vehicle infotainment-based access control mechanism. In: Park, J.J., Loia, V., Choo, K.-K.R., Yi, G. (eds.) MUE\/FutureTech -2018. LNEE, vol. 518, pp. 383\u2013388. Springer, Singapore (2019). \n                      https:\/\/doi.org\/10.1007\/978-981-13-1328-8_49"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-319-98938-9_10","volume-title":"Integrated Formal Methods","author":"M Farrell","year":"2018","unstructured":"Farrell, M., Luckcuck, M., Fisher, M.: Robotics and integrated formal methods: necessity meets opportunity. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 161\u2013171. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-98938-9_10"},{"key":"25_CR9","doi-asserted-by":"publisher","DOI":"10.1002\/9781119991472","volume-title":"An Introduction to Practical Formal Methods Using Temporal Logic","author":"M Fisher","year":"2011","unstructured":"Fisher, M.: An Introduction to Practical Formal Methods Using Temporal Logic. Wiley, Hoboken (2011)"},{"key":"25_CR10","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"key":"25_CR11","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-030-16722-6_12","volume-title":"Fundamental Approaches to Software Engineering","author":"Li Huang","year":"2019","unstructured":"Huang, L., Kang, E.-Y.: Formal verification of safety and security related timing constraints for a cooperative automotive system. In: Fundamental Approaches to Software Engineering. LNCS, vol. 11424, pp. 210\u2013227. Springer, Cham (2019). \n                      https:\/\/doi.org\/10.1007\/978-3-030-16722-6_12"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Jagielski, M., Jones, N., Lin, C.-W., Nita-Rotaru, C., Shiraishi, S.: Threat detection for collaborative adaptive cruise control in connected cars. In: ACM Conference on Security & Privacy in Wireless and Mobile Networks, pp. 184\u2013189. ACM (2018)","DOI":"10.1145\/3212480.3212492"},{"issue":"4","key":"25_CR13","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"25_CR14","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-030-12988-0_2","volume-title":"Formal Techniques for Safety-Critical Systems","author":"M Kamali","year":"2019","unstructured":"Kamali, M., Linker, S., Fisher, M.: Modular verification of vehicle platooning with respect to decisions, space and time. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2018. CCIS, vol. 1008, pp. 18\u201336. Springer, Cham (2019). \n                      https:\/\/doi.org\/10.1007\/978-3-030-12988-0_2"},{"key":"25_CR15","unstructured":"Kohnfelder, L., Garg, P.: The threats to our products (April 1999). \n                      https:\/\/adam.shostack.org\/microsoft\/The-Threats-To-Our-Products.docx\n                      \n                    . Accessed 10 Dec 2018"},{"key":"25_CR16","unstructured":"Langenstein, B., Vogt, R., Ullmann, M.: The use of formal methods for trusted digital signature devices. In: Florida Artificial Intelligence Research Society, pp. 336\u2013340. AAAI Press (2000)"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"25_CR18","unstructured":"Liu, J., Yan, C., Xu, W.: Can you trust autonomous vehicles: contactless attacks against sensors of self-driving vehicles. In: DEFCON24 (2016). \n                      http:\/\/bit.ly\/2EQNOLs"},{"key":"25_CR19","volume-title":"Formal Specification and Verification of Autonomous Robotic Systems: A Survey","author":"M Luckcuck","year":"2019","unstructured":"Luckcuck, M., Farrell, M., Dennis, L., Dixon, C., Fisher, M.: Formal Specification and Verification of Autonomous Robotic Systems: A Survey. ACM Computing Surveys, US (2019). accepted"},{"key":"25_CR20","unstructured":"Michele Rondinone, A.C.: Deliverable (d) no: 5.1 definition of v2x message sets. report, Universidad Miguel Hernandez, V1.0 27\/08\/2018 (August 2018)"},{"key":"25_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3273-8","volume-title":"On the Refinement Calculus","author":"C Morgan","year":"1988","unstructured":"Morgan, C., Robinson, K., Gardiner, P.: On the Refinement Calculus. Springer, Cham (1988). \n                      https:\/\/doi.org\/10.1007\/978-1-4471-3273-8"},{"key":"25_CR22","first-page":"2015","volume":"11","author":"J Petit","year":"2015","unstructured":"Petit, J., Stottelaar, B., Feiri, M., Kargl, F.: Remote attacks on automated vehicles sensors: experiments on camera and lidar. Black Hat Eur. 11, 2015 (2015)","journal-title":"Black Hat Eur."},{"key":"25_CR23","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Symposium on the Foundations of Computer Science, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"25_CR24","unstructured":"Ross, R.S.: Guide for conducting risk assessments. Technical report, National Institute of Standards and Technology. SP 800\u201330 Rev. 1 (September 2012)"},{"key":"25_CR25","first-page":"3","volume":"2","author":"A Ruddle","year":"2009","unstructured":"Ruddle, A., et al.: Security requirements for automotive on-board networks based on dark-side scenarios. EVITA Deliverable D 2, 3 (2009)","journal-title":"EVITA Deliverable D"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Santa, J., Pere\u00f1\u00edguez, F., Morag\u00f3n, A., Skarmeta, A.F.: Vehicle-to-infrastructure messaging proposal based on CAM\/DENM specifications. In: Wireless Days (WD), IFIP, pp. 1\u20137. IEEE (2013)","DOI":"10.1109\/WD.2013.6686514"},{"key":"25_CR27","unstructured":"Schneider, S.: Formal analysis of a non-repudiation protocol. In: Computer Security Foundations Workshop, pp. 54\u201365. IEEE (1998)"},{"issue":"9","key":"25_CR28","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1109\/32.713329","volume":"24","author":"S Schneider","year":"1998","unstructured":"Schneider, S.: Verifying authentication protocols in CSP. IEEE Trans. Softw. Eng. 24(9), 741\u2013758 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"25_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/11423348_14","volume-title":"Communicating Sequential Processes. The First 25 Years","author":"S Schneider","year":"2005","unstructured":"Schneider, S., Delicata, R.: Verifying security protocols: an application of CSP. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. The First 25 Years. LNCS, vol. 3525, pp. 243\u2013263. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/11423348_14"},{"key":"25_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-319-57288-8_6","volume-title":"NASA Formal Methods","author":"C Snook","year":"2017","unstructured":"Snook, C., Hoang, T.S., Butler, M.: Analysing security protocols using refinement in iUML-B. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 84\u201398. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-57288-8_6"},{"key":"25_CR31","volume-title":"Computer Security: Principles and Practice","author":"W Stallings","year":"2012","unstructured":"Stallings, W., Brown, L., Bauer, M.D., Bhattacharjee, A.K.: Computer Security: Principles and Practice. Pearson, Upper Saddle River (2012)"},{"key":"25_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-319-22969-0_4","volume-title":"Software Engineering and Formal Methods","author":"G Vanspauwen","year":"2015","unstructured":"Vanspauwen, G., Jacobs, B.: Verifying protocol implementations by augmenting existing cryptographic libraries with specifications. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 53\u201368. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-22969-0_4"},{"key":"25_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-68063-7_10","volume-title":"Security and Trust Management","author":"J Whitefield","year":"2017","unstructured":"Whitefield, J., et al.: Formal analysis of V2X revocation protocols. In: Livraga, G., Mitchell, C. (eds.) STM 2017. LNCS, vol. 10547, pp. 147\u2013163. Springer, Cham (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-319-68063-7_10"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30446-1_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,8]],"date-time":"2019-09-08T19:43:29Z","timestamp":1567971809000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30446-1_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030304454","9783030304461"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30446-1_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"9 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SEFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Software Engineering and Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oslo","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sefm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sefm2019.inria.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"89","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"27","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}