arXiv subjects

Ron van der Meyden

Publications and source records attributed to Ron van der Meyden.

27 records · Page 2Linked to original sources

arXiv2014

The Complexity of Synchronous Notions of Information Flow Security

The paper considers the complexity of verifying that a finite state system satisfies a number of definitions of information flow security. The systems model considered is one in which agents operate synchronously with awareness of the global clock. This enables timing based attacks to be captured, whereas previous work on this topic has dealt primarily with asynchronous systems. Versions of the notions of nondeducibility on inputs, nondeducibility on strategies, and an unwinding based notion are formulated for this model. All three notions are shown to be decidable, and their computational complexity is characterised.

cs.CR↗

arXiv2013

Complexity and Unwinding for Intransitive Noninterference

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, as is checking ITO-security (van der Meyden). The most important ingredients in the proofs of the PTIME upper bounds are new characterizations of the respective security notions, which also lead to new unwinding proof techniques that are shown to be sound and complete for these notions of security, and enable the algorithms to return simple counter-examples demonstrating insecurity. Our results for IP-security improve a previous doubly exponential bound of Hadj-Alouane et al.

cs.CR↗

arXiv2013

Synthesis from Knowledge-Based Specifications

In program synthesis, we transform a specification into a program that is guaranteed to satisfy the specification. In synthesis of reactive systems, the environment in which the program operates may behave nondeterministically, e.g., by generating different sequences of inputs in different runs of the system. To satisfy the specification, the program needs to act so that the specification holds in every computation generated by its interaction with the environment. Often, the program cannot observe all attributes of its environment. In this case, we should transform a specification into a program whose behavior depends only on the observable history of the computation. This is called synthesis with incomplete information. In such a setting, it is desirable to have a knowledge-based specification, which can refer to the uncertainty the program has about the environment's behavior. In this work we solve the problem of synthesis with incomplete information with respect to specifications in the logic of knowledge and time. We show that the problem has the same worst-case complexity as synthesis with complete information.

cs.LO↗

arXiv2012

Consistent assignment of quantum probabilities

We pose and solve a problem concerning consistent assignment of quantum probabilities to a set of bases associated with maximal projective measurements. We show that our solution is optimal. We also consider some consequences of the main theorem in the paper in conjunction with Gleason's theorem. Some potential applications to state tomography and probabilistic quantum secret-sharing scheme are discussed.

quant-ph↗

arXiv2010

Abstraction for Epistemic Model Checking of Dining Cryptographers-based Protocols

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, including specifications describing what an agent knows about other agents' knowledge. This result can be used to optimize model checking of Dining Cryptographers-based protocols, and applied within a methodology for knowledge-based program implementation and verification. Some case studies of such an application are given, for a protocol 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.

cs.LO↗

arXiv2010

Epistemic Model Checking for Knowledge-Based Program Implementation: an Application to Anonymous Broadcast

Knowledge-based programs provide an abstract level of description of protocols in which agent actions are related to their states of knowledge. The paper describes how epistemic model checking technology may be applied to discover and verify concrete implementations based on this abstract level of description. The details of the implementations depend on the specific context of use of the protocol. The knowledge-based approach enables the implementations to be optimized relative to these conditions of use. The approach is illustrated using extensions of the Dining Cryptographers protocol, a security protocol for anonymous broadcast.

cs.LO↗

arXiv2002

Complete Axiomatizations for Reasoning About Knowledge and Time

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. 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 have a unique initial state, whether they operate synchronously, whether they have perfect recall, and whether they 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.

cs.LO↗

arXiv2002

A logical reconstruction of SPKI

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.

cs.CR↗

arXiv2000

A Logic for SDSI's Linked Local Name Spaces

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

cs.CR↗