
\section{Introduction}

This is a formalization of {\em Bounded-Deducibility Security} ({\em BD Security}),
a flexible notion of information-flow security applicable to arbitrary transition systems.
It generalizes Sutherland's classic notion of
nondeducibility~\cite{sutherland-modelOfInf} by factoring in declassification bounds and triggers---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.

\par \ \par
BD Security was introduced in~\cite{cocon-CAV2014}, where an application to the verification of a conference management called CoCon
system is also presented.
%
The framework is further discussed in detail in \cite{cocon-JAR2021}
and \cite{BDsecurity-ITP2021}.

Other verification case studies of BD Security are discussed
in \cite{cosmed-itp2016,cosmed-jar2018} and \cite{cosmedis-SandP2017}.

