Abstract In order to develop solutions that perform actions as early as possible, analysis of distributed algorithms using epistemic logic has generally concentrated on “full-information protocols”, which may be inefficient with respect to space and computation time. The paper reconsiders the epistemic analysis of the problem of Simultaneous Byzantine Agreement with respect to weaker, but more practical, exchanges of information. This paper first clarifies some issues concerning both the specification of this problem and the knowledge based program characterizing its solution. One of these differences concerns the distinction between the notions of “nonfaulty” and “not yet failed”, on which there are variances in the literature. A second difference in the literature concerns the use of common knowledge versus common belief in the knowledge based program. The paper identifies situations where these notions are equivalent, but establishes that the version of the knowledge based program using common belief of the nonfaulty agent is more general. It is then shown that, when implemented relative to a given failure model and an information exchange protocol satisfying certain conditions, the common belief based knowledge based program yields a protocol that is optimal relative to solutions using the same information exchange. Conditions are also identified under which this implementation is also an optimum, but an example is provided that shows this does not hold in general.

Logics of knowledge and knowledge-based programs provide a way to give abstract descriptions of solutions to problems in fault-tolerant distributed computing, and have been used to derive optimal protocols for these problems with respect to a variety of failure models. Generally, these results have involved complex pencil and paper analyses with respect to the theoretical "full-information protocol" model of information exchange between network nodes. It is equally of interest to be able to establish the optimality of protocols using weaker, but more practical, models of information exchange, or else identify opportunities to improve their performance. Over the last 20 years, automated verification and synthesis tools for the logic of knowledge have been developed, such as the model checker MCK, that can be applied to this problem. This paper concerns the application of MCK to automated analyses of this kind. A number of information-exchange models are considered, for Simultaneous and Eventual variants of Byzantine Agreement under a range of failure types. MCK is used to automatically analyze these models. The results demonstrate that it is possible to automatically identify optimization opportunities, and to automatically synthesize optimal protocols. The paper provides performance measurements for the automated analysis, establishing a benchmark for epistemic model checking and synthesis tools.

The increasing wireless communication capabilities of vehicles creates opportunities for more efficient intersection management strategies. One promising approach is the replacement of traffic lights with a system wherein vehicles run protocols among themselves to determine right of way. In this paper, we define the intersection problem to model this scenario abstractly, without any assumptions on the specific structure of the intersection or a bound on the number of vehicles. Protocols solving the intersection problem must guarantee safety (no collisions) and liveness (every vehicle eventually goes through). In addition, we would like these protocols to satisfy various optimality criteria, some of which turn out to be achievable only in a subset of the contexts. In particular, we show a partial equivalence between eliminating unnecessary waiting, a criterion of interest in the distributed mutual-exclusion literature, and a notion of optimality that we define called lexicographical optimality. We then introduce a framework to design protocols for the intersection problem by converting an intersection policy, which is based on a global view of the intersection, to a protocol that can be run by the vehicles through the use of knowledge-based programs. Our protocols are shown to guarantee safety and liveness while also being optimal under sufficient conditions on the context. Finally, we investigate protocols in the presence of faulty vehicles that experience communication failures and older vehicles with limited communication capabilities. We show that intersection protocols can be made safe, live and optimal even in the presence of faulty behavior.

Work on optimal protocols for Eventual Byzantine Agreement (EBA)---protocols that, in a precise sense, decide as soon as possible in every run and guarantee that all nonfaulty agents decide on the same value---has focused on full-information protocols (FIPs), where agents repeatedly send messages that completely describe their past observations to every other agent. While it can be shown that, without loss of generality, we can take an optimal protocol to be an FIP, full information exchange is impractical to implement for many applications due to the required message size. We separate protocols into two parts, the information-exchange protocol and the action protocol, so as to be able to examine the effects of more limited information exchange. We then define a notion of optimality with respect to an information-exchange protocol. Roughly speaking, an action protocol P is optimal with respect to an information-exchange protocol ε if, with P, agents decide as soon as possible among action protocols that exchange information according to ε. We present a knowledge-based EBA program for omission failures all of whose implementations are guaranteed to be correct and are optimal if the information exchange satisfies a certain safety condition. We then construct concrete programs that implement this knowledge-based program in two settings of interest that are shown to satisfy the safety condition. Finally, we show that a small modification of our program results in an FIP that is both optimal and efficiently implementable, settling an open problem posed by Halpern, Moses, and Waarts (SIAM J. Comput., 2001).

