Reasoning about security properties involves reasoning about where the information of a system is located, and how it evolves over time. While most security analysis techniques need to cope with some notions of information locality and knowledge propagation, usually they do not provide a general language for expressing arbitrary properties involving local knowledge and knowledge transfer. Building on this observation, we introduce a framework for security protocol analysis based on dynamic spatial logic specifications. Our computational model is a variant of existing pi-calculi, while specifications are expressed in a dynamic spatial logic extended with an epistemic operator. We present the syntax and semantics of the model and logic, and discuss the expressiveness of the approach, showing it complete for passive attackers. We also prove that generic Dolev-Yao attackers may be mechanically determined for any deterministic finite protocol, and discuss how this result may be used to reason about security properties of open systems. We also present a model-checking algorithm for our logic, which has been implemented as an extension to the SLMC system.
The formal analysis of security protocols is a challenging field, with various approaches being studied nowadays. The famous Burrows-Abadi-Needham Logic was the first logical system aiming to validate security protocols. Combining ideas from previous approaches, in this paper we define a complete system of dynamic epistemic logic for modeling security protocols. Our logic is implemented, and few of its properties are verifyied, using the theorem prover Lean.
In process algebras, security properties are expressed as equivalences between processes, but which equivalence is suitable is not clear. This means that there is a gap between an intuitive security notion and the formulation. Appropriate formalization is essential for verification, and our purpose is bridging this gap. By chasing scope extrusions, we prove that trace equivalence is congruent. Moreover, we construct an epistemic logic for the applied pi calculus and show that its logical equivalence agrees with the trace equivalence. We use the epistemic logic to show that trace equivalence is…
Recent ideas about epistemic modals and indicative conditionals in formal semantics have significant overlap with ideas in modal logic and dynamic epistemic logic. The purpose of this paper is to show how greater interaction between formal semantics and dynamic epistemic logic in this area can be of mutual benefit. In one direction, we show how concepts and tools from modal logic and dynamic epistemic logic can be used to give a simple, complete axiomatization of Yalcin's [16] semantic consequence relation for a language with epistemic modals and indicative conditionals. In the other direction…
We derive a Prolog theorem prover for an Intuitionistic Epistemic Logic by starting from the sequent calculus {\bf G4IP} that we extend with operator definitions providing an embedding in intuitionistic propositional logic ({\bf IPC}). With help of a candidate definition formula generator, we discover epistemic operators for which axioms and theorems of Artemov and Protopopescu's {\em Intuitionistic Epistemic Logic} ({\bf IEL}) hold and formulas expected to be non-theorems fail. We compare the embedding of {\bf IEL} in {\bf IPC} with a similarly discovered successful embedding of Dosen's doubl…
Logic $L$ was introduced by Lewitzka [7] as a modal system that combines intuitionistic and classical logic: $L$ is a conservative extension of CPC and it contains a copy of IPC via the embedding $φ\mapsto\squareφ$. In this article, we consider $L3$, i.e. $L$ augmented with S3 modal axioms, define basic epistemic extensions and prove completeness w.r.t. algebraic semantics. The resulting logics combine classical knowledge and belief with intuitionistic truth. Some epistemic laws of Intuitionistic Epistemic Logic studied by Artemov and Protopopescu [1] are reflected by classical modal principle…
This work proposes a Dynamic Epistemic Logic with Communication Actions that can be performed concurrently. Unlike Concurrent Epistemic Action Logic introduced by Ditmarsch, Hoek and Kooi, where the concurrency mechanism is the so called true concurrency, here we use an approach based on process calculus, like CCS and CSP, and Action Models Logic. Our approach makes possible the proof of soundness, completeness and decidability, different from the others approaches. We present an axiomatization and show that the proof of soundness, completeness and decidability can be done using a reduction me…
In this paper, we introduce $\textit{partial}$ dependency modality $\mathcal{D}$ into epistemic logic so as to reason about $\textit{partial}$ dependency relationship in Kripke models. The resulted dependence epistemic logic possesses decent expressivity and beautiful properties. Several interesting examples are provided, which highlight this logic's practical usage. The logic's bisimulation is then discussed, and we give a sound and strongly complete axiomatization for a sub-language of the logic.
Verifiers and Generators: Epistemic Semantics for Intuitionistic Logic (Long Version)
Universidad Nacional de Quilmes (CONICET)（基尔梅斯国立大学（国家科学研究和技术委员会））；Departamento de Computación, Facultad de Ciencias Exactas y Naturales, Universidad de Buenos Aires（布宜诺斯艾利斯大学自然科学学院计算系）
Dynamic Epistemic Logic (DEL) is a logic that models information change in a multi-agent setting through the use of action models with pre- and post-conditions. In a recent work, DEL has been extended to first-order epistemic logic (DFOEL), with a proof that the resulting Epistemic Planning Problem is decidable, as long as action models pre- and post-conditions are non-modal and the first-order domain is finite. Our contribution highlights the role post-conditions have in DFOEL. We show that the Epistemic Planning Problem with possibly infinite first-order domains is undecidable if the non-mod…
In this paper, we present an alternative interpretation of propositional inquisitive logic as an epistemic logic of knowing how. In our setting, an inquisitive logic formula $α$ being supported by a state is formalized as "knowing how to resolve $α$" (more colloquially, "knowing how $α$ is true") holds on the S5 epistemic model corresponding to the state. Based on this epistemic interpretation, we use a dynamic epistemic logic with both know-how and know-that operators to capture the epistemic information behind the innocent-looking connectives in inquisitive logic. We show that the set of val…
This paper revisits the multi-agent epistemic logic presented in [10], where agents and sets of agents are replaced by abstract, intensional "names". We make three contributions. First, we study its model theory, providing adequate notions of bisimulation and frame morphisms, and use them to study the logic's expressive power and definability. Second, we show that the logic has a natural neighborhood semantics, which in turn allows to show that the axiomatization in [10] does not rely on possibly controversial introspective properties of knowledge. Finally, we extend the logic with common and …
This paper presents an extension of temporal epistemic logic with operators that quantify over agent strategies. Unlike previous work on alternating temporal epistemic logic, the semantics works with systems whose states explicitly encode the strategy being used by each of the agents. This provides a natural way to express what agents would know were they to be aware of some of the strategies being used by other agents. A number of examples that rely upon the ability to express an agent's knowledge about the strategies being used by other agents are presented to motivate the framework, includi…
We present a substructural epistemic logic, based on Boolean BI, in which the epistemic modalities are parametrized on agents' local resources. The new modalities can be seen as generalizations of the usual epistemic modalities. The logic combines Boolean BI's resource semantics --- we introduce BI and its resource semantics at some length --- with epistemic agency. We illustrate the use of the logic in systems modelling by discussing some examples about access control, including semaphores, using resource tokens. We also give a labelled tableaux calculus and establish soundness and completene…
IRIT University of Toulouse（图卢兹大学IRIT研究所）；CNRS（法国国家科学研究中心）；Universität Potsdam（波茨坦大学）
In a recent line of research, two familiar concepts from logic programming semantics (unfounded sets and splitting) were extrapolated to the case of epistemic logic programs. The property of epistemic splitting provides a natural and modular way to understand programs without epistemic cycles but, surprisingly, was only fulfilled by Gelfond's original semantics (G91), among the many proposals in the literature. On the other hand, G91 may suffer from a kind of self-supported, unfounded derivations when epistemic cycles come into play. Recently, the absence of these derivations was also formalis…
We introduce a new semantics for a logic of explicit and implicit beliefs based on the concept of multi-agent belief base. Differently from existing Kripke-style semantics for epistemic logic in which the notions of possible world and doxastic/epistemic alternative are primitive, in our semantics they are non-primitive but are defined from the concept of belief base. We provide a complete axiomatization and prove decidability for our logic via a finite model argument. We also provide a polynomial embedding of our logic into Fagin & Halpern's logic of general awareness and establish a complexit…
In this paper we consider Epistemic Logic Programs, which extend Answer Set Programming (ASP) with "epistemic operators" and "epistemic negation", and a recent approach to the semantics of such programs in terms of World Views. We propose some observations on the existence and number of world views. We show how to exploit an extended ASP semantics in order to: (i) provide a characterization of world views, different from existing ones; (ii) query world views and query the whole set of world views.
Dynamic Epistemic Logic (DEL) is a logical framework in which one can describe in great detail how actions are perceived by the agents, and how they affect the world. DEL games were recently introduced as a way to define classes of games with imperfect information where the actions available to the players are described very precisely. This framework makes it possible to define easily, for instance, classes of games where players can only use public actions or public announcements. These games have been studied for reachability objectives, where the aim is to reach a situation satisfying some …
This paper aims to give an epistemic interpretation to the tensor disjunction in dependence logic, through a rather surprising connection to the so-called weak disjunction in Medvedev's early work on intermediate logic under the Brouwer-Heyting-Kolmogorov (BHK)-interpretation. We expose this connection in the setting of inquisitive logic with tensor disjunction discussed by Ciardelli and Barbero (2019}, but from an epistemic perspective. More specifically, we translate the propositional formulae of inquisitive logic with tensor into modal formulae in a powerful epistemic language of "knowing h…
Logics for social networks have been studied in recent literature. This paper presents a framework based on *dynamic term-modal logic* (DTML), a quantified variant of dynamic epistemic logic (DEL). In contrast with DEL where it is commonly known to whom agent names refer, DTML can represent dynamics with uncertainty about agent identity. We exemplify dynamics where such uncertainty and de re/de dicto distinctions are key to social network epistemics. Technically, we show that DTML semantics can represent a popular class of hybrid logic epistemic social network models. We also show that DTML ca…
Peking University（北京大学）；University of Auckland（奥克兰大学）
In standard epistemic logic, agent names are usually assumed to be common knowledge implicitly. This is unreasonable for various applications. Inspired by term modal logic and assignment operators in dynamic logic, we introduce a lightweight modal predicate logic where names can be non-rigid. The language can handle various de dicto and de re distinctions in a natural way. The main technical result is a complete axiomatisation of this logic over S5 models.
Epistemic logic has become a major field of philosophical logic ever since the groundbreaking work by Hintikka (1962). Despite its various successful applications in theoretical computer science, AI, and game theory, the technical development of the field has been mainly focusing on the propositional part, i.e., the propositional modal logics of "knowing that". However, knowledge is expressed in everyday life by using various other locutions such as "knowing whether", "knowing what", "knowing how" and so on (knowing-wh hereafter). Such knowledge expressions are better captured in quantified ep…
Bayreuth University（拜罗伊特大学）；University of Bamberg（班贝格大学）；Lund University（隆德大学）；University of Copenhagen（哥本哈根大学）
The paper analyzes dynamic epistemic logic from a topological perspective. The main contribution consists of a framework in which dynamic epistemic logic satisfies the requirements for being a topological dynamical system thus interfacing discrete dynamic logics with continuous mappings of dynamical systems. The setting is based on a notion of logical convergence, demonstratively equivalent with convergence in Stone topology. Presented is a flexible, parametrized family of metrics inducing the latter, used as an analytical aid. We show maps induced by action model transformations continuous wi…
We define reachability games based on Dynamic Epistemic Logic (DEL), where the players' actions are finely described as DEL action models. We first consider the setting where an external controller with perfect information interacts with an environment and aims at reaching some epistemic goal state regarding the passive agents of the system. We study the problem of strategy existence for the controller, which generalises the classic epistemic planning problem, and we solve it for several types of actions such as public announcements and public actions. We then consider a yet richer setting whe…
This paper positively solves an open problem if it is possible to provide a Hilbert system to Epistemic Logic of Friendship (EFL) by Seligman, Girard and Liu. To find a Hilbert system, we first introduce a sound, complete and cut-free tree (or nested) sequent calculus for EFL, which is an integrated combination of Seligman's sequent calculus for basic hybrid logic and a tree sequent calculus for modal logic. Then we translate a tree sequent into an ordinary formula to specify a Hilbert system of EFL and finally show that our Hilbert system is sound and complete for the intended two-dimensional…
Recent years witnessed a growing interest in non-standard epistemic logics of knowing whether, knowing how, knowing what, knowing why and so on. The new epistemic modalities introduced in those logics all share, in their semantics, the general schema of $\exists x \Box ϕ$, e.g., knowing how to achieve $ϕ$ roughly means that there exists a way such that you know that it is a way to ensure that $ϕ$. Moreover, the resulting logics are decidable. Inspired by those particular logics, in this work, we propose a very general and powerful framework based on quantifier-free predicate language extended …
Cornell University（康奈尔大学）；University of New South Wales（新南威尔士大学）；Forrester Research（弗雷斯特研究公司）
While there have been many attempts, going back to BAN logic, to base reasoning about security protocols on epistemic notions, they have not been all that successful. Arguably, this has been due to the particular logics chosen. We present a simple logic based on the well-understood modal operators of knowledge, time, and probability, and show that it is able to handle issues that have often been swept under the rug by other approaches, while being flexible enough to capture all the higher- level security notions that appear in BAN logic. Moreover, while still assuming that the knowledge operat…
The paper suggests a definition of "know who" as a modality using Grove-Halpern semantics of names. It also introduces a logical system that describes the interplay between modalities "knows who", "knows", and "for all agents". The main technical result is a completeness theorem for the proposed system.
Epistemic Logic Programs (ELPs), an extension of Answer Set Programming (ASP) with epistemic operators, have received renewed attention from the research community in recent years. Classically, evaluating an ELP yields a set of world views, with each being a set of answer sets. In this paper, we propose an alternative definition of world views that represents them as three-valued assignments, where each atom can be either always true, always false, or neither. Based on several examples, we show that this definition is natural and intuitive. We also investigate relevant computational properties…
Institute of Mathematics and Statistics, Federal University of Bahia - UFBA（巴伊亚联邦大学数学与统计学院）
AGM's belief revision is one of the main paradigms in the study of belief change operations. In this context, belief bases (prioritised bases) have been primarily used to specify the agent's belief state. While the connection of iterated AGM-like operations and their encoding in dynamic epistemic logics have been studied before, few works considered how well-known postulates from iterated belief revision theory can be characterised by means of belief bases and their counterpart in dynamic epistemic logic. Particularly, it has been shown that some postulates can be characterised through transfo…
We develop a tableau-based decision procedure for the full coalitional multiagent temporal-epistemic logic of linear time CMATEL(CD+LT). It extends LTL with operators of common and distributed knowledge for all coalitions of agents. The tableau procedure runs in exponential time, matching the lower bound obtained by Halpern and Vardi for a fragment of our logic, thus providing a complexity-optimal decision procedure for CMATEL(CD+LT).
Categorization systems are widely studied in psychology, sociology, and organization theory as information-structuring devices which are critical to decision-making processes. In the present paper, we introduce a sound and complete epistemic logic of categories and agents' categorical perception. The Kripke-style semantics of this logic is given in terms of data structures based on two domains: one domain representing objects (e.g. market products) and one domain representing the features of the objects which are relevant to the agents' decision-making. We use this framework to discuss and pro…
Epistemic Logic Programs (ELPs), that is, Answer Set Programming (ASP) extended with epistemic operators, have received renewed interest in recent years, which led to a flurry of new research, as well as efficient solvers. An important question is under which conditions a sub-program can be replaced by another one without changing the meaning, in any context. This problem is known as strong equivalence, and is well-studied for ASP. For ELPs, this question has been approached by embedding them into epistemic extensions of equilibrium logics. In this paper, we consider a simpler, more direct cha…
