Composable Security Analysis of OS Services
We provide an analytical framework for analyzing basic integrity properties of file systems, namely the binding of files to filenames and writing capabilities. A salient feature of our modeling and analysis is that it is *composable*: In spite of the fact that we analyze the filesystem in isolation, security is guaranteed even when the file system operates as a component within an arbitrary, and potentially adversarial system. Such secure composability properties seem essential when trying to assert the security of large systems. Our results are obtained by adapting the *Universally Composable* (UC) security framework to the analysis of software systems. Originally developed for cryptographic protocols, the UC framework allows the analysis of simple components in isolation, and provides assurance that these components maintain their behavior when combined in a large system, potentially under adversarial conditions.
Mitigating Dictionary Attacks on Password-Protected Local Storage
We address the issue of encrypting data in local storage using a key that is derived from the user's password. The typical solution in use today is to derive the key from the password using a cryptographic hash function. This solution provides relatively weak protection, since an attacker that gets hold of the encrypted data can mount an off-line dictionary attack on the user's password, thereby recovering the key and decrypting the stored data. We propose an approach for limiting off-line dictionary attacks in this setting without relying on secret storage or secure hardware. In our proposal, the process of deriving a key from the password requires the user to solve a puzzle that is presumed to be solvable only by humans (e.g, a CAPTCHA). We describe a simple protocol using this approach: many different puzzles are stored on the disk, the user's password is used to specify which of them need to be solved, and the encryption key is derived from the password and the solutions of the specified puzzles. Completely specifying and analyzing this simple protocol, however, raises a host of modeling and technical issues, such as new properties of human-solvable puzzles and some seemingly hard combinatorial problems. Here we analyze this protocol in some interesting special cases.
Hardness amplification of weakly verifiable puzzles
Is it harder to solve many puzzles than it is to solve just one? This question has different answers, depending on how you define puzzles. For the case of inverting one-way functions it was shown by Yao that solving many independent instances simultaneously is indeed harder than solving a single instance (cf. the transformation from weak to strong one-way functions). The known proofs of that result, however, use in an essential way the fact that for one-way functions, verifying candidate solutions to a given puzzle is easy. We extend this result to the case where solutions are efficiently verifiable only by the party that generated the puzzle. We call such puzzles weakly verifiable. That is, for weakly verifiable puzzles we show that if no efficient algorithm can solve a single puzzle with probability more than $\eps$, then no efficient algorithm can solve $n$ independent puzzles simultaneously with probability more than $\eps^n$. We also demonstrate that when the puzzles are not even weakly verifiable, solving many puzzles may be no harder than solving a single one. Hardness amplification of weakly verifiable puzzles turns out to be closely related to the reduction of soundness error under parallel repetition in computationally sound arguments. Indeed, the proof of Bellare, Impagliazzo and Naor that parallel repetition reduces soundness error in three-round argument systems implies a result similar to our first result, albeit with considerably worse parameters. Also, our second result is an adaptation of their proof that parallel repetition of four-round systems may not reduce the soundness error.
Assumptions Related to Discrete Logarithms: Why Subtleties Make a Real Difference
The security of many cryptographic constructions relies on assumptions related to Discrete Logarithms (DL), e.g., the Diffie-Hellman, Square Exponent, Inverse Exponent or Representation Problem assumptions. In the concrete formalizations of these assumptions one has some degrees of freedom offered by parameters such as computational model, problem type (computational, decisional) or success probability of adversary. However, these parameters and their impact are often not properly considered or are simply overlooked in the existing literature. In this paper we identify parameters relevant to cryptographic applications and describe a formal framework for defining DL-related assumptions. This enables us to precisely and systematically classify these assumptions. In particular, we identify a parameter, termed granularity, which describes the underlying probability space in an assumption. Varying granularity we discover the following surprising result: We prove that two DL-related assumptions can be reduced to each other for medium granularity but we also show that they are provably not reducible with generic algorithms for high granularity. Further we show that reductions for medium granularity can achieve much better concrete security than equivalent high-granularity reductions.