  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.
