arXiv subjects

Ron van der Meyden

Publications and source records attributed to Ron van der Meyden.

At least 19 recordsLinked to original sources

arXiv2025

Optimality of Simultaneous Consensus with Limited Information Exchange (Extended Abstract)

Work on the development of optimal fault-tolerant Agreement protocols using the logic of knowledge has concentrated on the "full information" approach to information exchange, which is costly with respect to message size. Alpturer, Halpern, and van der Meyden (PODC 2023) introduced the notion of optimality with respect to a limited information exchange, and studied the Eventual Agreement problem in the sending omissions failure model. The present paper studies the Simultaneous Agreement problem for the crash failures model, and a number of limited information exchanges from the literature. In particular, the paper considers information exchanges from a FloodSet protocol (Lynch, Distributed Algorithms 1996), a variant of this in which agents also count the number of failures (Castañeda et al, NETYS 2017), and a variant in which agents associate each agent with a value (Raynal, PRDC 2002). A new information exchange is also introduced that enables decisions to be made at worst one round later than the optimal protocol of Dwork and Moses (I&C 88), but with lower computation cost and space requirements. By determining implementations of a knowledge based program, protocols are derived that are optimal amongst protocols for each of these information exchanges.

cs.DC↗

arXiv2025

Optimal Simultaneous Byzantine Agreement, Common Knowledge and Limited Information Exchange

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. The paper first clarifies some issues concerning both the specification of this problem and the knowledge based program characterizing its solution, concerning the distinction between the notions of ``nonfaulty'' and ``not yet failed'', on which there are variances in the literature. It is then shown that, when implemented relative to a given failure model and an information exchange protocol satisfying certain conditions, this 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.

cs.DC↗

arXiv2025

Model Checking and Synthesis for Optimal Use of Knowledge in Consensus Protocols

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.

cs.DC↗

arXiv2024

A Knowledge-Based Analysis of Intersection Protocols

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.

cs.DC↗

arXiv2023

Optimal Eventual Byzantine Agreement Protocols with Omission Failures

