Formal Engineering of XACML Access Control Policies in VDM++

Jeremy W. Bryans, John S. Fitzgerald

    Research output: Chapter in Book/Report/Conference proceedingConference proceedingpeer-review

    14 Citations (Scopus)


    We present a formal, tool-supported approach to the design and maintenance of access control policies expressed in the eXtensible Access Control Markup Language (XACML). Our aim is to help developers evaluate the consequences of policy decisions in complex situations where security requirements change and access decisions may depend on the external dynamic environment. The approach applies the model-oriented specification language from the Vienna Development Method (VDM++). An executable formal model of XACML access control is presented in VDM++. The use of the model to analyse and revise both policies and requirements on the environment is illustrated through an example. An approach to the practical problem of analysing access control in virtual organisations with dynamic membership and goals is proposed.
    Original languageEnglish
    Title of host publicationFormal Methods and Software Engineering
    EditorsMichael Butler, Michael G. Hinchey, María M. Larrondo-Petrie
    Place of PublicationBerlin
    PublisherSpringer Verlag
    Number of pages20
    Volume4789 LNCS
    ISBN (Electronic)978-3-540-76650-6
    ISBN (Print)978-3-540-76648-3
    Publication statusPublished - 2007
    EventInternational Conference on Formal Engineering Methods - Boca Raton, United States
    Duration: 14 Nov 200715 Nov 2007
    Conference number: 9

    Publication series

    NameLecture Notes in Computer Science


    ConferenceInternational Conference on Formal Engineering Methods
    Abbreviated titleICFEM
    Country/TerritoryUnited States
    CityBoca Raton


    Dive into the research topics of 'Formal Engineering of XACML Access Control Policies in VDM++'. Together they form a unique fingerprint.

    Cite this