Formal Engineering of XACML Access Control Policies in VDM++

Jeremy W. Bryans, John S. Fitzgerald

    Research output: Chapter in Book/Report/Conference proceedingConference proceeding

    11 Citations (Scopus)

    Abstract

    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
    Pages37-56
    Number of pages20
    Volume4789 LNCS
    ISBN (Electronic)978-3-540-76650-6
    ISBN (Print)978-3-540-76648-3
    DOIs
    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
    PublisherSpringer
    Volume4789

    Conference

    ConferenceInternational Conference on Formal Engineering Methods
    Abbreviated titleICFEM
    CountryUnited States
    CityBoca Raton
    Period14/11/0715/11/07

    Fingerprint

    Specification languages
    Access control
    Markup languages

    Cite this

    Bryans, J. W., & Fitzgerald, J. S. (2007). Formal Engineering of XACML Access Control Policies in VDM++. In M. Butler, M. G. Hinchey, & M. M. Larrondo-Petrie (Eds.), Formal Methods and Software Engineering (Vol. 4789 LNCS, pp. 37-56). (Lecture Notes in Computer Science; Vol. 4789). Berlin: Springer Verlag. https://doi.org/10.1007/978-3-540-76650-6_4

    Formal Engineering of XACML Access Control Policies in VDM++. / Bryans, Jeremy W.; Fitzgerald, John S.

    Formal Methods and Software Engineering. ed. / Michael Butler; Michael G. Hinchey; María M. Larrondo-Petrie. Vol. 4789 LNCS Berlin : Springer Verlag, 2007. p. 37-56 (Lecture Notes in Computer Science; Vol. 4789).

    Research output: Chapter in Book/Report/Conference proceedingConference proceeding

    Bryans, JW & Fitzgerald, JS 2007, Formal Engineering of XACML Access Control Policies in VDM++. in M Butler, MG Hinchey & MM Larrondo-Petrie (eds), Formal Methods and Software Engineering. vol. 4789 LNCS, Lecture Notes in Computer Science, vol. 4789, Springer Verlag, Berlin, pp. 37-56, International Conference on Formal Engineering Methods, Boca Raton, United States, 14/11/07. https://doi.org/10.1007/978-3-540-76650-6_4
    Bryans JW, Fitzgerald JS. Formal Engineering of XACML Access Control Policies in VDM++. In Butler M, Hinchey MG, Larrondo-Petrie MM, editors, Formal Methods and Software Engineering. Vol. 4789 LNCS. Berlin: Springer Verlag. 2007. p. 37-56. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-540-76650-6_4
    Bryans, Jeremy W. ; Fitzgerald, John S. / Formal Engineering of XACML Access Control Policies in VDM++. Formal Methods and Software Engineering. editor / Michael Butler ; Michael G. Hinchey ; María M. Larrondo-Petrie. Vol. 4789 LNCS Berlin : Springer Verlag, 2007. pp. 37-56 (Lecture Notes in Computer Science).
    @inproceedings{ffc1b051493349b285dc0ee4d103d5b6,
    title = "Formal Engineering of XACML Access Control Policies in VDM++",
    abstract = "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.",
    author = "Bryans, {Jeremy W.} and Fitzgerald, {John S.}",
    year = "2007",
    doi = "10.1007/978-3-540-76650-6_4",
    language = "English",
    isbn = "978-3-540-76648-3",
    volume = "4789 LNCS",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer Verlag",
    pages = "37--56",
    editor = "Michael Butler and Hinchey, {Michael G.} and Larrondo-Petrie, {Mar{\'i}a M.}",
    booktitle = "Formal Methods and Software Engineering",
    address = "Austria",

    }

    TY - GEN

    T1 - Formal Engineering of XACML Access Control Policies in VDM++

    AU - Bryans, Jeremy W.

    AU - Fitzgerald, John S.

    PY - 2007

    Y1 - 2007

    N2 - 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.

    AB - 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.

    U2 - 10.1007/978-3-540-76650-6_4

    DO - 10.1007/978-3-540-76650-6_4

    M3 - Conference proceeding

    SN - 978-3-540-76648-3

    VL - 4789 LNCS

    T3 - Lecture Notes in Computer Science

    SP - 37

    EP - 56

    BT - Formal Methods and Software Engineering

    A2 - Butler, Michael

    A2 - Hinchey, Michael G.

    A2 - Larrondo-Petrie, María M.

    PB - Springer Verlag

    CY - Berlin

    ER -