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


Theories of Bounded_Deducibility_Security