(*<*) theory Bounded_Deducibility_Security imports (* Preliminaries *) Filtermap Transition_System IO_Automaton (* Definitions *) BD_Security_IO BD_Security_Triggers (* Proof methods *) Compositional_Reasoning begin end (*>*)