Author name cluster

Peter van Rossum

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.

3 papers

1 author row

TCS Journal 2011 Journal Article

Information hiding in probabilistic concurrent systems

Miguel E. Andrés
Catuscia Palamidessi
Peter van Rossum
Ana Sokolova

Information hiding is a general concept which refers to the goal of preventing an adversary from inferring secret information from the observables. Anonymity and Information Flow are examples of this notion. We study the problem of information hiding in systems characterized by the coexistence of randomization and concurrency. It is well known that the presence of nondeterminism, due to the possible interleavings and interactions of the parallel components, can cause unintended information leaks. The most established approach to solve this problem is to fix the strategy of the scheduler beforehand. In this work, we propose a milder restriction on the schedulers, and we define the notion of strong (probabilistic) information hiding under various notions of observables. Furthermore, we propose a method, based on the notion of automorphism, to verify that a system satisfies the property of strong information hiding, namely strong anonymity or non-interference, depending on the context. Through the paper, we use the canonical example of the Dining Cryptographers to illustrate our ideas and techniques.

Details DOI

TCS Journal 2008 Journal Article

Sound and complete computational interpretation of symbolic hashes in the standard model

Flavio D. Garcia
Peter van Rossum

This paper provides one more step towards bridging the gap between the formal and computational approaches to the verification of cryptographic protocols. We extend the well-known Abadi–Rogaway logic with probabilistic hashes and give a precise semantic interpretation to it using Canetti’s oracle hashes. These are probabilistic polynomial-time hashes that hide all partial information. We show that, under appropriate conditions on the encryption scheme, this interpretation is computationally sound and complete. This can be used to port security results from the formal world to the computational world when considering passive adversaries. We also give an explicit example showing that oracle hashing is not strong enough to obtain such a result for active adversaries.

Details DOI

I&C Journal 2006 Journal Article

Efficient theory combination via boolean search

Marco Bozzano
Roberto Bruttomesso
Alessandro Cimatti
Tommi Junttila
Silvio Ranise
Peter van Rossum
Roberto Sebastiani

Many approaches to deciding the satisfiability of quantifier-free formulae with respect to a background theory T—also known as Satisfiability Modulo Theory, or SMT(T)—rely on the integration between an enumerator of truth assignments and a decision procedure for conjunction of literals in T. When the background theory T is the combination T 1 ∪ T 2 of two simpler theories, the approach is typically instantiated by means of a theory combination schema (e. g. Nelson–Oppen, Shostak). In this paper we propose a new approach to SMT ( T 1 ∪ T 2 ), where the enumerator of truth assignments is integrated with two decision procedures, one for T 1 and one for T 2, acting independently from each other. The key idea is to search for a truth assignment not only to the atoms occurring in the formula, but also to all the equalities between variables which are shared between the theories. This approach is simple and expressive: for instance, no modification is required to handle non-convex theories (as opposed to traditional Nelson-Oppen combinations which require a mechanism for splitting). Furthermore, it can be made practical by leveraging on state-of-the-art boolean and SMT search techniques, and on theory layering (i. e. , cheaper reasoning first, and more often). We provide thorough experimental evidence to support our claims: we instantiate the framework with two decision procedures for the combinations of Equality and Uninterpreted Functions ( EUF ) and Linear Arithmetic ( LA ), both for (the convex case of) reals and for (the non-convex case of) integers; we analyze the impact of the different optimizations on a variety of test cases; and we compare the approach with state-of-the-art competitor tools, showing that our implemented tool compares positively with them, sometimes with dramatic gains in performance.

Details DOI