Bounded-Deducibility Security

Andrei Popescu 🌐, Peter Lammich 🌐 and Thomas Bauereiss 📧

April 22, 2014

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

This is a formalization of bounded-deducibility security (BD security), a flexible notion of information-flow security applicable to arbitrary transition systems. It generalizes Sutherland's classic notion of nondeducibility by factoring in declassification bounds and trigger, whereas nondeducibility states that, in a system, information cannot flow between specified sources and sinks, BD security indicates upper bounds for the flow and triggers under which these upper bounds are no longer guaranteed.

License

BSD License

History

August 12, 2021
Generalised BD Security from I/O automata to nondeterministic transition systems, with the former retained as an instance of the latter (renaming locale BD_Security to BD_Security_IO). Generalise unwinding conditions to allow making more than one transition at a time when constructing alternative traces. Add results about the expressivity of declassification triggers vs. bounds, due to Thomas Bauereiss (added as author).

Topics

Session Bounded_Deducibility_Security

Used by

Cite

× 
@article{Bounded_Deducibility_Security-AFP,
  author  = {Andrei Popescu and Peter Lammich and Thomas Bauereiss},
  title   = {Bounded-Deducibility Security},
  journal = {Archive of Formal Proofs},
  month   = {April},
  year    = {2014},
  note    = {\url{https://isa-afp.org/entries/Bounded_Deducibility_Security.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: