Trustworthy Systems

A demonic lattice of information


Carroll Morgan




Landuaer and Redmond’s Lattice of Information was an early and influential formalisation of the pure structure of security [8]: a partial order was defined for information-flow from a hidden state. In modern terms we would say that more-security refines less-security. For Landauer, the deterministic case [op. cit.], the refinement order is a lattice. Very recently [9,3] a similar approach has been taken to purely probabilistic systems and there too a refinement order can be defined; but it is not a lattice [12]. In between deterministic and probabilistic is demonic, where behaviour is not deterministic but also not quantifiable. We show that our own earlier approach to this [15,16] fits into the same pattern as deterministic and probabilistic, and illustrate that with results concerning compositionality, testing, soundness and completeness. Finally, we make some remarks about source-level reasoning.

BibTeX Entry

    author           = {Morgan, Carroll},
    booktitle        = {Concurrency, Security, and Puzzles --- Essays Dedicated to Andrew William Roscoe on the Occasion of
                        His 60th Birthday},
    doi              = {987-3-319-51045-3},
    month            = jan,
    pages            = {203--222},
    paperurl         = {},
    publisher        = {Springer},
    series           = {Lecture Notes in Computer Science},
    title            = {A Demonic Lattice of Information},
    volume           = {10160},
    year             = {2017}