Formal Specification of User Interfaces Bernhard Beckert and Gerd Beuster We examine formal requirements for the specification of security critical interactive applications. In the first part, we define operating system requirements for guaranteeing security against software based man-in-the-middle attacks on input/output facilities. In the second part, we formalize security relevant usability aspects of application design.