[isabelle] New AFP entry: Bounded-Deducibility Security

Bounded-Deducibility Security
Andrei Popescu and Peter Lammich

This is a formalization of bounded-deducibility security (BD security), a
flexible notion of information-flow security applicable to arbitrary
input-output automata. 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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.