  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.
