Skip to main content

Über dieses Buch

The security issues set by the global digitization of our society have had, and will continue to have, a crucial impact at all levels of our social organization, including, just to mention a few, privacy, economics, environmental policies, national sovereignty, medical environments. The importance of the collaborations in the various ?elds of computer s- ence to solve these problems linked with other sciences and techniques is clearly recognized. Moreover, the collaborative work to bridge the formal theory and practical applications becomes increasingly important and useful. In this context, and since France and Japan have strong academic and ind- trial backgrounds in the theory and practice of the scienti?c challenges set by this digitized world, in 2005 we started a formal French–Japanese collaboration and workshop series on computer security. The three ?rst editions of these French–Japanese Computer Security wo- shops in Tokyo, September 5–7, 2005 and December 4–5, 2006 and in Nancy, March 13–14, 2008 were very fruitful and were accompanied by several imp- tant research exchanges between France and Japan. Because of this success, we launched a call for papers dedicated to computer security from it’s foundation to practice, with the goal of gathering together ?nal versions of the rich set of papers and ideas presented at the workshops, yet opening the call to everyone interested in contributing in this context. This v- ume presents the selection of papers arising from this call and this international collaboration.



Formal to Practical Security

Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables

First-order logic resolution is a standard way to automate the verification of security protocols. However, it sometimes fails to produce security proofs for secure protocols because of the detection of false attacks. For the verification of a bounded number of sessions, false attacks can be avoided by introducing rigid variables. Unfortunately, this yields complicated resolution procedures. We show here that there is a simple translation of the security problem for a bounded number of sessions into first-order logic, that does not introduce false attacks. This is shown by translating clauses involving rigid variables into classical first-order clauses, while preserving satisfiability. We illustrate this approach by giving a complete and terminating strategy for a first-order logic fragment resulting from the above translation, that yields a decision procedure for a bounded number of sessions.
Reynald Af feldt, Hubert Comon-Lundh

Validating Integrity for the Ephemerizer’s Protocol with CL-Atse

It is usually very difficult in Computer Science to make an information “disappear” after a certain time, once it has been published or mirrored by servers world wide. This, however, is the goal of the IBM ephemerizer’s protocol by Radia Perlman. We present in this paper the general structure of the CL-Atse protocol analysis tool from the AVISPA’s tool-suite, and symbolic analysis of the ephemerizer’s protocol and its extensions using CL-Atse. This protocol allows transmitting a data which retrieval is guarantied to be impossible after a certain time. We show that this protocol is secure for this property plus the secrecy of the data, but is trivially non secure for its integrity. We model a standard integrity check as a first extension to this protocol, which is natural and close to common usage, and we present a second extension for integrity that is much less obvious and deeply integrated in the structure of the ephemerizer’s protocol. Then, we show that while the first extension guaranty the basic integrity property under certain conditions, the second one is much stronger and allows faster computations.
Charu Arora, Mathieu Turuani

Computational Semantics for First-Order Logical Analysis of Cryptographic Protocols

This paper is concerned about relating formal and computational models of cryptography in case of active adversaries when formal security analysis is done with first order logic As opposed to earlier treatments, we introduce a new, fully probabilistic method to assign computational semantics to the syntax. The idea is to make use of the usual mathematical treatment of stochastic processes, hence be able to treat arbitrary probability distributions, non-negligible probability of collision, causal dependence or independence, and so on. We present this via considering a simple example of such a formal model, the Basic Protocol Logic by K. Hasebe and M. Okada [20], but we think the technique is suitable for a wide range of formal methods for protocol correctness proofs. We first review our framework of proof-system, BPL, for proving correctness of authentication protocols, and provide computational semantics. Then we give a full proof of the soundness theorem. We also comment on the differences of our method and that of Computational PCL.
Gergei Bana, Koji Hasebe, Mitsuhiro Okada

Fake Fingers in Fingerprint Recognition: Glycerin Supersedes Gelatin

Fingerprint Recognition currently widespreads in numerous identity verification applications such as electronic ID cards, travel documents, access control and time attendance. Security issues with the condition of use of the authentication device is a major concern in such applications. Recent publication in this field shows the lack of aliveness detection mechanism in fingerprint sensors technology, especially by using Gelatin-made fake fingers. Different material may be used to mold and reproduce exact copy of a fingerprint with its detailed shape and extended characteristics (e.g. minutiae points location). In this paper we will present a state-of-the-art of fake finger materials and disclose the power of a, let’s say, brand new material in this field: Glycerin
Claude Barral, Assia Tria

Comparing State Spaces in Automatic Security Protocol Analysis

