*18:17* [Pub][ePrint]
Revisiting Security Claims of XLS and COPA, by Mridul Nandi
Ristenpart and Rogaway proposed XLS in 2007 which is ageneric method to encrypt messages with incomplete last blocks. Later

Andreeva et al., in 2013 proposed an authenticated encryption COPA

which uses XLS while processing incomplete message blocks. Following

the design of COPA, several other CAESAR candidates used the similar

approach. Surprisingly in 2014, Nandi showed a three-query distinguisher against XLS which violates the security claim of XLS and puts a question mark on all schemes using XLS. However, due to the interleaved nature of encryption and decryption queries of the distinguisher, it was not clear whether the security claims of COPA remains true or not. This paper revisits XLS and COPA both in the direction of cryptanalysis and provable security. Our contribution of the paper can be summarized into following two parts:

1. Cryptanalysis: We describe two attacks - (i) a new distinguisher

against XLS and extending this attack to obtain (ii) a forging algo-

rithm with query complexity about 2^n/3 against COPA where n is

the block size of the underlying blockcipher.

2. Security Proof: Due to the above attacks the main claims of XLS

(already known before) and COPA are wrong. So we revise the security analysis of both and show that (i) both XLS and COPA are

pseudorandom function or PRF up to 2^n/2 queries and (ii) COPA is

integrity-secure up to 2^n/3 queries (matching the query complexity

of our forging algorithm).

*18:17* [Pub][ePrint]
XLS is not a Strong Pseudorandom Permutation, by Mridul Nandi
In FSE 2007, Ristenpart and Rogaway had described a genericmethod XLS to construct a length-preserving strong pseudorandom per-

mutation (SPRP) over bit-strings of size at least n. It requires a length-preserving permutation E over all bits of size multiple of n and a blockcipher E with block size n. The SPRP security of XLS was proved from the SPRP assumptions of both E and E. In this paper we disprove the claim by demonstrating a SPRP distinguisher of XLS which makes only

three queries and has distinguishing advantage about 1/2. XLS uses a

multi-permutation linear function, called mix2. In this paper, we also

show that if we replace mix2 by any invertible linear functions, the construction XLS still remains insecure. Thus the mode has inherit weakness.

*18:17* [Pub][ePrint]
On the Amortized Complexity of Zero-knowledge Protocols, by Ronald Cramer and Ivan Damgård and Marcel Keller
We propose a general technique that allows improving the complexity ofzero-knowledge protocols for a large class of problems where

previously the best known solution was a simple cut-and-choose style

protocol, i.e., where the size of a proof for problem instance $x$ and

error probability $2^{-n}$ was $O(|x| n)$ bits. By using our technique

to prove $n$ instances simultaneously, we can bring down the proof

size per instance to $O(|x| + n)$ bits for the same error probability

while using no computational assumptions. Examples where our technique

applies include proofs for quadratic residuosity, proofs of subgroup

membership and knowledge of discrete logarithms in groups of unknown

order, interval proofs of the latter, and proofs of plaintext

knowledge for various types of homomorphic encryption schemes. We

first propose our protocols as $\\Sigma$-protocols and extend them

later to zero-knowledge proofs of knowledge.

*12:17* [Pub][ePrint]
A Hybrid Approach for Proving Noninterference of Java Programs, by Ralf Kuesters and Tomasz Truderung and Bernhard Beckert and Daniel Bruns and Michael Kirsten and Martin Mohr
Several tools and approaches for proving noninterference properties for Java and other languages exist. Some of them have a high degree of automation or are even fully automatic, but overapproximate the actual information flow, and hence, may produce false positives. Other tools, such as those based on theorem proving, are precise, but may need interaction, and hence, analysis is time-consuming.In this paper, we propose a \\emph{hybrid approach} that aims at obtaining the best of both approaches: We want to use fully automatic analysis as much as possible and only at places in a program where, due to overapproximation, the automatic approaches fail, we resort to more precise, but interactive analysis, where the latter involves the verification only of specific functional properties in certain parts of the program, rather than checking more intricate noninterference properties for the whole program.

