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

http://afp.sourceforge.net/entries/Bounded_Deducibility_Security.shtml

Enjoy!




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