There are several automatic tools available for the symbolic analysis of security protocols. The models underlying these tools differ in many aspects. Some of the differences have already been formally related to each other in the literature, such as difference in protocol execution models or definitions of security properties. However, there is an important difference between analysis tools that has not been investigated in depth before: the explored state space. Some tools explore all possible behaviors, whereas others explore strict subsets, often by using so-called scenarios.
We identify several types of state space explored by protocol analysis tools, and relate them to each other. We find previously unreported differences between the various approaches. Using combinatorial results, we determine the requirements for emulating one type of state space by combinations of another type.
We apply our study of state space relations in a performance comparison of several well-known automatic tools for security protocol analysis. We model a set of protocols and their properties as homogeneously as possible for each tool. We analyze the performance of the tools over comparable state spaces. This work enables us to effectively compare these automatic tools, i.e., using the same protocol description and exploring the same state space. We also propose some explanations for our experimental results, leading to a better understanding of the tools.
Cas J. F. Cremers, Pascal Lafourcade, Philippe Nadeau

Anonymous Consecutive Delegation of Signing Rights: Unifying Group and Proxy Signatures

We define a general model for consecutive delegations of signing rights with the following properties: The delegatee actually signing and all intermediate delegators remain anonymous. As for group signatures, in case of misuse, a special authority can open signatures to reveal all delegators’ and the signer’s identity. The scheme satisfies a strong notion of non-frameability generalizing the one for dynamic group signatures. We give formal definitions of security and show them to be satisfiable by constructing an instantiation proven secure under general assumptions in the standard model. Our primitive is a proper generalization of both group signatures and proxy signatures and can be regarded as non-frameable dynamic hierarchical group signatures.
Georg Fuchsbauer, David Pointcheval

Unconditionally Secure Blind Authentication Codes: The Model, Constructions, and Links to Commitment

In this paper, as a fundamental cryptographic protocol with information-theoretic security, we propose an unconditionally secure blind authentication code (BA-code for short) which is an unconditionally secure authentication code with anonymity of messages. As we will see, the BA-code is a simple model of an authentication code with the function similar to that of the unconditionally secure blind signature (USBS for short). The relationship between BA-codes and USBS is similar to the one between traditional authentication codes and unconditionally secure signature schemes as well as the one between group authentication codes and group signature schemes. In addition, we provide two kinds of constructions of BA-codes: direct constructions based on polynomials over finite fields, and a generic construction by using unconditionally secure encryption and A2-codes. Furthermore, as application we show a link between BA-codes and commitment in unconditional security setting: starting from BA-codes, unconditionally secure commitment schemes can be constructed in a black-box way.
Yuki Hara, Taiki Ishiwata, Junji Shikata, Tsutomu Matsumoto

New Anonymity Notions for Identity-Based Encryption

Identity-based encryption is a very convenient tool to avoid key management. Recipient-privacy is also a major concern nowadays. To combine both, anonymous identity-based encryption has been proposed. This paper extends this notion to stronger adversaries (the authority itself). We discuss this new notion, together with a new kind of non-malleability with respect to the identity, for several existing schemes. Interestingly enough, such a new anonymity property has an independent application to password-authenticated key exchange. We thus come up with a new generic framework for password-authenticated key exchange, and a concrete construction based on pairings.
Malika Izabachène, David Pointcheval

Computationally Sound Formalization of Rerandomizable RCCA Secure Encryption

Rerandomizing ciphertexts plays an important role in protecting privacy in security protocols such as mixnets. We investigate the relationship between formal and computational approaches to the analysis of the security protocols using a rerandomizable encryption scheme. We introduce a new method of dealing with composed randomnesses in an Abadi-Rogaway-style pattern, formalize a rerandomizable RCCA secure encryption scheme, and prove its computational soundness.
Yusuke Kawamoto, Hideki Sakurada, Masami Hagiya

Writing an OS Kernel in a Strictly and Statically Typed Language

OS kernels have been written in weakly typed or non typed programming languages, for example, C. Therefore, it is extremely hard to verify even simple memory safety of the kernels. The difficulty could be resolved by writing OS kernels in strictly typed programming languages, but existing strictly typed languages are not flexible enough to implement important OS facilities (e.g., memory management and multi-thread management facilities). To address the problem, we designed and implemented TALK, a new strictly and statically typed assembly language which is flexible enough to implement OS facilities, and wrote an OS kernel with TALK. In our approach, the safety of the kernel can be verified automatically through static type checking at the level of binary executables without source code.
Toshiyuki Maeda, Akinori Yonezawa


Weitere Informationen

Premium Partner