Reasoning about XACML policies using CSP

ABSTRACT

In this work we explore the use of process algebra in formalising and analysing access control policies. We do this by considering a standard access control language (XACML) and show how the core concepts in the language can be represented in CSP. We then show how properties of these policies may also be described in CSP, and how model checking may be used to verify that a policy meets the property.We further consider how we may introduce a notion of workflow into this framework, and show that a simple appreciation of the workflow context may limit the things we need to verify about a policy.

REFERENCES

• 1: K. Bhargavan, C. Fournet, and A. Gordon. A Santics for Web Services Authentication. Theoretical Computer Science, 340(1):102--153,June 2005.
• 2: Sabrina De Capitani di Vimercati , Stefano Paraboschi , Pierangela Samarati, Access control: principles and solutions, Software—Practice & Experience, v.33 n.5, p.397-421, 25 April 2003 [doi>10.1002/spe.513]
• 3: Kathi Fisler , Shriram Krishnamurthi , Leo A. Meyerovich , Michael Carl Tschantz, Verification and change-impact analysis of access-control policies, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062502]
• 4: D. Guelev, M. Ryan, and P. Schobbens. Model-checking Access Control Policies. In ISC, 2004.
• 5: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 6: E Kleiner and A. W. Roscoe. Web Services Security: a preliminary study using Casper and FDR. In ARPSA, pages 160--174,2004.
• 7: Formal Systs (Europe)Ltd. Failures-Divergences Refinent: User Manual and Tutorial. Oxford University.
• 8: T. Moses. eXtensible Access Control Markup Language (XACML)version 1.0. Technical report, OASIS, Feb 2003.
• 9: A. W. Roscoe , C. A. R. Hoare , Richard Bird, The Theory and Practice of Concurrency, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 10: Peter Y. A. Ryan, Mathematical Models of Computer Security, Revised versions of lectures given during the IFIP WG 1.7 International School on Foundations of Security Analysis and Design on Foundations of Security Analysis and Design: Tutorial Lectures, p.1-62, September 01, 2000
• 11: Peter Ryan and Ragni Ryvold Arnesen. A Process Algebraic Approach to Security Policies. In Ehud Gudes and Sujeet Shenoi, editors, DBSec, volume 256 of IFIP Conference Proceedings, pages 301--312. Kluwer, 2002.
• 12: Peter Ryan, Steve Schneider, Michael Goldsmith, Gavin Lowe, and Bill Roscoe. Modelling and Analysis of Security Protocols. Pearson Education, 2001.
• 13: Steve Schneider , S. A. Schneider, Concurrent and Real Time Systems: The CSP Approach, John Wiley & Sons, Inc., New York, NY, 1999
• 14: Nan Zhang , Mark Ryan , Dimitar P. Guelev, Synthesising verified access control systems in XACML, Proceedings of the 2004 ACM workshop on Formal methods in security engineering, October 29-29, 2004, Washington DC, USA [doi>10.1145/1029133.1029141]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Specialized application languages
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Access controls

General Terms:
Security, Theory, Verification

Keywords:
CSP, XACML, access control, santic models