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.