文摘

We are interested in formal modelling and verification of security ceremonies. Considerable efforts have been put into verifying security protocols, with quite successful tools currently being widely used. The relatively recent concept of security ceremonies, introduced by Carl Ellison, increases the complexity of protocol analysis in several directions: a ceremony should include all relevant out-of-bad assumptions, should compose protocols, and should include the human agent. Work on modelling human agents as part of IT systems is quite limited, and the few existing studies come from psychology or sociology. A step towards understanding how to model and analyse security ceremonies is to integrate a model of human agents with models for protocols (or combination of protocols). Current works essentially model human agent interaction with a user interface as a nondeterministic process. In this paper we propose a more realistic model which includes more information about the user interaction, obtained by sociologists usually through experiments and observation, and model the actions of a human agent as a probabilistic process. An important point that we make in this paper is to separate the model of the human and the model of the user interface, and to provide a “compilation-operation putting the two together and encoding the interaction between the human and the interface. We base our work on a recently proposed model for security ceremonies, which we call the Bella-Coles-Kemp model.