Catálogo de publicaciones - libros

Interpolation results are investigated for various types of formulae. By shifting the focus from syntactic to , we generate, prove and classify a series of interpolation results for first-order logic. A few of these results non-trivially generalize known interpolation results. All the others are new.

The logic extends first-order logic by a generalized form of counting quantifiers (“the number of elements satisfying ... belongs to the set ”). This logic is investigated for structures with an injective -automatic presentation. If first-order logic is extended by an infinity-quantifier, the resulting theory of any such structure is known to be decidable [4]. It is shown that, as in the case of automatic structures [13], also modulo-counting quantifiers as well as infinite cardinality quantifiers (“there are many elements satisfying ...”) lead to decidable theories. For a structure of bounded degree with injective -automatic presentation, the fragment of that contains only effective quantifiers is shown to be decidable and an elementary algorithm for this decision is presented. Both assumptions (-automaticity and bounded degree) are necessary for this result to hold.

We consider parity games played on special pushdown graphs, namely those generated by one-counter processes. For parity games on pushdown graphs, it is known from [23] that deciding the winner is an -complete problem. An important corollary of this result is that the -calculus model checking problem for pushdown processes is -complete. As one-counter processes are special cases of pushdown processes, it follows that deciding the winner in a parity game played on the transition graph of a one-counter process can be achieved in . Nevertheless the proof for the -hardness lower bound of [23] cannot be adapted to that case. Therefore, a natural question is whether the upper bound can be improved in this special case. In this paper, we adapt techniques from [11,4] and provide a upper bound and a -hard lower bound for this problem. We also give two important consequences of this result. First, we improve the best upper bound known for model-checking one-counter processes against -calculus. Second, we show how these games can be used to solve pushdown games with winning conditions that are Boolean combinations of a parity condition on the control states with conditions on the stack height.

We describe a denotational semantics for a sequential functional language with random number generation over a countably infinite set (the natural numbers), and prove that it is fully abstract with respect to may-and-must testing.

Our model is based on biordered sets similar to Berry’s bidomains, and stable, monotone functions. However, (as in prior models of unbounded non-determinism) these functions may not be continuous. Working in a biordered setting allows us to exploit the different properties of both extensional and stable orders to construct a Cartesian closed category of sequential, discontinuous functions, with least and greatest fixpoints having strong enough properties to prove computational adequacy.

We establish full abstraction of the semantics by showing that it contains a simple, first-order “universal type-object” within which all types may be embedded using functions defined by (countable) ordinal induction.

This paper introduces the Φ-calculus, a new call-by-value version of the -calculus, following the spirit of Plotkin’s -calculus. The Φ-calculus satisfies some interesting properties, in particular that its set of solvable terms coincides with the set of -strongly normalizing terms in the classical -calculus.

The confluence of untyped -calculus with rewriting has already been studied in various directions. In this paper, we investigate the confluence of -calculus with rewriting and provide general results in two directions. First, when conditional rules are algebraic. This extends results of Müller and Dougherty for unconditional rewriting. Two cases are considered, whether beta-reduction is allowed or not in the evaluation of conditions. Moreover, Dougherty’s result is improved from the assumption of strongly normalizing -reduction to weakly normalizing -reduction. We also provide examples showing that outside these conditions, modularity of confluence is difficult to achieve. Second, we go beyond the algebraic framework and get new confluence results using a restricted notion of orthogonality that takes advantage of the conditional part of rewrite rules.

The indistinguishability of two pieces of data (or two lists of pieces of data) can be represented formally in terms of a relation called static equivalence. Static equivalence depends on an underlying equational theory. The choice of an inappropriate equational theory can lead to overly pessimistic or overly optimistic notions of indistinguishability, and in turn to security criteria that require protection against impossible attacks or—worse yet—that ignore feasible ones. In this paper, we define and justify an equational theory for standard, fundamental cryptographic operations. This equational theory yields a notion of static equivalence that implies computational indistinguishability. Static equivalence remains liberal enough for use in applications. In particular, we develop and analyze a principled formal account of guessing attacks in terms of static equivalence.

We present a static analysis technique for the verification of cryptographic protocols, specified in a process calculus. Rather than assuming a specific, fixed set of cryptographic primitives, we only require them to be specified through a term rewriting system, with no restrictions. Examples are provided to support our analysis. First, we tackle forward secrecy for a Diffie-Hellman-based protocol involving exponentiation, multiplication and inversion. Then, a simplified version of Kerberos is analyzed, showing that its use of timestamps succeeds in preventing replay attacks.

Web services are an important series of industry standards for adding semantics to web-based and XML-based communication, in particular among enterprises. Like the entire series, the security standards and proposals are highly modular. Combinations of several standards are put together for testing as interoperability scenarios, and these scenarios are likely to evolve into industry best practices. In the terminology of security research, the interoperability scenarios correspond to security protocols. Hence, it is desirable to analyze them for security. In this paper, we analyze the security of the new Secure WS-ReliableMessaging Scenario, the first scenario to combine security elements with elements of another quality-of-service standard. We do this both symbolically and cryptographically. The results of both analyses are positive. The discussion of actual cryptographic primitives of web services security is a novelty of independent interest in this paper.