Bounded-Deducibility Security (Invited Paper)

Andrei Popescu, Thomas Bauereiss, Peter Lammich

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

2 Citations (Scopus)
64 Downloads (Pure)


We describe Bounded-Deducibility (BD) security, an expressive framework for the specification and verification of information-flow security. The framework grew by confronting concrete challenges of specifying and verifying fine-grained confidentiality properties in some realistic web-based systems. The concepts and theorems that constitute this framework have an eventful history of such "confrontations", often involving trial and error, which are reported in previous papers. This paper is the first to focus on the framework itself rather than the case studies, gathering in one place all the abstract results about BD security.
Original languageEnglish
Title of host publication12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference)
EditorsLiron Cohen, Cezary Kaliszyk
Publication statusPublished - 21 Jun 2021
Event12th International Conference on Interactive Theorem Proving, ITP 2021 - Online Conference
Duration: 29 Jun 20211 Jul 2021
Conference number: 12


Conference12th International Conference on Interactive Theorem Proving, ITP 2021
Abbreviated titleITP 2021
CityOnline Conference


Dive into the research topics of 'Bounded-Deducibility Security (Invited Paper)'. Together they form a unique fingerprint.

Cite this