{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T06:19:16Z","timestamp":1743142756832,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030630850"},{"type":"electronic","value":"9783030630867"}],"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-63086-7_5","type":"book-chapter","created":{"date-parts":[[2020,12,11]],"date-time":"2020-12-11T08:07:25Z","timestamp":1607674045000},"page":"61-79","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Verification of Configuration-Based Mutation Techniques for Moving Target Defense"],"prefix":"10.1007","author":[{"given":"Muhammad Abdul Basit Ur","family":"Rahim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ehab","family":"Al-Shaer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qi","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,12,12]]},"reference":[{"key":"5_CR1","unstructured":"Al-Shaer, E.: Mutable networks, National cyber leap year summit 2009 participants ideas report. Technical report, Networking and Information Technology Research and Development (NTIRD) (2009)"},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-1-4614-0977-9_9","volume-title":"Moving Target Defense, Advances in Information Security","author":"E Al-Shaer","year":"2011","unstructured":"Al-Shaer, E.: Toward network configuration randomization for moving target defense. In: Jajodia, S., Ghosh, A.K., Swarup, V., Wang, C., Wang, X.S. (eds.) Moving Target Defense, Advances in Information Security, vol. 54, pp. 153\u2013159. Springer, New York (2011). https:\/\/doi.org\/10.1007\/978-1-4614-0977-9_9"},{"key":"5_CR3","series-title":"Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-642-36883-7_19","volume-title":"Security and Privacy in Communication Networks","author":"E Al-Shaer","year":"2013","unstructured":"Al-Shaer, E., Duan, Q., Jafarian, J.H.: Random host mutation for moving target defense. In: Keromytis, A.D., Di Pietro, R. (eds.) SecureComm 2012. LNICST, vol. 106, pp. 310\u2013327. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36883-7_19"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"An, J., Zhan, N., Li, X., Zhang, M., Yi, W.: Model checking bounded continuous-time extended linear duration invariants. In: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (Part of CPS Week), HSCC 2018 pp. 81\u201390. ACM, New York (2018)","DOI":"10.1145\/3178126.3178147"},{"key":"5_CR5","unstructured":"Atighetchi, M., Pal, P., Webber, F., Jones, C.: Adaptive use of network-centric mechanisms in cyber-defense. In: Second IEEE International Symposium on Network Computing and Applications, NCA 2003, pp. 179\u2013188 (2003)"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Basit-Ur-Rahim, M.A., Ahmad, J., Arif, F.: Parallel verification of UML using divine tool. In: 2013 5th International Conference on Computer Science and Information Technology, pp. 49\u201353 (2013)","DOI":"10.1109\/CSIT.2013.6588757"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Basit-Ur-Rahim, M.A., Arif, F., Ahmad, J.: Modeling of real-time embedded systems using SysML and its verification using UPPAAL and DiVinE. In: 2014 IEEE 5th International Conference on Software Engineering and Service Science, pp. 132\u2013136 (2014)","DOI":"10.1109\/ICSESS.2014.6933529"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Dadeau, F., H\u00e9am, P., Kheddam, R.: Mutation-based test generation from security protocols in hlpsl. In: 2011 Fourth IEEE International Conference on Software Testing, Verification and Validation, pp. 240\u2013248 (2011)","DOI":"10.1109\/ICST.2011.42"},{"key":"5_CR10","unstructured":"Droms, R., Bound, J., Volz, B., Lemon, T., Perkins, C., Carney, M.: Dynamic host configuration protocol for IPv6 (2003). https:\/\/tools.ietf.org\/html\/rfc3315"},{"key":"5_CR11","unstructured":"Dunlop, M., Groat, S., Marchany, R., Tront, J.: IPv6: now you see me, now you don\u2019t. In: The Tenth International Conference on Networks, ICN 2011 (2011)"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Dunlop, M., Groat, S., Urbanski, W., Marchany, R., Tront, J.: Mt6d: a moving target IPv6 defense. In: 2011 - MILCOM 2011 Military Communications Conference, pp. 1321\u20131326 (2011)","DOI":"10.1109\/MILCOM.2011.6127486"},{"key":"5_CR13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511619953","volume-title":"Real-Time Systems: Formal Specification and Automatic Verification","author":"ER Olderog","year":"2008","unstructured":"Olderog, E.R., Dierks, H.: Real-Time Systems: Formal Specification and Automatic Verification. Cambridge University Press, Cambridge (2008)"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Fang, K., Li, X., Hao, J., Feng, Z.: Formal modeling and verification of security protocols on cloud computing systems based on UML 2.3. In: 2016 IEEE Trustcom\/BigDataSE\/ISPA, pp. 852\u2013859 (2016)","DOI":"10.1109\/TrustCom.2016.0148"},{"key":"5_CR15","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.cose.2013.01.005","volume":"36","author":"Y Fu","year":"2013","unstructured":"Fu, Y., Kon\u00e9, O.: Validation of security protocol implementations from security objectives. Comput. Secur. 36, 27\u201339 (2013)","journal-title":"Comput. Secur."},{"issue":"1\u20132","key":"5_CR16","doi-asserted-by":"publisher","first-page":"9","DOI":"10.3166\/jancl.14.9-54","volume":"14","author":"V Goranko","year":"2004","unstructured":"Goranko, V., Montanari, A., Sciavicco, G.: A road map of interval temporal logics and duration calculi. J. Appl. Non-Class. Logics 14(1\u20132), 9\u201354 (2004)","journal-title":"J. Appl. Non-Class. Logics"},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/978-3-319-69483-2_7","volume-title":"Dependable Software Engineering. Theories, Tools, and Applications","author":"DP Guelev","year":"2017","unstructured":"Guelev, D.P., Wang, S., Zhan, N.: Compositional hoare-style reasoning about hybrid CSP in the duration calculus. In: Larsen, K.G., Sokolsky, O., Wang, J. (eds.) SETTA 2017. LNCS, vol. 10606, pp. 110\u2013127. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-69483-2_7"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Lugou, F., Li, L.W., Apvrille, L., Ameur-Boulifa, R.: SYSML models and model transformation for security. In: 2016 4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD), pp. 331\u2013338 (2016)","DOI":"10.5220\/0005748703310338"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/11921240_23","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"R Meyer","year":"2006","unstructured":"Meyer, R., Faber, J., Rybalchenko, A.: Model checking duration calculus: a practical approach. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 332\u2013346. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11921240_23"},{"issue":"6","key":"5_CR20","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1017\/S095679680700634X","volume":"17","author":"RL Page","year":"2007","unstructured":"Page, R.L.: Engineering software correctness. J. Funct. Program. 17(6), 675\u2013686 (2007)","journal-title":"J. Funct. Program."},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Pedroza, G., Apvrille, L., Knorreck, D.: Avatar: A SYSML environment for the formal verification of safety and security properties. In: 2011 11th Annual International Conference on New Technologies of Distributed Systems, pp. 1\u201310 (2011)","DOI":"10.1109\/NOTERE.2011.5957992"},{"key":"5_CR22","unstructured":"Rahim, M.A.B.U., Duan, Q., Al-Shaer, E.: A formal analysis of moving target defense (2020)"},{"key":"5_CR23","unstructured":"Basit ur Rahim, M.A., Arif, F.: Translating activity diagram from duration calculus for modeling of real-time systems and its formal verification using UPPAAL and DiVinE. Mehran Univ. Res. J. Eng. Technol. 35(1), 139\u2013154 (2016)"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/978-3-319-09156-3_38","volume-title":"Computational Science and Its Applications \u2013 ICCSA 2014","author":"MA Basit Ur Rahim","year":"2014","unstructured":"Basit Ur Rahim, M.A., Arif, F., Ahmad, J.: Modeling of embedded system using SysML and its parallel verification using DiVinE tool. In: Murgante, B., et al. (eds.) ICCSA 2014. LNCS, vol. 8583, pp. 541\u2013555. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09156-3_38"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-642-19835-9_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"AP Ravn","year":"2011","unstructured":"Ravn, A.P., Srba, J., Vighio, S.: Modelling and verification of web services business activity protocol. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 357\u2013371. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_32"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Schwammberger, M.: Introducing liveness into multi-lane spatial logic lane change controllers using UPPAAL, pp. 17\u201331. CoRR abs\/1804.04346 (2018)","DOI":"10.4204\/EPTCS.269.3"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Shen, G., Li, X., Feng, R., Xu, G., Hu, J., Feng, Z.: An extended UML method for the verification of security protocols. In: 2014 19th International Conference on Engineering of Complex Computer Systems, pp. 19\u201328 (2014)","DOI":"10.1109\/ICECCS.2014.12"},{"key":"5_CR28","doi-asserted-by":"publisher","first-page":"14455","DOI":"10.1109\/ACCESS.2017.2728860","volume":"5","author":"S Sultana","year":"2017","unstructured":"Sultana, S., Arif, F.: Computational conversion via translation rules for transforming C++ code into UPPAAL\u2019s automata. IEEE Access 5, 14455\u201314467 (2017)","journal-title":"IEEE Access"},{"key":"5_CR29","doi-asserted-by":"crossref","unstructured":"Wang, H., Zhou, X., Dong, Y., Tang, L.: Modeling timing behavior for cyber-physical systems. In: 2009 International Conference on Computational Intelligence and Software Engineering, pp. 1\u20134 (2009)","DOI":"10.1109\/CISE.2009.5364357"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-11623-0_14","volume-title":"Fundamentals of Software Engineering","author":"M Zhang","year":"2010","unstructured":"Zhang, M., Liu, Z., Zhan, N.: Model checking linear duration invariants of networks of automata. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 244\u2013259. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11623-0_14"}],"container-title":["Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering","Security and Privacy in Communication Networks"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-63086-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T21:26:34Z","timestamp":1619299594000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-63086-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030630850","9783030630867"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-63086-7_5","relation":{},"ISSN":["1867-8211","1867-822X"],"issn-type":[{"type":"print","value":"1867-8211"},{"type":"electronic","value":"1867-822X"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"12 December 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SecureComm","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Security and Privacy in Communication Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Washington, WA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","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":"21 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"securecomm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/securecomm.eai-conferences.org\/2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Confy","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"120","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":"50","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":"42% - 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":"2,86","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":"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 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)"}}]}}