Author name cluster

David Nowak

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

2 author rows

I&C Journal 2015 Journal Article

Formal security proofs with minimal fuss: Implicit computational complexity at work

David Nowak
Yu Zhang

We show how implicit computational complexity can be used in order to increase confidence in game-based security proofs in cryptography. For this purpose we extend CSLR, a probabilistic lambda-calculus with a type system that guarantees the existence of a probabilistic polynomial-time bound on computations. This allows us to define cryptographic constructions, feasible adversaries, security notions, computational assumptions, game transformations, and game-based security proofs in a unified framework. We also show that the standard practice of cryptographers, ignoring that polynomial-time Turing machines cannot generate all uniform distributions, is actually sound. We illustrate our calculus on cryptographic constructions for public-key encryption and pseudorandom bit generation.

Details DOI

I&C Journal 2007 Journal Article

On the freeze quantifier in Constraint LTL: Decidability and complexity

Stéphane Demri
Ranko Lazić
David Nowak

Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, but this variable-binding mechanism is quite general and ubiquitous in many logical languages (first-order temporal logics, hybrid logics, logics for sequence diagrams, navigation logics, logics with λ-abstraction, etc.). We show that Constraint LTL over the simple domain 〈 N, = 〉 augmented with the freeze quantifier is undecidable which is a surprising result in view of the poor language for constraints (only equality tests). Many versions of freeze-free Constraint LTL are decidable over domains with qualitative predicates and our undecidability result actually establishes Σ 1 1 -completeness. On the positive side, we provide complexity results when the domain is finite (ExpSpace-completeness) or when the formulae are flat in a sense introduced in the paper. Our undecidability results are sharp (i. e. with restrictions on the number of variables) and all our complexity characterisations ensure completeness with respect to some complexity class (mainly PSpace and ExpSpace).

Details DOI

I&C Journal 2006 Journal Article

Synchronous structures

David Nowak

Synchronous languages have been designed to ease the development of reactive systems, by providing a methodological framework for assisting system designers from the early stages of requirement specifications to the final stages of code generation or circuit production. Synchronous languages enable a very high-level specification and an extremely modular design of complex reactive systems by structural decomposition of them into elementary processes. We define an order-theoretical model that gives a unified mathematical formalisation of all the above aspects of the synchronous methodology and characterises the essentials of the synchronous paradigm.

Details DOI

TIME Conference 2005 Conference Paper

On the Freeze Quantifier in Constraint LTL: Decidability and Complexity

Stéphane Demri
Ranko Lazic 0001
David Nowak

Constraint LTL, a generalization of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, but this variable-binding mechanism is quite general and ubiquitous in many logical languages (first-order temporal logics, hybrid logics, logics for sequence diagrams, navigation logics, etc.). We show that Constraint LTL over the simple domain augmented with the freeze operator is undecidable which is a surprising result regarding the poor language for constraints (only equality tests). Many versions of freeze-free constraint LTL are decidable over domains with qualitative predicates and our undecidability result actually establishes /spl Sigma//sub 1//sup 1/ -completeness. On the positive side, we provide complexity results when the domain is finite (EXPSPACE-completeness) or when the formulae are flat in a sense introduced in the paper.

Details

CSL Conference 2004 Conference Paper

Complete Lax Logical Relations for Cryptographic Lambda-Calculi

Jean Goubault-Larrecq
Slawomir Lasota 0001
David Nowak
Yu Zhang

Abstract Security properties are profitably expressed using notions of contextual equivalence, and logical relations are a powerful proof technique to establish contextual equivalence in typed lambda calculi, see e. g. Sumii and Pierce’s logical relation for a cryptographic lambda-calculus. We clarify Sumii and Pierce’s approach, showing that the right tool is prelogical relations, or lax logical relations in general: relations should be lax at encryption types, notably. To explore the difficult aspect of fresh name creation, we use Moggi’s monadic lambda-calculus with constants for cryptographic primitives, and Stark’s name creation monad. We define logical relations which are lax at encryption and function types but strict (non-lax) at various other types, and show that they are sound and complete for contextual equivalence at all types.

Details

CSL Conference 2003 Conference Paper

Logical Relations for Dynamic Name Creation

Yu Zhang
David Nowak

Abstract Pitts and Stark’s nu-calculus is a typed lambda-calculus which forms a basis for the study of interaction between higher-order functions and dynamically created names. A similar approach has received renewed attention recently through Sumii and Pierce’s cryptographic lambda-calculus, which deals with security protocols. Logical relations are a powerful tool to prove properties of such a calculus, notably observational equivalence. While Pitts and Stark construct a logical relation for the nu-calculus, it rests heavily on operational aspects of the calculus and is hard to be extended. We propose an alternative Kripke logical relation for the nu-calculus, which is derived naturally from the categorical model of the nu-calculus and the general notion of Kripke logical relation. This is also related to the Kripke logical relation for the name creation monad by Goubault-Larrecq et al. (CSL’2002), which the authors claimed had similarities with Pitts and Stark’s logical relation. We show that their Kripke logical relation for names is strictly weaker than Pitts and Stark’s. We also show that our Kripke logical relation, which extends the definition of Goubault-Larrecq et al. , is equivalent to Pitts and Stark’s up to first-order types; our definition rests on purely semantic constituents, and dispenses with the detours through operational semantics that Pitts and Stark use.

Details

CSL Conference 2002 Conference Paper

Logical Relations for Monadic Types

Jean Goubault-Larrecq
Slawomir Lasota 0001
David Nowak

Abstract Logical relations and their generalizations are a fundamental tool in proving properties of lambda-calculi, e. g. , yielding sound principles for observational equivalence. We propose a natural notion of logical relations able to deal with the monadic types of Moggi’s computational lambda-calculus. The treatment is categorical, and is based on notions of subsconing and distributivity laws for monads. Our approach has a number of interesting applications, including cases for lambda-calculi with non-determinism (where being in logical relation means being bisimilar), dynamic name creation, and probabilistic systems.

Details