2026-07-24T06:07:34Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13898 2024-03-06T10:53:05Z ddc:004 open_access

Bounded-Deducibility Security (Invited Paper) Popescu, Andrei Bauereiss, Thomas Lammich, Peter Information-flow security Unwinding proof method Compositionality Verification 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andrei Popescu and Thomas Bauereiss and Peter Lammich 2021 Is Part Of LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2021.3 urn:nbn:de:0030-drops-138982 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.3 eng https://creativecommons.org/licenses/by/4.0/legalcode