  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.
