Author name cluster

David Basin

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers

1 author row

JMLR Journal 2012 Journal Article

Multi-Assignment Clustering for Boolean Data

Mario Frank
Andreas P. Streich
David Basin
Joachim M. Buhmann

We propose a probabilistic model for clustering Boolean data where an object can be simultaneously assigned to multiple clusters. By explicitly modeling the underlying generative process that combines the individual source emissions, highly structured data are expressed with substantially fewer clusters compared to single-assignment clustering. As a consequence, such a model provides robust parameter estimators even when the number of samples is low. We extend the model with different noise processes and demonstrate that maximum-likelihood estimation with multiple assignments consistently infers source parameters more accurately than single-assignment clustering. Our model is primarily motivated by the task of role mining for role-based access control, where users of a system are assigned one or more roles. In experiments with real-world access-control data, our model exhibits better generalization performance than state-of-the-art approaches. [abs] [ pdf ][ bib ] &copy JMLR 2012. ( edit, beta )

PDF Details

TCS Journal 2011 Journal Article

Distributed temporal logic for the analysis of security protocol models

David Basin
Carlos Caleiro
Jaime Ramos
Luca Viganò

The distributed temporal logic DTL is an expressive logic, well suited for formalizing properties of concurrent, communicating agents. We show how DTL can be used as a metalogic to reason about and relate different security protocol models. This includes reasoning about model simplifications, where models are transformed to have fewer agents or behaviors, and verifying model reductions, where to establish the validity of a property it suffices to consider its satisfaction on only a subset of models. We illustrate how DTL can be used to formalize security models, protocols, and properties, and then present three concrete examples of metareasoning. First, we prove a general theorem about sufficient conditions for data to remain secret during communication. Second, we prove the equivalence of two models for guaranteeing message-origin authentication. Finally, we relate channel-based and intruder-centric models, showing that it is sufficient to consider models in which the intruder completely controls the network. While some of these results belong to the folklore or have been shown, mutatis mutandis, using other formalisms, DTL provides a uniform means to prove them within the same formalism. It also allows us to clarify subtle aspects of these model transformations that are often neglected or cannot be specified in the first place.

Details DOI

TCS Journal 2006 Journal Article

On the semantics of Alice&Bob specifications of security protocols

Carlos Caleiro
Luca Viganò
David Basin

In the context of security protocols, the so-called Alice&Bob notation is often used to describe the messages exchanged between honest principals in successful protocol runs. While intuitive, this notation is ambiguous in its description of the actions taken by principals, in particular with respect to the conditions they must check when executing their roles and the actions they must take when the checks fail. In this paper, we investigate the semantics of protocol specifications in Alice&Bob notation. We provide both a denotational and an operational semantics for such specifications, rigorously accounting for these conditions and actions. Our denotational semantics is based on a notion of incremental symbolic runs, which reflect the data possessed by principals and how this data increases monotonically during protocol execution. We contrast this with a standard formalization of the behavior of principals, which directly interprets message exchanges as sequences of atomic actions. In particular, we provide a complete characterization of the situations where this simpler, direct approach is adequate and prove that incremental symbolic runs are more expressive in general. Our operational semantics, which is guided by the denotational semantics, implements each role of the specified protocol as a sequential process of the pattern-matching spi calculus.

Details DOI

TCS Journal 2003 Journal Article

Decision procedures for inductive Boolean functions based on alternating automata

Abdelwaheb Ayari
David Basin
Felix Klaedtke

We show how alternating automata provide decision procedures for the equality of inductively defined Boolean functions and present applications to reasoning about parameterized families of circuits. We use alternating word automata to formalize families of linearly structured circuits and alternating tree automata to formalize families of tree structured circuits. We provide complexity bounds for deciding the equality of function (or circuit) families and show how our decision procedures can be implemented using BDDs. In comparison to previous work, our approach is simpler, has better complexity bounds, and, in the case of tree-structured families, is more general.

Details DOI

TCS Journal 2001 Journal Article

A theoretical and empirical investigation of search in imperfect information games

Ian Frank
David Basin

We examine search algorithms for games with imperfect information. We first investigate Monte Carlo sampling, showing that for very simple game trees the chance of finding an optimal strategy rapidly approaches zero as size of the tree increases. We identify the reasons for this sub-optimality, and show that the same problems occur in Bridge, a popular real-world imperfect information game. We then analyse the complexity of the underlying problem, proving it to be NP-complete and describing several polynomial time heuristics. We evaluate these heuristics theoretically and experimentally, demonstrating that they significantly out-perform Monte Carlo sampling. Indeed, on a set of Bridge problems drawn from a definitive expert text, our heuristics consistently identify strategies as good as, or superior to, the expert solutions – the first time a game-general tree search algorithm has been capable of such performance.

Details DOI

I&C Journal 2000 Journal Article

Structuring Metatheory on Inductive Definitions

David Basin
Seán Matthews

We examine a problem for machine supported metatheory. There are true statements about a theory that are true of some (but only some) extensions; however, standard theory-structuring facilities do not support selective inheritance. We use the example of the deduction theorem for modal logic and show how a statement about a theory can explicitly formalize the closure conditions extensions should satisfy for it to remain true. We show how metatheories based on inductive definitions allow theories and general metatheorems to be organized this way and report on a case study using the theory FS0.

Details DOI

AIJ Journal 1998 Journal Article

Search in games with incomplete information: a case study using Bridge card play

Ian Frank
David Basin

We examine search algorithms in games with incomplete information, formalising a best defence model of such games based on the assumptions typically made when incomplete information problems are analysed in expert texts. We show that equilibrium point strategies for optimal play exist for this model, and define an algorithm capable of computing such strategies. Using this algorithm as a reference we then analyse search architectures that have been proposed for the incomplete information game of Bridge. These architectures select strategies by analysing some statistically significant collection of complete information sub-games. Our model allows us to clearly state the limitations of such architectures in producing expert analysis, and to precisely formalise and distinguish the problems that lead to sub-optimality. We illustrate these problems with simple game trees and with actual play situations from Bridge itself.

Details DOI