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 liveness. 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.

By admin