5-7 July 2006S. Servolo island, Venice - Italy
5-7 July 2006
Technical Program:
Five minute talks
PIN blocks are 64-bit strings that encode a PIN ready for encryption and secure transmission in banking networks. PIN block attacks exploit feedback from error messages during PIN block manipulation operations, to allow an attacker to guess a PIN in far fewer operations than would be required by a brute-force attack. This talk will briefly describe our framework for formal analysis of such attacks. Our analysis is probabilistic, and is automated using constraint logic programming and probabilistic model checking.
A modified version of the Indistinguishability-Based model from the computational complexity approach is encoded using Asynchronous Product Automata (APA). A model checker tool, Simple Homomorphism Verification Tool (SHVT), is then used to perform state-space analysis on the Automata in the setting of planning problem. A previously proven secure protocol is used as a case study. We then refute its security proof by revealing a previously unpublished flaw in the protocol using SHVT. We then show how our approach can automatically repair the protocol. This is, to the best of our knowledge, the first work that integrates an adversarial model from the computational complexity paradigm with an automated tool from the computer security paradigm to analyse protocols in an artificial intelligence problem setting – planning problem – and, most importantly, to repair protocols.
We present a novel approach for concisely abstracting authentication protocols and for subsequently analyzing those abstractions in a sound manner, i.e., deriving authentication guarantees for protocol abstractions suffices for proving these guarantees for the actual protocols. The abstractions are formalized in a novel calculus which constitutes a higher-level abstraction of the p-spi calculus and is specifically tailored towards reasoning about challenge-response mechanisms within authentication protocols. Furthermore, it allows for expressing protocols without having to include details on the specific structure of exchanged messages. This in particular entails that many authentication protocols share a common abstraction so that a single validation of this abstraction already gives rise to security guarantees for all these protocols. Moreover, such an abstract validation can be automatically performed using static analysis techniques based on an effect system. Finally, extensions to abstractions of additional protocol classes immediately enjoy a soundness theorem provided that these extensions satisfy certain explicit, easily checkable conditions.
In this work, we introduce a quantitative extension of the usual Dolev-Yao intruder model. This extended model provides a basis for considering protocol attacks that are possible when the intruder has a reasonable amount of computational power, in particular when he is able, with a certain probability, to guess encryption keys or other particular kind of data such as the body of a hashed message. This way we can measure the insecurity of protocols and consider protocols for which a certain security bound is met. We also show that these extensions do not augment the computational complexity of the protocol insecurity problem in the case of a finite number of interleaved protocol sessions.
The standard symbolic, deducibility-based notions of secrecy are in general insufficient from a cryptographic point of view, especially in presence of hash functions. Therefore we devise and motivate a more appropriate secrecy criterion which exactly captures a standard cryptographic notion of secrecy for protocols involving public-key enryption and hash functions: protocols that satisfy it are computationally secure while any violation of our criterion directly leads to an attack. Furthermore, we prove that our criterion is decidable via an NP decision procedure. Our results hold for standard security notions for encryption and hash functions modeled as random oracles.
We define and study a distributed cryptographic implementation for an asynchronous pi calculus. At the source level, we adapt simple type systems designed for establishing formal secrecy properties. We show that those secrecy properties have counterparts in the implementation, not formally but at the level of bitstrings, and with respect to probabilistic polynomial-time active adversaries. We rely on compilation to a typed intermediate language with a fixed scheduling strategy. While we exploit interesting, previous theorems for that intermediate language, our result appears to be the first computational soundness theorem for a standard process calculus with mobile channels.
The Dependency Core Calculus (DCC) is an extension of the computational lambda calculus that was designed in order to capture the notion of dependency that arises in information-flow control, partial evaluation, and other programming-language settings. We show that, unexpectedly, DCC can also be used as a calculus for access control in distributed systems.
Preventative policy enforcement mechanisms are limited: they are inflexible when unanticipated circumstances arise, and most are either inflexible with respect the policies they can enforce or incapable of continuing to enforce policies on data objects as they move from one system to another. In this talk we make a case for approach to enforcing policies not by preventing unauthorized use, but rather by deterring it.
When designing a protection mechanism we would like assurance that a malicious principal cannot bypass security in some unexpected, but permitted (according to the design), manner. This malicious principal corresponds to: the Trojan Horse exploiting a covert channel; the Spy engaging a replay attack on a security protocol; the principal engaging subterfuge in a trust management scheme, etc. In this short talk we will demonstrate how subterfuge can occur in delegation schemes and argue that non-interference provides the basis for a formal understanding of this attack.
Bedwyr is a software system currently under development between two teams at INRIA (LIX, Ecole Polytechnique) and the University of Minnesota. This system, currently written in OCaml, is a direct implementation of two recent advances in the theory of proof search.
(1) Finite success and finite failure can be modelled as a negation within a proof theory setting allows a proof search system to capture both aspects of may and must behavior in operational semantics.
(2) Higher-order abstract syntax is directly supported using term-level lambda-binders, the nabla-quantifier, higher-order pattern unification, and explicit substitutions. These features allow reasoning directly on expressions containing bound variables.
Applications that we have explored range from computing symbolic bisimulation and modal logic checking for the pi-calculus, computing winning strategies for games, and various model checking problems.
David Baelde & Dale Miller (INRIA & LIX/Ecole Polytechnique)
Andrew Gacek & Gopalan Nadathur (University of Minneapolis)
Alwen Tiu (Australian National University and NICTA).
Formal reasoning about quantum systems has become important due to recent advances in quantum computation and quantum security. Extensions of classical logic for reasoning about quantum states based on the exogenous semantics approach have shown potential for applications. So far no recursive axiomatization was achieved. Herein we present a decidable proof system by restricting the language and relaxing the semantics.
We propose a general framework of secrecy and preservation of secrecy for labeled transition systems. Our definition of secrecy is parameterized by the distinguishing power of the observer, the properties to be kept secret, and the executions of interest, and captures a multitude of definitions in the literature. We define a notion of secrecy preserving refinement between systems by strengthening the classical trace-based refinement so that the implementation leaks a secret only when the specification also leaks it. We show that secrecy is in general not definable in $\mu$-calculus, and thus not expressible in specification logics supported by standard model-checkers. However, we develop a simulation-based proof technique for establishing secrecy preserving refinement. This result shows how existing refinement checkers can be used to show correctness of an implementation with respect to a specification.
We propose an information theoretical analysis of security of
looping programs, both in terms of absolute and rate of leakage,
the main interest being the investigation and classification of
bounded and unbounded covert channels. This analysis is based
on information theoretical formulas derived from the
denotational semantics of while statements and, given programs
like
low=20; while ( high < low) {low=low-1}
Unwinding conditions provide a general framework for the definition of security properties. They basically depend on the operational semantics and on the (low level) observational equivalence of the specification language under consideration. Hence, unwinding conditions are quite natural also in the case of concurrent imperative languages.
Unfortunately, they are usually undecidable because of the presence of both infinite states and arithmetic operations over the integers. In this context type systems and other static analysis techniques introduced in the literature can be seen as sufficient conditions to prove unwinding-based security
properties. In order to increment the precision of the static analysis, we combine a static proof system with dynamic verification techniques and apply it for the analysis of a basic imperative concurrent language. In particular, we exploit first-order formulae over the reals to both approximate the computation over the integers and symbolically represent an infinite number of states. The proposed first-order formulae mime the operational semantics of the non-recursive fragment of our language. The main issues at this point concern:
(1) how can we bound the computational complexity of our method? (2) how can we introduce a dynamic verification component also for recursion? (3) which extensions of the concurrent imperative language should we consider first?
Considerable attention has been paid to information-flow based enforcement mechanisms in latest years. The theory of information-flow security is now well established, and has to be applied to real problems. We propose to use information flow analysis to secure applications in small, open, Java-enabled embedded systems. To take into account constrains of such systems, we propose an algorithm divided into two phases, an "off-board" analysis, whose result is embedded in the mobile code, and then verified by the target embedded system at loading time.
We propose a framework in which anonymity protocols are interpreted as particular kinds of channels, and the degree of anonymity provided by the protocol as the converse of the channel's capacity. We illustrate how several notions of anonymity can be expressed in this framework, and show the relation with various definitions of probabilistic anonymity in literature.