<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE article PUBLIC "-//TaxonX//DTD Taxonomic Treatment Publishing DTD v0 20100105//EN" "../../nlm/tax-treatment-NS0.dtd">
<article xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:tp="http://www.plazi.org/taxpub" article-type="research-article" dtd-version="3.0" xml:lang="en">
  <front>
    <journal-meta>
      <journal-id journal-id-type="publisher-id">109</journal-id>
      <journal-id journal-id-type="index">urn:lsid:arphahub.com:pub:3dc5f44e-8666-58db-bc76-a455210e8891</journal-id>
      <journal-title-group>
        <journal-title xml:lang="en">JUCS - Journal of Universal Computer Science</journal-title>
        <abbrev-journal-title xml:lang="en">jucs</abbrev-journal-title>
      </journal-title-group>
      <issn pub-type="ppub">0948-695X</issn>
      <issn pub-type="epub">0948-6968</issn>
      <publisher>
        <publisher-name>Journal of Universal Computer Science</publisher-name>
      </publisher>
    </journal-meta>
    <article-meta>
      <article-id pub-id-type="doi">10.3217/jucs-013-08-1073</article-id>
      <article-id pub-id-type="publisher-id">28837</article-id>
      <article-categories>
        <subj-group subj-group-type="heading">
          <subject>Research Article</subject>
        </subj-group>
        <subj-group subj-group-type="scientific_subject">
          <subject>D.2.4 - Software/Program Verification</subject>
          <subject>F.3.1 - Specifying and Verifying and Reasoning about Programs</subject>
        </subj-group>
      </article-categories>
      <title-group>
        <article-title>Specification and Refinement of Access Control</article-title>
      </title-group>
      <contrib-group content-type="authors">
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Méry</surname>
            <given-names>Dominique</given-names>
          </name>
          <email xlink:type="simple">dominique.mery@loria.fr</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Merz</surname>
            <given-names>Stephan</given-names>
          </name>
          <xref ref-type="aff" rid="A2">2</xref>
        </contrib>
      </contrib-group>
      <aff id="A1">
        <label>1</label>
        <addr-line content-type="verbatim">Nancy University &amp; LORIA, Nancy, France</addr-line>
        <institution>Nancy University &amp; LORIA</institution>
        <addr-line content-type="city">Nancy</addr-line>
        <country>France</country>
      </aff>
      <aff id="A2">
        <label>2</label>
        <addr-line content-type="verbatim">INRIA Nancy &amp; LORIA, Nancy, France</addr-line>
        <institution>INRIA Nancy &amp; LORIA</institution>
        <addr-line content-type="city">Nancy</addr-line>
        <country>France</country>
      </aff>
      <author-notes>
        <fn fn-type="corresp">
          <p>Corresponding author: Dominique Méry (<email xlink:type="simple">dominique.mery@loria.fr</email>).</p>
        </fn>
        <fn fn-type="edited-by">
          <p>Academic editor: </p>
        </fn>
      </author-notes>
      <pub-date pub-type="collection">
        <year>2007</year>
      </pub-date>
      <pub-date pub-type="epub">
        <day>28</day>
        <month>08</month>
        <year>2007</year>
      </pub-date>
      <volume>13</volume>
      <issue>8</issue>
      <fpage>1073</fpage>
      <lpage>1093</lpage>
      <uri content-type="arpha" xlink:href="http://openbiodiv.net/B8C7B6CE-23C9-51B2-9EBB-CCCADEF469F4">B8C7B6CE-23C9-51B2-9EBB-CCCADEF469F4</uri>
      <uri content-type="zenodo_dep_id" xlink:href="https://zenodo.org/record/6999900">6999900</uri>
      <permissions>
        <copyright-statement>Dominique Méry, Stephan Merz</copyright-statement>
        <license license-type="creative-commons-attribution" xlink:href="" xlink:type="simple">
          <license-p>This article is freely available under the J.UCS Open Content License.</license-p>
        </license>
      </permissions>
      <abstract>
        <label>Abstract</label>
        <p>We consider the extension of fair event system specifications by concepts of access control (prohibitions, user rights, and obligations). We give proof rules for verifying that an access control policy is correctly implemented in a system, and consider preservation of access control by refinement of event systems. Prohibitions and obligations are expressed as properties of traces and are preserved by standard refinement notions of event systems. Preservation of user rights is not guaranteed by construction; we propose to combine implementation-level user rights and obligations to implement high-level user rights.</p>
      </abstract>
    </article-meta>
  </front>
</article>