The article develops a logical understanding of processes for signature of legal contracts, motivated by applications to legal recognition of smart contracts on blockchain platforms. A number of axioms and rules of inference are developed that can be used to justify a “meeting of the minds” precondition for contract formation from the fact that certain content has been signed. In addition to an “offer and acceptance” process, the article considers “signature in counterparts”, a legal process that permits a contract between two or more parties to be brought into force by having the parties independently (possibly, remotely) sign different copies of the contract, rather than placing their signatures on a common copy at a physical meeting. It is argued that a satisfactory account of signature in counterparts benefits from a logic with syntactic self-reference. The axioms used are supported by a formal semantics, and a number of further properties of the logic are investigated. In particular, it is shown that the logic implies that when a contract has been signed, the parties do not just agree, but are inmutual agreement(a common-knowledge-like notion) about the terms of the contract.

We investigate the decidability of model checking logics of time, knowledge, and probability, with respect to two epistemic semantics: the clock and synchronous perfect recall semantics in partially observable discrete-time Markov chains. Decidability results are known for certain restricted logics with respect to these semantics, subject to a variety of restrictions that are either unexplained or involve a longstanding unsolved mathematical problem. We show that mild generalizations of the known decidable cases suffice to render the model checking problem definitively undecidable. In particular, for the synchronous perfect recall semantics, a generalization from temporal operators with finite reach to operators with infinite reach renders model checking undecidable. The case of the clock semantics is closely related to a monadic second-order logic of time and probability that is known to be decidable, except on a set of measure zero. We show that two distinct extensions of this logic make model checking undecidable. One of these involves polynomial combinations of probability terms, the other involves monadic second-order quantification into the scope of probability operators. These results explain some of the restrictions in previous work.

This article presents an extension of temporal epistemic logic with operators that can express quantification 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 on the ability to express an agent’s knowledge about the strategies being used by other agents are presented to motivate the framework, including reasoning about game-theoretic equilibria, knowledge-based programs, and information-theoretic computer security policies. Relationships to several variants of alternating temporal epistemic logic are discussed. The computational complexity of model checking the logic and several of its fragments are also characterized.

Abstract The paper studies dynamic information flow security policies in an automaton-based model. Two semantic interpretations of such policies are developed, both of which generalize the notion of TA-security [van der Meyden ESORICS 2007] for static intransitive noninterference policies. One of the interpretations focuses on information flows permitted by policy edges, the other focuses on prohibitions implied by absence of policy edges. In general, the two interpretations differ, but necessary and sufficient conditions are identified for the two interpretations to be equivalent. Sound and complete proof techniques are developed for both interpretations. Two applications of the theory are presented. The first is a general result showing that access control mechanisms are able to enforce a dynamic information flow policy. The second is a simple capability system motivated by the Flume operating system.

Abstract This paper argues that Haigh and Young’s definition of noninterference for intransitive security policies admits information flows that are not in accordance with the intuitions it seeks to formalize. Several alternative definitions are discussed, which are shown to be equivalent to the classical definition of noninterference with respect to transitive policies. Rushby’s unwinding conditions for intransitive noninterference are shown to be sound and complete for one of these definitions, TA-security. Access control systems compatible with a policy are shown to be TA-secure, and it is also shown that TA-security implies that the system can be interpreted as an access control system.

We demonstrate, by a number of examples, that information flow security properties can be proved from abstract architectural descriptions, which describe only the causal structure of a system and local properties of trusted components. We specify these architectural descriptions of systems by generalizing intransitive noninterference policies to admit the ability to filter information passed between communicating domains. A notion of refinement of such system architectures is developed that supports top-down development of architectural specifications and proofs by abstraction of information security properties. We also show that, in a concrete setting where the causal structure is enforced by access control, a static check of the access control setting plus local verification of the trusted components is sufficient to prove that a generalized intransitive noninterference policy is satisfied.

