Synthesis of winning attacks on communication protocols using supervisory control theory: two case studies

DOI10.1007/S10626-022-00369-1MaRDI QIDQ2106413zbMATH OpenOpenAlexFDO

Authors Shoma Matsui, Stéphane Lafortune

Publication date 14 December 2022

Published in Discrete Event Dynamic Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2102.06028

zbMATH Keywords

supervisory controldistributed protocolsalternating bit protocoltransmission control protocolperson-in-the-middle attacks

Mathematics Subject Classification ID

Hierarchical systems (93A13) Discrete event control/observation systems (93C65) Computer security (68M25)

Abstract: There is an increasing need to study the vulnerability of communication protocols in distributed systems to malicious attacks that attempt to violate properties such as safety or nonblockingness. In this paper, we propose a common methodology for formal synthesis of successful attacks against two well-known protocols, the Alternating Bit Protocol (ABP) and the Transmission Control Protocol (TCP), where the attacker can always eventually win, called For-all attacks. This generalizes previous work on the synthesis of There-exists attacks for TCP, where the attacker can sometimes win. We model the ABP and TCP protocols and system architecture by finite-state automata and employ the supervisory control theory of discrete event systems to pose and solve the synthesis of For-all attacks, where the attacker has partial observability and controllability of the system events. We consider several scenarios of person-in-themiddle attacks against ABP and TCP and present the results of attack synthesis using our methodology for each case.

Recommendations

• The synthesis of communication protocols
• Automated Technology for Verification and Analysis
• scientific article; zbMATH DE number 177251
• A Framework for the Analysis of Supervised Discrete Event Systems Under Attack
• Synthesis of sensor deception attacks at the supervisory layer of cyber-physical systems

Cites work

• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A discrete event systems approach for protocol conversion
• Detection and mitigation of classes of attacks in supervisory control systems
• Formulas for calculating supremal controllable and normal sublanguages
• Introduction to Discrete Event Systems
• On supremal languages of classes of sublanguages that arise in supervisor synthesis problems with partial observation
• Supervisor synthesis to thwart cyber attack with bounded sensor reading alterations
• Supervisory control and reactive synthesis: a comparative introduction
• Supervisory control of discrete-event systems
• Supervisory control of discrete-event systems under attacks
• Synthesis of Maximally Permissive Supervisors for Partially-Observed Discrete-Event Systems
• Synthesis of Supervisors Robust Against Sensor Deception Attacks
• Synthesis of covert actuator attackers for free
• Synthesis of sensor deception attacks at the supervisory layer of cyber-physical systems
• Synthesis of winning attacks on communication protocols using supervisory control theory: two case studies

Cited in

(2)

• Diagnosability and attack detection for discrete event systems under sensor attacks
• Synthesis of winning attacks on communication protocols using supervisory control theory: two case studies

Describes a project that uses

Uses Software

• UMDES
• GitHub

This page was built for publication: Synthesis of winning attacks on communication protocols using supervisory control theory: two case studies

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2106413)