A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces Bernhard Beckert and Gerd Beuster We present a methodology for the formalization of human-computer interaction under security aspects. As part of the methodology, we give formal semantics for the well-known GOMS methodology for user modeling, and we provide a formal definition of human-computer interaction security. We show how formal GOMS models can be augmented with formal models of (1) the application and (2) the user's assumptions about the application. In combination, this allows the pervasive formal modeling of and reasoning about secure human-computer interaction.