To illustrate the hybrid approach, in a case study we use this approach---along with the fully automatic tool Joana for checking noninterference properties for Java programs and the theorem prover KeY for the verification of Java programs--- as well as the CVJ framework proposed by K{\\\"u}sters, Truderung, and Graf to establish cryptographic privacy properties for a non-trivial Java program, namely an e-voting system. The CVJ framework allows one to establish cryptographic indistinguishability properties for Java programs by checking (standard) noninterference properties for such programs.

*12:17* [Pub][ePrint]
On Concurrently Secure Computation in the Multiple Ideal Query Model, by Vipul Goyal and Abhishek Jain
The multiple ideal query (MIQ) model was introduced by Goyal, Jain and Ostrovsky [Crypto\'10] as a relaxed notion of security which allows one to construct concurrently secure protocols in the plain model. The main question relevant to the MIQ model is how many queries must we allow to the ideal world adversary? The importance of the above question stems from the fact that if the answer is positive, then it would enable meaningful security guarantees in many application scenarios, as well as, lead to resolution of long standing open questions such as fully concurrent password based key exchange in the plain model.In this work, we continue the study of the MIQ model and prove severe lower bounds on the number of ideal queries per session. Following are our main results:

1) There exists a two-party functionality that cannot be securely realized in the MIQ model with only a constant number of ideal queries per session.

2) There exists a two-party functionality that cannot be securely realized in the MIQ model by any constant round protocol, with any polynomial number of ideal queries per session.

Both of these results are unconditional and even rule out protocols proven secure using a non-black-box simulator. We in fact prove a more general theorem which allows for trade-off between round complexity and the number of ideal queries per session. We obtain our negative results in the following two steps:

1) We first prove our results with respect to black-box simulation, i.e., we only rule out simulators that make black-box use of the adversary.

2) Next, we give a technique to compile our negative results w.r.t. black-box simulation into full impossibility results (ruling out non-black-box simulation as well) in the MIQ model. Interestingly, our compiler uses ideas from the work on obfuscation using tamper-proof hardware, even though our setting does not involve any hardware tokens.

*12:17* [Pub][ePrint]
Message-Locked Encryption for Lock-Dependent Messages, by Martín Abadi and Dan Boneh and Ilya Mironov and Ananth Raghunathan and Gil Segev
Motivated by the problem of avoiding duplication in storage systems, Bellare, Keelveedhi, and Ristenpart have recently put forward the notion of Message-Locked Encryption (MLE) schemes which subsumes convergent encryption and its variants. Such schemes do not rely on permanent secret keys, but rather encrypt messages using keys derived from the messages themselves.We strengthen the notions of security proposed by Bellare et al. by considering plaintext distributions that may depend on the public parameters of the schemes. We refer to such inputs as lock-dependent messages. We construct two schemes that satisfy our new notions of security for message-locked encryption with lock-dependent messages.

Our main construction deviates from the approach of Bellare et al. by avoiding the use of ciphertext components derived deterministically from the messages. We design a fully randomized scheme that supports an equality-testing algorithm defined on the ciphertexts.

Our second construction has a deterministic ciphertext component that enables more efficient equality testing. Security for lock-dependent messages still holds under computational assumptions on the message distributions produced by the attacker.

In both of our schemes the overhead in the length of the ciphertext is only additive and independent of the message length.

*12:17* [Pub][ePrint]
Enhancing Trust in Reconfigurable Based Hardware Systems with Tags and Monitors, by Devu Manikantan Shila and Vivek Venugopalan and Cameron D Patterson
Extensive use of third party IP cores (e.g., HDL, netlist) and open source tools in the FPGA application design and development process in conjunction with the inadequate bitstream protection measures have raised crucial security concerns in the past for reconfigurable hardware systems. Designing high fidelity and secure methodologies for FPGAs are still infancy and in particular, there are almost no concrete methods/techniques that can ensure trust in FPGA applications not entirely designed and/or developed in a trusted environment. This work strongly suggests the need for an anomaly detection capability within the FPGAs that can continuously monitor the behavior of the underlying FPGA IP cores and the communication activities of IP cores with other IP cores or peripherals for any abnormalities. To capture this need, we propose a technique called FIDelity Enhancing Security (FIDES) methodology for FPGAs that uses a combination of access control policies and behavior learning techniques for anomaly detection. FIDES essentially comprises of two components: (i) {\\em Trusted Wrappers}, a layer of monitors with sensing capabilities distributed across the FPGA fabric; these wrappers embed the output of each IP core $i$ with a tag $\\tau_i$ according to the pre-defined security policy $\\Pi$ and also verifies the embeddings of each input to the IP core to detect any violation of policies. The use of tagging and tracking enables us to capture the generalized interactions of each IP core with its environment (e.g., other IP cores, memory, OS or I/O ports). {\\em Trusted Wrappers} also monitors the statistical properties exhibited by each IP core functions on execution such as power consumption, number of clock cycles and timing variations to detect any anomalous operations; (ii) a {\\em Trusted Anchor} that monitors the communication between the IP cores and the peripherals with regard to the centralized security policies $\\Psi$ and the statistical properties produced by the peripherals. We target FIDES architecture on a Xilinx Zynq 7020 device for a red-black system comprising of sensitive and non-sensitive IP cores. Our FIDES implementation leads to only 1-2\\% overhead in terms of the logic resources per wrapper but 4-5X increase in latency (worst case scenario), measured in terms of clock cycles, as compared to the baseline implementation.