Synthesising verified access control systems in XACML. - Nan Zhang 003; Mark Ryan 001; Dimitar P. Guelev (FMSE, 2004)

Evaluating Access Control Policies Through Model Checking. - Nan Zhang 003; Mark Ryan 001; Dimitar P. Guelev (ISC, 2005)

Generating verified access control policies through model-checking. - Nan Zhang 003 (2005)

Synthesising verified access control systems through model checking. - Nan Zhang 003; Mark Ryan 001; Dimitar P. Guelev (J. Comput. Secur., 2008)