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

DOI10.1007/S10626-022-00369-1zbMATH Open1505.93002arXiv2102.06028OpenAlexW3198395630MaRDI QIDQ2106413FDOQ2106413

Authors: Shoma Matsui, Stéphane Lafortune 

Publication date: 14 December 2022

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

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.

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

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

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)

Cites Work

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

Cited In (2)

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

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)