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.


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.


BSD License


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).


Session Bounded_Deducibility_Security