Synthesis of Winning Attacks on Communication Protocols using Supervisory Control Theory: Two Case Studies

TL;DR

This paper introduces a formal methodology using supervisory control theory to synthesize successful, always-winning attacks on communication protocols like ABP and TCP, considering various attack scenarios.

Contribution

It presents a unified approach for synthesizing For-all attacks on communication protocols using finite-state automata and supervisory control theory, extending previous work on TCP attacks.

Findings

Successfully synthesized attacks for ABP and TCP protocols.

Demonstrated attack synthesis under partial observability and controllability.

Validated methodology across multiple attack scenarios.

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.