{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:46:38Z","timestamp":1755999998131,"version":"3.37.0"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2010,3,1]],"date-time":"2010-03-01T00:00:00Z","timestamp":1267401600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2010,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The access control problem in computer security is fundamentally concerned with the ability of system entities to see, make use of, or alter various system resources. We provide a mathematical framework for modelling and reasoning about (distributed) systems with access control. This is based on a calculus of resources and processes together with a Hennessy\u2013Milner-style modal logic, based on the connectives of bunched logic, for which an appropriate correspondence theorem obtains. As a consequence we get a consistent account of both operational behaviour and logical reasoning for systems with access control features. In particular, we are able to introduce a process combinator that describes, as a form of concurrent composition, the action of one agent in the role of another, and provide a logical characterization of this operator via a modality \u2018says\u2019. We give a range of examples, including analyses of co-signing, roles, and chains of trust, which illustrates the utility of our mathematical framework.<\/jats:p>","DOI":"10.1007\/s00165-009-0107-x","type":"journal-article","created":{"date-parts":[[2009,3,16]],"date-time":"2009-03-16T09:12:55Z","timestamp":1237194775000},"page":"83-104","source":"Crossref","is-referenced-by-count":12,"title":["Algebra and logic for access control"],"prefix":"10.1145","volume":"22","author":[{"given":"Matthew","family":"Collinson","sequence":"first","affiliation":[{"name":"Hewlett-Packard Laboratories, Long Down Avenue, BS34 8QZ, Stoke Gifford, Bristol, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pym","sequence":"additional","affiliation":[{"name":"Hewlett-Packard Laboratories, Long Down Avenue, BS34 8QZ, Stoke Gifford, Bristol, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abadi M (2003) Logic in access control. In: Proceedings of LICS\u201903 pp 228\u2013233","DOI":"10.1109\/LICS.2003.1210062"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/155183.155225"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Abadi M Gordon A (1997) A calculus for cryptographic protocols: the spi calculus. In: Proceedings conference Computer and Communications Security. ACM Press London pp 36\u201347","DOI":"10.1145\/266420.266432"},{"key":"e_1_2_1_2_4_2","unstructured":"Baldwin A Beres Y Casassa Mont M Griffin J Shiu S (2008) Identity analytics: using modeling and simulation to improve data security decision making. Technical Report HPL-2008-188 HP Labs 2008. http:\/\/www.hpl.hp.com\/techreports\/2008\/HPL-2008-188.html"},{"volume-title":"Managing information risk and the economics of security","year":"2008","author":"Beautement A","key":"e_1_2_1_2_5_2"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Beres Y Griffin J Shiu S Heitman M Markle D Ventura P (2008) Analysing the performance of security solutions to reduce vulnerability exposure window. In: Proceedings of 2008 annual computer security applications conference (ACSAC). IEEE","DOI":"10.1109\/ACSAC.2008.42"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4899-6685-8","volume-title":"Demos\u2014discrete event modelling on Simula","author":"Birtwistle G","year":"1979"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Becker MY Nanz S (2007) A logic for state-modifying authorization policies. In: 12th European symposium on research in computer security (ESORICS) Lecture Notes in Computer Science vol 4734","DOI":"10.1007\/978-3-540-74835-9_14"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.485845"},{"key":"e_1_2_1_2_10_2","unstructured":"Collinson M Monahan B Pym D (2008a) Located Demos2k\u2014towards a tool for modelling processes and distributed resources. Technical Report HPL-2008-76 HP Labs 2008. http:\/\/library.hp.com\/techpubs\/2008\/HPL-2008-76.html"},{"key":"e_1_2_1_2_11_2","unstructured":"Collinson M Monahan B Pym D (2008b) A logical and computational theory of located resource. Technical Report HPL-2008-74R1 HP Labs 2008 (Submitted). http:\/\/library.hp.com\/techpubs\/2008\/HPL-2008-74R1.html"},{"key":"e_1_2_1_2_12_2","unstructured":"Collinson M Monahan B Pym D (2008c) An update to located Demos2k. Technical Report HPL-2008-205 HP Labs 2008. http:\/\/library.hp.com\/techpubs\/2008\/HPL-2008-205.html"},{"key":"e_1_2_1_2_13_2","unstructured":"Collinson M Pym D (2009) Algebra and logic for resource-based systems modelling. Technical Report HPL-2009-21 HP Labs 2009 (Submitted). http:\/\/library.hp.com\/techpubs\/2009\/HPL-2009-10.html."},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Collinson M Pym D Tofts C (2007) Errata for formal aspects of computing (2006) 18:495\u2013517 and their consequences. Formal Aspects Comput 19(4):551\u2013554","DOI":"10.1007\/s00165-007-0047-2"},{"key":"e_1_2_1_2_15_2","unstructured":"Demos2k. http:\/\/www.demos2k.org"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"DeTreville J (2002) Binder a logic-based security language. In: Proceedings of 2002 IEEE symposium on security and privacy pp 105\u2013113","DOI":"10.1109\/SECPRI.2002.1004365"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Guelev DP Ryan MD Schobbens P-Y (2004) Model-checking access control policies. In: Seventh information security conference (ISC\u201904) Lecture Notes in Computer Science vol 3225. Springer Heidelberg","DOI":"10.1007\/978-3-540-30144-8_19"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Ishtiaq S O\u2019Hearn PW (2001) BI as an assertion language for mutable data structures. In: Proceedings of POPL 2001. ACM London pp 14\u201326","DOI":"10.1145\/373243.375719"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Kamoda H Yamaoka M Matsuda S Broda K Sloman M (2006) Access control policy analysis using free variable tableaux. Information Processing Society of Japan (IPSJ) Digital Courier vol 2","DOI":"10.2197\/ipsjdc.2.207"},{"issue":"10","key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1145\/138873.138874","article-title":"Authentication in distributed systems: theory and practice","volume":"4","author":"Lampson B","year":"1992","journal-title":"ACM Trans Comput Syst"},{"key":"e_1_2_1_2_23_2","unstructured":"Lampson BW (1971) Protection. In: Proceedings of fifth Princeton symposium information sciences and systems pp 437\u2013443"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Li N Wang Q (2008) Beyond separation of duty: An algebra for specifying high-level security policies. J ACM 55(3)","DOI":"10.1145\/1379759.1379760"},{"volume-title":"A calculus of communicating systems, Lecture Notes in Computer Science, vol 92","year":"1980","author":"Milner R","key":"e_1_2_1_2_25_2"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90114-7"},{"volume-title":"Communication and concurrency","year":"1989","author":"Milner R","key":"e_1_2_1_2_27_2"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.2307\/421090"},{"key":"e_1_2_1_2_30_2","first-page":"17","article-title":"Structural operational semantics","volume":"60","author":"Plotkin GD","year":"2004","journal-title":"J Logic Algebraic Program"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0018-z"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Pym D Tofts C (2007) Systems modelling via resources and processes: philosphy calculus semantics and logic. In: Cardelli L Fiore M Winskel G (eds) Computation meaning and logic: articles dedicated to Gordon Plotkin Electronic Notes in Theoretical Computer Science vol 107. Elsevier Amsterdam pp 545\u2013587. Errata in [CPT07]","DOI":"10.1016\/j.entcs.2007.02.020"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Pym D (1999) On bunched predicate logic. In: Proceedings of LICS\u201999 pp 183\u2013192. IEEE New York","DOI":"10.1109\/LICS.1999.782614"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Pym DJ (2002) The semantics and proof theory of the logic of bunched implications Applied Logic Series vol 26. Kluwer Dordrecht. Errata at: http:\/\/www.cs.bath.ac.uk\/~pym\/BI-monograph-errata.pdf","DOI":"10.1007\/978-94-017-0091-7"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: Proceedings of LICS\u201902. IEEE New York pp 55\u201374","DOI":"10.1109\/LICS.2002.1029817"},{"volume-title":"The modelling and analysis of security protocols","year":"2001","author":"Ryan P","key":"e_1_2_1_2_37_2"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Schneider S (1996) Security properties and CSP. In: IEEE symposium on security and privacy pp 174\u2013187","DOI":"10.1109\/SECPRI.1996.502680"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1016\/j.tcs.2005.10.044","article-title":"A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols","volume":"353","author":"Scedrov A","year":"2006","journal-title":"Theor Comput Scie"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/PROC.1975.9939"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"publisher","DOI":"10.5555\/500817"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-009-0107-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-009-0107-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-009-0107-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T11:27:28Z","timestamp":1739014048000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-009-0107-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,3]]}},"alternative-id":["10.1007\/s00165-009-0107-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-009-0107-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2010,3]]}}}