This paper presents a symbolic BDD-based model checking algorithm for an epistemic strategy logic with observational semantics. The logic has been shown to be more expressive than several variants of ATELand therefore the algorithm can also be used for ATEL model checking. We implement the algorithm in a model checker and apply it to an application on train control system. The performance of the algorithm is also reported, with a comparison showing improved results over a previous partially symbolic approach for ATEL model checking.

The paper identifies a special case in which the complex problem of synthesis from specifications in temporal-epistemic logic can be reduced to the simpler problem of model checking such specifications. An application is given of strategy synthesis in pursuit-evasion games, where one or more pursuers with incomplete information aim to discover theexistence of an evader. Experimental results are provided to evaluate the feasibility of the approach.

This paper addresses the question of how TA-security, a semantics for intransitive information-flow policies in deterministic systems, can be generalized to nondeterministic systems. Various definitions are proposed, including definitions that state that the system enforces as much of the policy as possible in the context of attacks in which groups of agents collude by sharing information through channels that lie outside the system. Relationships between the various definitions proposed are characterized, and an unwinding-based proof technique is developed. Finally, it is shown that on a specific class of systems, access control systems with local non-determinism, the strongest definition can be verified by checking a simple static property.

Abstract This paper deals with architectural designs that specify components of a system and the permitted flows of information between them. In the process of systems development, one might refine such a design by viewing a component as being composed of subcomponents, and specifying permitted flows of information between these subcomponents and others in the design. The paper studies the soundness of such refinements with respect to a spectrum of different semantics for information flow policies, including Goguen and Meseguer’s purge-based definition, Haigh and Young’s intransitive purge-based definition, and some more recent notions TA-security, TO-security and ITO-security defined by van der Meyden. It is shown that all these definitions support the soundness of architectural refinement, for both a state- and an action-observed model of systems. A notion of systems refinement in which the information content of observations is reduced is also studied. It is also shown that refinement preserves weak access control structure, an implementation mechanism that ensures TA-security.

The paper considers several definitions of information flow security for intransitive policies from the point of view of the complexity of verifying whether a finite-state system is secure. The results are as follows. Checking (i) P-security (Goguen and Meseguer), (ii) IP-security (Haigh and Young), and (iii) TA-security (van der Meyden) are all in PTIME, while checking TO-security (van der Meyden) is undecidable. The most important ingredients in the proofs of the PTIME upper bounds are new characterizations of the respective security notions, which also enable the algorithms to return simple counterexamples demonstrating insecurity. Our results for IP-security improve a previous doubly exponential bound of Hadj-Alouane et al.

The paper describes an abstraction for protocols that are based on multiple rounds of Chaum's Dining Cryptographers protocol. It is proved that the abstraction preserves a rich class of specifications in the logic of knowledge. This result is applied to optimize model checking of implementations of a knowledge-based program that uses the Dining Cryptographers protocol as a primitive in an anonymous broadcast system. Performance results are given for model checking knowledge-based specifications in the concrete and abstract models of this protocol, and some new conclusions about the protocol are derived.

This paper describes an algorithm for model checking a fragment of the logic of knowledge and probability in multi-agent systems, with respect to a perfect recall interpretation of knowledge and agents' subjective probability. The algorithm has been implemented in the epistemic model checker MCK. Some experiments with the implemented algorithm are reported, in which some properties of agents' probabilistic knowledge are verified in two security protocols: Chaum's Dining Cryptographers protocol, and a protocol for Oblivious Transfer due to Rivest.

In the clock semantics for epistemic logic, two situations are indistinguishable for an agent when it makes the same observation and the time in the situations is the same. The paper characterizes the complexity of model checking branching time logics of knowledge in finite state systems with respect to the clock semantics.

