There is an increasing need to study the vulnerability of communication protocols in distributed systems to malicious attacks that attempt to violate safety or liveness properties. In this paper, we propose a general methodology for formal synthesis of successful attacks against protocols where the attacker always eventually wins, called For-all attacks. This generalizes previous work on the synthesis of There-exists attacks, where the attacker can sometimes win. As we model protocols and system architectures by finite-state automata, our methodology employs the supervisory control theory of discrete event systems, which is well suited to pose and the synthesis of For-all attacks where the attacker has partial observability and controllability of the system events. We demonstrate our methodology using examples of man-in-the-middle attacks against the Alternating Bit Protocol and the Transmission Control Protocol.
View on arXiv