Work on \emph{optimal} protocols for \emph{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 emph{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 \emph{information-exchange protocol} and the \emph{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 $\mathcal{E}$ if, with $P$, agents decide as soon as possible among action protocols that exchange information according to $\mathcal{E}$. 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).

cs.DC↗

arXiv2021

A Game Theoretic Analysis of Liquidity Events in Convertible Instruments

Convertible instruments are contracts, used in venture financing, which give investors the right to receive shares in the venture in certain circumstances. In liquidity events, investors may have the option to either receive back their principal investment, or to receive a proportional payment after conversion of the contract to a shareholding. In each case, the value of the payment may depend on the choices made by other investors who hold such convertible contracts. A liquidity event therefore sets up a game theoretic optimization problem. The paper defines a general model for such games, which is shown to cover all instances of the Y Combinator Simple Agreement for Future Equity (SAFE) contracts, a type of convertible instrument that is commonly used to finance startup ventures. The paper shows that, in general, pure strategy Nash equilibria do not necessarily exist in this model, and there may not exist an optimum pure strategy Nash equilibrium in cases where pure strategy Nash equilibria do exist. However, it is shown when all contracts are uniformly one of the SAFE contract types, an optimum pure strategy Nash equilibrium exists. Polynomial time algorithms for computing (optimum) pure strategy Nash equilibria in these cases are developed.

econ.TH↗

arXiv2021

A Formal Treatment of Contract Signature

The paper 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 paper 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 in mutual agreement (a common-knowledge-like notion) about the terms of the contract.

cs.AI↗

arXiv2018

On the specification and verification of atomic swap smart contracts

Blockchain systems and smart contracts provide ways to securely implement multi-party transactions without the use of trusted intermediaries, which currently underpin many commercial transactions. However, they do so by transferring trust to computer systems, raising the question of whether code can be trusted. Experience with high value losses resulting from incorrect code has already shown that formal verification of smart contracts is likely to be beneficial. This note investigates the specification and verification of a simple form of multi-party transaction, atomic swaps. It is argued that logics with the ability to express properties of strategies of players in a multi-agent setting are conceptually useful for this purpose, although ultimately, for our specific examples, the less expressive setting of temporal logic suffices for verification of concrete implementations. This is illustrated through a number of examples of the use of a model checker to verify atomic swap smart contracts in on-chain and cross-chain settings.

cs.LO↗

arXiv2018

An Epistemic Strategy Logic

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, 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.

cs.LO↗

arXiv2017

An Epistemic Foundation for Authentication Logics (Extended Abstract)

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 operator allows for unbounded computation, it can handle the fact that a computationally bounded agent cannot decrypt messages in a natural way, by distinguishing strings and message terms. We demonstrate that our logic can capture BAN logic notions by providing a translation of the BAN operators into our logic, capturing belief by a form of probabilistic knowledge.

cs.CR↗

arXiv2017

Optimizing Epistemic Model Checking Using Conditional Independence (Extended Abstract)

This paper shows that conditional independence reasoning can be applied to optimize epistemic model checking, in which one verifies that a model for a number of agents operating with imperfect information satisfies a formula expressed in a modal multi-agent logic of knowledge. The optimization has been implemented in the epistemic model checker MCK. The paper reports experimental results demonstrating that it can yield multiple orders of magnitude performance improvements.

cs.LO↗

arXiv2016

Optimizing Epistemic Model Checking using Conditional Independence

Conditional independence reasoning has been shown to be helpful in the context of Bayesian nets to optimize probabilistic inference, and related techniques have been applied to speed up a number of logical reasoning tasks in boolean logic by eliminating irrelevant parts of the formulas. This paper shows that conditional independence reasoning can also be applied to optimize epistemic model checking, in which one verifies that a model for a number of agents operating with imperfect information satisfies a formula expressed in a modal multi-agent logic of knowledge. An optimization technique is developed that precedes the use of a model checking algorithm with an analysis that applies conditional independence reasoning to reduce the size of the model. The optimization has been implemented in the epistemic model checker MCK. The paper reports experimental results demonstrating that it can yield multiple orders of magnitude performance improvements.

cs.LO↗

arXiv2016

On Reductions from Multi-Domain Noninterference to the Two-Level Case

The literature on information flow security with respect to transitive policies has been concentrated largely on the case of policies with two security domains, High and Low, because of a presumption that more general policies can be reduced to this two-domain case. The details of the reduction have not been the subject of careful study, however. Many works in the literature use a reduction based on a quantification over "Low-down" partitionings of domains into those below and those not below a given domain in the information flow order. A few use "High-up" partitionings of domains into those above and those not above a given domain. Our paper argues that more general "cut" partitionings are also appropriate, and studies the relationships between the resulting multi-domain notions of security when the basic notion for the two-domain case to which we reduce is either Nondeducibility on Inputs or Generalized Noninterference. The Low-down reduction is shown to be weaker than the others, and while the High-up reduction is sometimes equivalent to the cut reduction, both it and the Low-down reduction may have an undesirable property of non-monotonicity with respect to a natural ordering on policies. These results suggest that the cut-based partitioning yields a more robust general approach for reduction to the two-domain case.

cs.CR↗

arXiv2016

The complexity of approximations for epistemic synthesis (extended abstract)

Epistemic protocol specifications allow programs, for settings in which multiple agents act with incomplete information, to be described in terms of how actions are related to what the agents know. They are a variant of the knowledge-based programs of Fagin et al [Distributed Computing, 1997], motivated by the complexity of synthesizing implementations in that framework. The paper proposes an approach to the synthesis of implementations of epistemic protocol specifications, that reduces the problem of finding an implementation to a sequence of model checking problems in approximations of the ultimate system being synthesized. A number of ways to construct such approximations is considered, and these are studied for the complexity of the associated model checking problems. The outcome of the study is the identification of the best approximations with the property of being PTIME implementable.

cs.LO↗

arXiv2016

Dynamic Intransitive Noninterference Revisited

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.

cs.CR↗

arXiv2015

Undecidable Cases of Model Checking Probabilistic Temporal-Epistemic Logic

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 observed 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 a synchronous perfect recall, 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.

cs.LO↗

arXiv2014

Using Architecture to Reason about Information Security

We demonstrate, by a number of examples, that information-flow security properties can be proved from abstract architectural descriptions, that 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.

cs.CR↗

arXiv2014

An Epistemic Strategy Logic (Extended Abstract)

The paper presents an extension of temporal epistemic logic with operators that quantify over strategies. The language also provides a natural way to represent what agents would know were they to be aware of the strategies being used by other agents. Some examples are presented to motivate the framework, and relationships to several variants of alternating temporal epistemic logic are discussed. The computational complexity of model checking the logic is also characterized.

cs.LO↗