One of our most resilient intuitions is that causality is a precondition for information flow: where there are no causal connections, we expect there to be no flow of information. In this paper, we study this idea as it arises in the computer science notion of systems architectures, which are high level designs that describe the coarse structure of a system in terms of its high-level components and their permitted causal interactions.

The focus of work on information flow security has primarily been on definitions of security in asynchronous systems models. This paper considers systems with schedulers, which require synchronous variants of these definitions. In particular, it studies the dependence of these variant definitions of security on implementation details of the scheduler. Such independence is shown to hold for synchronous variants of trace-based definitions, but not for bisimulation-based definitions. Stronger versions of the bisimulation-based definitions are proposed that recover implementation-independence.

We introduce (i) a general class of security protocols with private channel as cryptographic primitive and (ii) a probabilistic epistemic logic to express properties of security protocols. Our main theorem says that when a property expressed in our logic holds for an ideal protocol (where "ideal" means that the private channel hides everything), then it also holds when the private channel is implemented using an encryption scheme that guarantees perfect secrecy (in the sense of Shannon). Our class of protocols contains, for instance, an oblivious transfer protocol by Rivest and Chaum's solution to the dining cryptographers problem. In our logic we can express fundamental security properties of these protocols. The proof of the main theorem is based on a notion of refinement for probabilistic Kripke structures.

Sound and complete axiomatizations are provided for a number of different logics involving modalities for knowledge and time. These logics arise from different choices for various parameters regarding the interaction of knowledge with time and regarding the language used. All the logics considered involve the discrete time linear temporal logic operators "next" and "until" and an operator for the knowledge of each of a number of agents. Both the single-agent and multiple-agent cases are studied: in some instances of the latter there is also an operator for the common knowledge of the group of all agents. Four different semantic properties of agents are considered: whether they (i) have a unique initial state, (ii) operate synchronously, (iii) have perfect recall, and (iv) learn. The property of no learning is essentially dual to perfect recall. Not all settings of these parameters lead to recursively axiomatizable logics, but sound and complete axiomatizations are presented for all the ones that do.

This paper applies to quantum systems a modelling for the logic of knowledge, originally developed for reasoning about distributed systems, but since then applied to game theory, computer security and artificial intelligence. A formal model of quantum message passing systems is developed and the question of how one might define the semantics of a modal operator for knowledge in this model is considered. It is argued that there are at least two plausible semantics, depending on whether the agents are permitted to make use of their quantum state in determining what they know, and on whether one is dealing with single instances of quantum systems, or ensembles. The framework is illustrated using a number of examples from the quantum computing literature, including protocols for quantum key distribution and teleportation.

Summary form only given, as follows. The paper gives a "stat of the art" overview of modal logics of knowledge and time, covering both axiomatizations and model checking. In the temporal dimension, we consider both linear and branching time logics. The semantics of knowledge can be defined in a variety of ways, reflecting differing assumptions about the resources available to the agent in determining what it knows: from its current observation only, to synchrony (observation plus clock) to perfect recall. We discuss the impact of these assumptions on the axiomatizations and on the complexity of model checking of the combined logics. We also describe some initial experiments with a model checker based on these results.

SPKI/SDSI is a proposed public key infrastructure standard that incorporates the SDSI public key infrastructure. SDSI's key innovation was the use of local names. We previously introduced a Logic of Local Name Containment that has a clear semantics and was shown to completely characterize SDSI name resolution. Here we show how our earlier approach can be extended to deal with a number of key features of SPKI, including revocation, expiry dates, and tuple reduction. We show that these extensions add relatively little complexity to the logic. In particular, we do not need a nonmonotonic logic to capture revocation. We then use our semantics to examine SPKI's tuple reduction rules. Our analysis highlights places where SPKI's informal description of tuple reduction is somewhat vague, and shows that extra reduction rules are necessary in order to capture general information about binding and authorization.

