David A. Basin

TIME Conference 2015 Conference Paper

Semantic Vacuity

• Grgur Petric Maretic
• Muhammad Torabi Dashti
• David A. Basin

The vacuous satisfaction of a temporal formula with respect to a model has been extensively studied in the literature. Although a universally accepted definition of vacuity does not yet exist, all existing proposals generalize, in one way or another, the antecedent failure of an implication to the syntax of a temporal logic. They are therefore syntactic: whether a model vacuously satisfies a formula is affected by semantics-preserving changes to the formula. This leads to inconsistent and counter-intuitive results. We propose an alternative: a semantic definition of vacuity for LTL where either two semantically equivalent LTL formulas are both satisfied vacuously in a model, or neither of them are. Our definition is based on a syntactic-invariant separation of LTL formulas, which gives rise to an algorithm for detecting semantic vacuity using trap properties. We also propose an alternative algorithm for Buchi automata, which can be used to detect the vacuous satisfaction of omega-regular properties as well as LTL formulas. We analyze this algorithm's worst-case complexity and, using real-world examples, demonstrate that semantic vacuity can be efficiently decided in practice.

TIME Conference 2011 Conference Paper

Monitoring Usage-Control Policies in Distributed Systems

• David A. Basin
• Matús Harvan
• Felix Klaedtke
• Eugen Zalinescu

We have previously presented a monitoring algorithm for compliance checking of policies formalized in an expressive metric first-order temporal logic. We explain here the steps required to go from the original algorithm to a working infrastructure capable of monitoring an existing distributed application producing millions of log entries per day. The main challenge is to correctly and efficiently monitor the trace interleavings obtained by totally ordering actions that happen at the same time. We provide solutions based on formula transformations and monitoring representative traces. We also report, for the first time, on statistics on the performance of our monitor on real-world data, providing evidence of its suitability for nontrivial applications.

CSL Conference 2010 Invited Paper

Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries

• David A. Basin
• Cas Cremers

Abstract We present a symbolic framework, based on a modular operational semantics, for formalizing different notions of compromise relevant for the analysis of cryptographic protocols. The framework’s rules can be combined in different ways to specify different adversary capabilities, capturing different practically-relevant notions of key and state compromise. We have extended an existing security-protocol analysis tool, Scyther, with our adversary models. This is the first tool that systematically supports notions such as weak perfect forward secrecy, key compromise impersonation, and adversaries capable of state-reveal queries. We also introduce the concept of a protocol-security hierarchy, which classifies the relative strength of protocols against different forms of compromise. In case studies, we use Scyther to automatically construct protocol-security hierarchies that refine and correct relationships between protocols previously reported in the cryptographic literature.

ICML Conference 2009 Conference Paper

Multi-assignment clustering for Boolean data

• Andreas P. Streich
• Mario Frank 0001
• David A. Basin
• Joachim M. Buhmann

TIME Conference 2008 Conference Paper

A Labeled Tableaux Systemfor the Distributed Temporal Logic DTL

• David A. Basin
• Carlos Caleiro
• Jaime Ramos
• Luca Viganò 0001

DTL is a distributed temporal logic for reasoning about temporal properties of distributed systems from the local point of view of the system's agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. We present a sound and complete labeled tableaux system for future-time DTL. To achieve this, we first formalize a labeled tableaux system for reasoning locally at each agent, which provides a system for full future-time LTL, and afterwards we combine the local systems into a global one by adding rules that capture the distributed nature of DTL.

LPAR Conference 2005 Conference Paper

Algebraic Intruder Deductions

• David A. Basin
• Sebastian Mödersheim
• Luca Viganò 0001

Abstract Many security protocols fundamentally depend on the algebraic properties of cryptographic operators. It is however difficult to handle these properties when formally analyzing protocols, since basic problems like the equality of terms that represent cryptographic messages are undecidable, even for relatively simple algebraic theories. We present a framework for security protocol analysis that can handle algebraic properties of cryptographic operators in a uniform and modular way. Our framework is based on two ideas: the use of modular rewriting to formalize a generalized equational deduction problem for the Dolev-Yao intruder, and the introduction of two parameters that control the complexity of the equational unification problems that arise during protocol analysis by bounding the depth of message terms and the operations that the intruder can perform when analyzing messages. We motivate the different restrictions made in our model by highlighting different ways in which undecidability arises when incorporating algebraic properties of cryptographic operators into formal protocol analysis.

CSL Conference 1998 Conference Paper

LISA: A Specification Language Based on WS2S

• Abdelwaheb Ayari
• David A. Basin
• Andreas Podelski

Abstract We integrate two concepts from programming languages into a specification language based on WS2S, namely high-level data structures such as records and recursively-defined datatypes (WS2S is the weak second-order monadic logic of two successors). Our integration is based on a new logic whose variables range over record-like trees and an algorithm for translating datatypes into tree automata. We have implemented LISA, a prototype system based on these ideas, which, when coupled with a decision procedure for WS2S like the MONA system, results in a verification tool that supports both high-level specifications and complexity estimations for the running time of the decision procedure.

ECAI Conference 1994 Conference Paper

Coloured Rippling: An Extension of a Theorem Proving Heuristic

• Tetsuya Yoshida
• Alan Bundy
• Ian Green
• Toby Walsh
• David A. Basin

LOPSTR Conference 1994 Conference Paper

Logic Frameworks for Logic Programs

• David A. Basin

Abstract We show how logical frameworks can provide a basis for logic program synthesis. With them, we may use first-order logic as a foundation to formalize and derive rules that constitute program development calculi. Derived rules may be in turn applied to synthesize logic programs using higher-order resolution during proof that programs meet their specifications. We illustrate this using Paulson's Isabelle system to derive and use a simple synthesis calculus based on equivalence preserving transformations.

IJCAI Conference 1993 Conference Paper

Difference Unification

• David A. Basin
• Toby Walsh

LOPSTR Conference 1993 Conference Paper

Logic Program Synthesis via Proof Planning

• Ina Kraan
• David A. Basin
• Alan Bundy

Abstract We propose a novel approach to automating the synthesis of logic programs: Logic programs are synthesized as a by-product of the planning of a verification proof. The approach is a two-level one: At the object level, we prove program verification conjectures in a sorted, first-order theory. The conjectures are of the form \( \forall \xrightarrow[{\arg s. }]{}prog(\xrightarrow[{\arg s}]{}) \leftrightarrow spec(\xrightarrow[{\arg s}]{}). \). At the meta-level, we plan the object-level verification with an unspecified program definition. The definition is represented with a (second-order) meta-level variable, which becomes instantiated in the course of the planning. This technique is an application of the Clam proof planning system [Bundy et al 90c]. Clam is currently powerful enough to plan verification proofs for given programs. We show that, if Clam’s use of middle-out reasoning is extended, it will also be able to synthesize programs.

ECAI Conference 1992 Conference Paper

An Adaptation of Proof-Planning to Declarer Play in Bridge

• Ian Frank
• David A. Basin
• Alan Bundy