Formal Engineering of XACML Access Control Policies in VDM++

Jeremy W. Bryans; John S. Fitzgerald

doi:10.1007/978-3-540-76650-6_4

Formal Engineering of XACML Access Control Policies in VDM++

Jeremy W. Bryans, John S. Fitzgerald

Newcastle University

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

14 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 language	English
Title of host publication	Formal Methods and Software Engineering
Editors	Michael Butler, Michael G. Hinchey, María M. Larrondo-Petrie
Place of Publication	Berlin
Publisher	Springer Verlag
Pages	37-56
Number of pages	20
Volume	4789 LNCS
ISBN (Electronic)	978-3-540-76650-6
ISBN (Print)	978-3-540-76648-3
DOIs	https://doi.org/10.1007/978-3-540-76650-6_4
Publication status	Published - 2007
Event	International Conference on Formal Engineering Methods - Boca Raton, United States Duration: 14 Nov 2007 → 15 Nov 2007 Conference number: 9

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	4789

Conference

Conference	International Conference on Formal Engineering Methods
Abbreviated title	ICFEM
Country/Territory	United States
City	Boca Raton
Period	14/11/07 → 15/11/07

Access to Document

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

Cite this

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 proceeding › Conference proceeding › peer-review

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

@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",

note = "International Conference on Formal Engineering Methods, ICFEM ; Conference date: 14-11-2007 Through 15-11-2007",

}

TY - GEN

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

AU - Bryans, Jeremy W.

AU - Fitzgerald, John S.

N1 - Conference code: 9

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

T2 - International Conference on Formal Engineering Methods

Y2 - 14 November 2007 through 15 November 2007

ER -

Formal Engineering of XACML Access Control Policies in VDM++

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this