Modelling trusted web applications

In this paper we model message exchange in a trusted multi-agent system (MAS). Modelling such MAS allows us to study and analyse agents’ behaviour. We apply our model in context where secure agent communication is paramount, i.e. within the context of data-sensitive and time-sensitive web-applications. As a result we aim to reduce design errors of such applications, analyse agents’ behaviour in secure and compromised web applications and consequently improve security, reliability and usability.

We use model checking to study the pattern of message exchange among agents. As a verification technique, model checking assists in finding flaws and simplifying the design of an application. We simulate a secure transaction between a client and a server. Our model is realistic; we augment it by introducing discrete time, web-session management, and authentication.