Abstract: SPKI/SDSI is a proposed public key infrastructure standard that incorporates the SDSI public key infrastructure. SDSI's key innovation was the use of local names. We previously introduced a Logic of Local Name Containment that has a clear semantics and was shown to completely characterize SDSI name resolution. Here we show how our earlier approach can be extended to deal with a number of key features of SPKI, including revocation, expiry dates, and tuple reduction, without invoking nonmonotonicity. We show that these extensions add relatively little complexity to the logic. We then use our semantics to examine SPKI's tuple reduction rules. Our analysis highlights places where SPKI's informal description of tuple reduction is somewhat vague, and shows that extra reduction rules are necessary in order to capture general information about binding and authorization.

Abadi has introduced a logic to explicate the meaning of local names in SDSI, the Simple Distributed Security Infrastructure proposed by Rivest and Lampson. Abadi's logic does not correspond precisely to SDSI, however; it draws conclusions about local names that do not follow from SDSI's name resol ution algorithm. Moreover, its semantics is somewhat unintuitive. This paper presents the Logic of Local Name Containment, which does not suffer from these deficiencies. It has a clear semantics and provides a tight characterization of SDSI name resolution. The semantics is shown to be closely related to that of logic programs, leading to an approach to the efficient implementation of queries concerning local names. A complete axiomatization of the logic is also provided.

In the optimization of queries in an object-oriented database (OODB) system, a natural first step is to use the typing constraints imposed by the schema to transform a query into an equivalent one that logically accesses a minimal set of objects. We study a class of queries for OODBs called conjunctive queries. Variables in a conjunctive query range over heterogeneous sets of objects. Consequently, a conjunctive query is equivalent to a union of conjunctive queries of a special kind, called terminal conjunctive queries. Testing containment is a necessary step in solving the equivalence and minimization problems. We first characterize the containment and minimization conditions for the class of terminal conjunctive queries. We then characterize containment for the class of all conjunctive queries and derive an optimization algorithm for this class. The equivalent optimal query produced is expressed as a union of terminal conjunctive queries, which has the property that the number of variables as well as their search spaces are minimal among all unions of terminal conjunctive queries. Finally, we investigate the complexity of the containment problem. We show that it is complete in $\Pi^{p}_{2}$.

The semantic framework for the modal logic of knowledge due to Halpern and Moses provides a way to ascribe knowlegde to agents in distributed and multiagent systems. In this paper we study two special cases of this framework:full systemsandhypercubes. Both model static situtations in which no agents has any information about another agent's state. Full systems and hypercubes are an appropriate model for the initial configurations of many systems of interest. We establish a correspondence between full systems and hypercube systems and certain classes of Kripke frames. We show that these classes of systems correspond to the same logic. Moreover, this logic is also the same as that generated by the larger class ofweakly directed frames. We provide a sound and complete axiomatization, S5WDnof this logic, and study its computational complexity. Finally, we show that under certain natural assumptions, in a model where knowledge evolves over time, S5WDncharacteristics the properties of knowledge not just at the initial configuration, but also at all later configurations. In this particular, this holds forhomogeneous broadcast systems,which capture settings in which agents are intially ignorant of each others local states, operate synchronously, have perfect recall, and can communicate only by broadcasting.

M. Abadi (1998) has introduced a logic to explicate the meaning of local names in SDSI, the simple distributed security infrastructure proposed by Rivest and Lampson. Abadi's logic does not correspond precisely to SDSI, however, it draws conclusions about local names that do not follow from SDSI's name resolution algorithm. Moreover its semantics is somewhat unintuitive. This paper presents the logic of local name containment, which does not suffer from these deficiencies. It has a clear semantics and provides a tight characterization of SDSI name resolution. The semantics is shown to be closely related to that of logic programs, leading to an approach to the efficient implementation of queries concerning local names. A complete axiomatization of the logic is also provided.

A distributed system, possibly asynchronous, is said to have perfect recall if at all times each processor's state includes a record of all its previous states. The completeness of a propositional modal logic of knowledge and time with respect to such systems is established. The logic includes modal operators for knowledge, and the linear time operators "next" and "until".>

Intelligent legal information systems require the ability to represent two different notions of permission, one of which, free choice permission, cannot be adequately represented in standard modal logics. A logic that handles this modality by using ideas from dynamic logic is defined. The main result is the completeness of an axiomatization of the logic.>