{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/44193"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/44193","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Security analysis of inter control center communication protocol using model checking","abstract":"Inter Control Center Communication Protocol (ICCP) plays a critical role in the Supervisory Control and Data Acquisition (SCADA) architecture by allowing utilities to exchange data in real time. Given the critical nature of ICCP, security of ICCP is of paramount importance to power community. However, the present state of ICCP security can be best described as an afterthought. The protocol itself does not provide strong authentication and authorization primitives. Furthermore, like many other protocols, interpretation of ICCP's standards is subject to user's interpretation and can aggravate the security situation if not interpreted and implemented in a uniform manner. In this work we undertake the task of formalizing parts of ICCP protocol and analyze and address the potential security issues found within those parts. We develop model of the protocol in a model checking tool called UPPAAL and then use Computation Tree Logic (CTL) properties over this model to see if they are valid. Once a problem is identified, we design a checker that can detect exploitation of the identified vulnerabilities. The soundness of these checkers is then verified by validating properties on the system in conjunction with this new checker.","abstract_html":"Inter Control Center Communication Protocol (ICCP) plays a critical role in the Supervisory Control and Data Acquisition (SCADA) architecture by allowing utilities to exchange data in real time. Given the critical nature of ICCP, security of ICCP is of paramount importance to power community. However, the present state of ICCP security can be best described as an afterthought. The protocol itself does not provide strong authentication and authorization primitives. Furthermore, like many other protocols, interpretation of ICCP&#x27;s standards is subject to user&#x27;s interpretation and can aggravate the security situation if not interpreted and implemented in a uniform manner. In this work we undertake the task of formalizing parts of ICCP protocol and analyze and address the potential security issues found within those parts. We develop model of the protocol in a model checking tool called UPPAAL and then use Computation Tree Logic (CTL) properties over this model to see if they are valid. Once a problem is identified, we design a checker that can detect exploitation of the identified vulnerabilities. The soundness of these checkers is then verified by validating properties on the system in conjunction with this new checker.","abstract_has_math":false,"creators":["Malik, Muhammad Salman"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Campbell, Roy H."],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2013,"date_issued":"2013-05-24T21:53:51Z","date_published":"2013-05-24T21:53:51Z","updated_at":"2026-07-22T22:25:33Z","subjects":["Security","UPPAAL","Inter Control Center Communication Protocol (ICCP)"],"languages":["en"],"rights":["Copyright 2013 Muhammad Salman Malik"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/44193","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Campbell, Roy H."]},{"key":"dc:creator","label":"Author","values":["Malik, Muhammad Salman"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2013-05-24T21:53:51Z","2013-05"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Security","UPPAAL","Inter Control Center Communication Protocol (ICCP)"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2013 Muhammad Salman Malik"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/44193"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["Inter Control Center Communication Protocol (ICCP) plays a critical role in the Supervisory Control and Data Acquisition (SCADA) architecture by allowing utilities to exchange data in real time. Given the critical nature of ICCP, security of ICCP is of paramount importance to power community. However, the present state of ICCP security can be best described as an afterthought. The protocol itself does not provide strong authentication and authorization primitives. Furthermore, like many other protocols, interpretation of ICCP's standards is subject to user's interpretation and can aggravate the security situation if not interpreted and implemented in a uniform manner. In this work we undertake the task of formalizing parts of ICCP protocol and analyze and address the potential security issues found within those parts. We develop model of the protocol in a model checking tool called UPPAAL and then use Computation Tree Logic (CTL) properties over this model to see if they are valid. Once a problem is identified, we design a checker that can detect exploitation of the identified vulnerabilities. The soundness of these checkers is then verified by validating properties on the system in conjunction with this new checker.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2013-04-22T21:26:21Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Malik_MuhammadSalman.pdf: 449451 bytes, checksum: f2564590c6ac6ad056df07efb2ee8831 (MD5)","Made available in DSpace on 2013-05-24T21:53:51Z (GMT). No. of bitstreams: 2 Muhammad Salman_Malik.pdf: 449451 bytes, checksum: f2564590c6ac6ad056df07efb2ee8831 (MD5) license.txt: 4071 bytes, checksum: c97d6bf41b64c5f0d855d30990afc382 (MD5)"]},{"key":"dc:title","label":"Title","values":["Security analysis of inter control center communication protocol using model checking"]}]}],"canonical_facts":{"dc:contributor":["Campbell, Roy H."],"dc:creator":["Malik, Muhammad Salman"],"dc:date":["2013-05-24T21:53:51Z","2013-05"],"dc:description":["Inter Control Center Communication Protocol (ICCP) plays a critical role in the Supervisory Control and Data Acquisition (SCADA) architecture by allowing utilities to exchange data in real time. Given the critical nature of ICCP, security of ICCP is of paramount importance to power community. However, the present state of ICCP security can be best described as an afterthought. The protocol itself does not provide strong authentication and authorization primitives. Furthermore, like many other protocols, interpretation of ICCP's standards is subject to user's interpretation and can aggravate the security situation if not interpreted and implemented in a uniform manner. In this work we undertake the task of formalizing parts of ICCP protocol and analyze and address the potential security issues found within those parts. We develop model of the protocol in a model checking tool called UPPAAL and then use Computation Tree Logic (CTL) properties over this model to see if they are valid. Once a problem is identified, we design a checker that can detect exploitation of the identified vulnerabilities. The soundness of these checkers is then verified by validating properties on the system in conjunction with this new checker.","Item withdrawn by Mark Zulauf (zulauf@illinois.edu) on 2013-04-22T21:26:21Z Item was in collections: University of Illinois Theses & Dissertations (ID: 1) No. of bitstreams: 1 Malik_MuhammadSalman.pdf: 449451 bytes, checksum: f2564590c6ac6ad056df07efb2ee8831 (MD5)","Made available in DSpace on 2013-05-24T21:53:51Z (GMT). No. of bitstreams: 2 Muhammad Salman_Malik.pdf: 449451 bytes, checksum: f2564590c6ac6ad056df07efb2ee8831 (MD5) license.txt: 4071 bytes, checksum: c97d6bf41b64c5f0d855d30990afc382 (MD5)"],"dc:identifier":["http://hdl.handle.net/2142/44193"],"dc:language":["en"],"dc:rights":["Copyright 2013 Muhammad Salman Malik"],"dc:subject":["Security","UPPAAL","Inter Control Center Communication Protocol (ICCP)"],"dc:title":["Security analysis of inter control center communication protocol using model checking"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:25:33Z"}