From Knowledge to Action: Logics of Permitted and Obligatory Announcements

Abstract

We formalize the notions of “permitted and obligatory announcements” in the context of information security, such as privacy policy compliance. In a sender-receiver setting, we define the sender’s permitted and obligatory announcements in terms of the receiver’s ideal epistemic states (i.e., the epistemic states that comply with the given security policies). We propose two logics, LPOA and DLPOA, to reason about permitted and obligatory announcements in static and dynamic contexts, respectively. These two logics are completely axiomatized, and we also study generalizations in which the receiver’s knowledge is characterized by non-S5 logics. Our paper makes two main contributions to the formalization of permitted and obligatory announcements: First, we clarify the interplay between the sender’s permitted and obligatory announcements and the receiver’s knowledge. Second, we distinguish between weakly and strongly permitted announcements.