{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T16:03:47Z","timestamp":1774022627749,"version":"3.50.1"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030545482","type":"print"},{"value":"9783030545499","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-54549-9_9","type":"book-chapter","created":{"date-parts":[[2020,8,19]],"date-time":"2020-08-19T19:03:42Z","timestamp":1597863822000},"page":"133-149","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Automated Attacker Synthesis for Distributed Protocols"],"prefix":"10.1007","author":[{"given":"Max","family":"von Hippel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cole","family":"Vick","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cristina","family":"Nita-Rotaru","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,31]]},"reference":[{"issue":"1","key":"9_CR1","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1145\/3061640.3061652","volume":"48","author":"R Alur","year":"2017","unstructured":"Alur, R., Tripakis, S.: Automatic synthesis of distributed protocols. SIGACT News 48(1), 55\u201390 (2017)","journal-title":"SIGACT News"},{"key":"9_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Bang, L., Rosner, N., Bultan, T.: Online synthesis of adaptive side-channel attacks based on noisy observations. In: 2018 IEEE European Symposium on Security and Privacy, pp. 307\u2013322. IEEE (2018)","DOI":"10.1109\/EuroSP.2018.00029"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., Dupressoir, F., Fouque, P.A., Gr\u00e9goire, B., Zapalowicz, J.C.: Synthesis of fault attacks on cryptographic implementations. In: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, pp. 1016\u20131027 (2014)","DOI":"10.1145\/2660267.2660304"},{"key":"9_CR5","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: 14th IEEE Computer Security Foundations Workshop, pp. 82\u201396. IEEE Computer Society, Cape Breton (2001)"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Branco, R., Hu, K., Kawakami, H., Sun, K.: A mathematical modeling of exploitations and mitigation techniques using set theory. In: 2018 IEEE Security and Privacy Workshops (SPW), pp. 323\u2013328. IEEE (2018)","DOI":"10.1109\/SPW.2018.00050"},{"issue":"6","key":"9_CR7","first-page":"13","volume":"36","author":"S Bratus","year":"2011","unstructured":"Bratus, S., Locasto, M.E., Patterson, M.L., Sassaman, L., Shubina, A.: Exploit programming: from buffer overflows to weird machines and theory of computation. USENIX Login 36(6), 13\u201321 (2011)","journal-title":"USENIX Login"},{"key":"9_CR8","unstructured":"Cho, C.Y., Babic, D., Poosankam, P., Chen, K.Z., Wu, E.X., Song, D.: MACE: model-inference-assisted concolic exploration for protocol and vulnerability discovery. In: USENIX Security Symposium, vol. 139 (2011)"},{"key":"9_CR9","unstructured":"Chong, S., et al.: Report on the NSF workshop on formal methods for security (2016)"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Church, A.: Application of recursive arithmetic to the problem of circuit synthesis (1957). https:\/\/doi.org\/10.2307\/2271310","DOI":"10.2307\/2271310"},{"key":"9_CR11","unstructured":"Dijkstra, E.W., et al.: Notes on structured programming (1970). http:\/\/www.cs.utexas.edu\/users\/EWD\/ewd02xx\/EWD249.PDF. Accessed 11 May 2020"},{"key":"9_CR12","unstructured":"Duran, J.W., Ntafos, S.: A report on random testing. In: Proceedings of the 5th International Conference on Software Engineering, pp. 179\u2013183. IEEE Press (1981)"},{"key":"9_CR13","unstructured":"Friedrichs, O.: A simple TCP spoofing attack (1997). http:\/\/citi.umich.edu\/u\/provos\/papers\/secnet-spoof.txt. Accessed 3 Jan 2020"},{"key":"9_CR14","unstructured":"von Hippel, M., Vick, C., Tripakis, S., Nita-Rotaru, C.: Automated attacker synthesis for distributed protocols (2020). arXiv preprint arXiv:2004.01220"},{"key":"9_CR15","volume-title":"The Spin Model Checker","author":"G Holzmann","year":"2003","unstructured":"Holzmann, G.: The Spin Model Checker. Addison-Wesley, Boston (2003)"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Hoque, E., Chowdhury, O., Chau, S.Y., Nita-Rotaru, C., Li, N.: Analyzing operational behavior of stateful protocol implementations for detecting semantic bugs. In: 2017 47th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 627\u2013638. IEEE (2017)","DOI":"10.1109\/DSN.2017.36"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Huang, S.K., Huang, M.H., Huang, P.Y., Lai, C.W., Lu, H.L., Leong, W.M.: Crax: software crash analysis for automatic exploit generation by modeling attacks as symbolic continuations. In: 2012 IEEE Sixth International Conference on Software Security and Reliability, pp. 78\u201387. IEEE (2012)","DOI":"10.1109\/SERE.2012.20"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Huang, Z., Etigowni, S., Garcia, L., Mitra, S., Zonouz, S.: Algorithmic attack synthesis using hybrid dynamics of power grid critical infrastructures. In: 2018 48th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks, pp. 151\u2013162. IEEE (2018)","DOI":"10.1109\/DSN.2018.00027"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Jero, S., Lee, H., Nita-Rotaru, C.: Leveraging state information for automated attack discovery in transport protocol implementations. In: 2015 45th Annual IEEE\/IFIP International Conference on Dependable Systems and Networks, pp. 1\u201312. IEEE (2015)","DOI":"10.1109\/DSN.2015.22"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-030-25540-4_12","volume-title":"Computer Aided Verification","author":"E Kang","year":"2019","unstructured":"Kang, E., Lafortune, S., Tripakis, S.: Automated synthesis of secure platform mappings. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 219\u2013237. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_12"},{"key":"9_CR21","unstructured":"Kayacik, H.G., Zincir-Heywood, A.N., Heywood, M.I., Burschka, S.: Generating mimicry attacks using genetic programming: a benchmarking study. In: 2009 IEEE Symposium on Computational Intelligence in Cyber Security, pp. 136\u2013143. IEEE (2009)"},{"key":"9_CR22","unstructured":"Kla\u0161ka, D., Ku\u010dera, A., Lamser, T., \u0158eh\u00e1k, V.: Automatic synthesis of efficient regular strategies in adversarial patrolling games. In: Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems, pp. 659\u2013666. International Foundation for Autonomous Agents and Multiagent Systems (2018)"},{"key":"9_CR23","unstructured":"Lin, L., Zhu, Y., Su, R.: Synthesis of actuator attackers for free (2019). arXiv preprint arXiv:1904.10159"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"McMillan, K.L., Zuck, L.D.: Formal specification and testing of QUIC. In: Proceedings of the ACM Special Interest Group on Data Communication, pp. 227\u2013240. ACM (2019)","DOI":"10.1145\/3341302.3342087"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Meira-G\u00f3es, R., Kwong, R., Lafortune, S.: Synthesis of sensor deception attacks for systems modeled as probabilistic automata. In: 2019 American Control Conference, pp. 5620\u20135626. IEEE (2019)","DOI":"10.23919\/ACC.2019.8814740"},{"key":"9_CR26","volume-title":"The Art of Software Testing","author":"GJ Myers","year":"1979","unstructured":"Myers, G.J.: The Art of Software Testing. John Wiley & Sons, Hoboken (1979)"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Phan, Q.S., Bang, L., Pasareanu, C.S., Malacaria, P., Bultan, T.: Synthesis of adaptive side-channel attacks. In: 2017 IEEE 30th Computer Security Foundations Symposium, pp. 328\u2013342. IEEE (2017)","DOI":"10.1109\/CSF.2017.8"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"Postel, J., et al.: Rfc 793 Transmission Control Protocol (1981)","DOI":"10.17487\/rfc0793"},{"issue":"17","key":"9_CR30","first-page":"26","volume":"68","author":"H Srivastava","year":"2013","unstructured":"Srivastava, H., Dwivedi, K., Pankaj, P.K., Tewari, V.: A formal attack centric framework highlighting expected losses of an information security breach. Int. J. Comput. Appl. 68(17), 26\u201331 (2013)","journal-title":"Int. J. Comput. Appl."},{"key":"9_CR31","unstructured":"@henryouly: [Solved] TCP connection blocked in SYN\\_SENT status (2007). https:\/\/bbs.archlinux.org\/viewtopic.php?id=33875. Accessed 3 Jan 2020"},{"issue":"3","key":"9_CR32","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1109\/MM.2019.2910010","volume":"39","author":"C Trippel","year":"2019","unstructured":"Trippel, C., Lustig, D., Martonosi, M.: Security verification via automatic hardware-aware exploit synthesis: the CheckMate approach. IEEE Micro 39(3), 84\u201393 (2019)","journal-title":"IEEE Micro"},{"key":"9_CR33","unstructured":"Valizadeh, S., van Dijk, M.: Toward a theory of cyber attacks (2019). arXiv preprint arXiv:1901.01598"},{"issue":"4","key":"9_CR34","doi-asserted-by":"publisher","first-page":"655","DOI":"10.1007\/s00145-012-9134-5","volume":"26","author":"M Van Dijk","year":"2013","unstructured":"Van Dijk, M., Juels, A., Oprea, A., Rivest, R.L.: FlipIt: The game of \u201cstealthy takeover\u201d. J. Cryptol. 26(4), 655\u2013713 (2013)","journal-title":"J. Cryptol."},{"key":"9_CR35","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the First Symposium on Logic in Computer Science, pp. 322\u2013331. IEEE Computer Society (1986)"},{"key":"9_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-319-24255-2_25","volume-title":"Computer Safety, Reliability, and Security","author":"M Vasilevskaya","year":"2015","unstructured":"Vasilevskaya, M., Nadjm-Tehrani, S.: Quantifying risks to data assets using formal metrics in embedded system design. In: Koornneef, F., van Gulijk, C. (eds.) SAFECOMP 2015. LNCS, vol. 9337, pp. 347\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24255-2_25"},{"issue":"4","key":"9_CR37","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3331524","volume":"52","author":"W Wide\u0142","year":"2019","unstructured":"Wide\u0142, W., Audinot, M., Fila, B., Pinchinat, S.: Beyond 2014: formal methods for attack tree-based security modeling. ACM Comput. Surv. 52(4), 1\u201336 (2019)","journal-title":"ACM Comput. Surv."},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"You, W., et al.: Semfuzz: semantics-based automatic generation of proof-of-concept exploits. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 2139\u20132154 (2017)","DOI":"10.1145\/3133956.3134085"},{"key":"9_CR39","unstructured":"Yuan, Y., Moon, S.J., Uppal, S., Jia, L., Sekar, V.: NetSMC: a custom symbolic model checker for stateful network verification. In: 17th USENIX Symposium on Networked Systems Design and Implementation. USENIX Association, Santa Clara (2020)"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability, and Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-54549-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,23]],"date-time":"2021-04-23T23:25:07Z","timestamp":1619220307000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-54549-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030545482","9783030545499"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-54549-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"31 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAFECOMP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Safety, Reliability, and Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 September 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 September 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"39","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"safecomp2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/safecomp2020.di.fc.ul.pt\/","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":"116","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":"2","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":"23% - 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.2","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)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}