Formal Modelling of a Usable Identity Management Solution for Virtual Organisations

Ali N. Haidar
(University College London)
P. V. Coveney
(University College London)
Ali E. Abdallah
(London South Bank University)
P. Y. A Ryan
(University of Luxembourg)
B. Beckles
(University of Cambridge Computing Service)
J. M. Brooke
(University of Manchester)
M . A. S. Jones
(University of Manchester)

This paper attempts to accurately model security requirements for computational grid environments with particular focus on authentication. We introduce the Audited Credential Delegation (ACD) architecture as a solution to some of the virtual organisations identity management usability problems. The approach uses two complementary models: one is state based, described in Z notation, and the other is event-based, expressed in the Process Algebra of Hoare's Communicating Sequential Processes (CSP). The former will be used to capture the state of the WS and to model back-end operations on it whereas the latter will be used to model behavior, and in particular, front-end interactions and communications. The modelling helps to clearly and precisely understand functional and security requirements and provide a basis for verifying that the system meets its intended requirements.

In Jeremy Bryans and John Fitzgerald: Proceedings Second Workshop on Formal Aspects of Virtual Organisations (FAVO 2009), Eindhoven, The Netherlands, 3rd November 2009, Electronic Proceedings in Theoretical Computer Science 16, pp. 41–50.
Published: 29th January 2010.

ArXived at: http://dx.doi.org/10.4204/EPTCS.16.4 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org