*18:17* [Pub][ePrint]
Ad-Hoc Secure Two-Party Computation on Mobile Devices using Hardware Tokens, by Daniel Demmler and Thomas Schneider and Michael Zohner
Secure two-party computation allows two mutually distrusting parties to jointly compute an arbitrary function on their private inputs without revealing anything but the result. An interesting target for deploying secure computation protocols are mobile devices as they contain a lot of sensitive user data. However, their resource restrictions make this a challenging task.In this work, we optimize and implement the secure computation protocol by Goldreich-Micali-Wigderson~(GMW) on mobile phones. To increase performance, we extend the protocol by a trusted hardware token (i.e., a smartcard). The trusted hardware token allows to pre-compute most of the workload in an initialization phase, which is executed locally on one device and can be pre-computed independently of the later communication partner. We develop and analyze a proof-of-concept implementation of generic secure two-party computation on Android smart phones making use of a microSD smartcard. Our use cases include private set intersection for finding shared contacts and private scheduling of a meeting with location preferences. For private set intersection, our token-aided implementation on mobile phones is up to two orders of magnitude faster than previous generic secure two-party computation protocols on mobile phones and even as fast as previous work on desktop computers.

*15:17* [Pub][ePrint]
Efficient Key-policy Attribute-based Encryption for General Boolean Circuits from Multilinear Maps, by Constantin Catalin Dragan and Ferucio Laurentiu Tiplea
We propose an efficient Key-policy Attribute-based Encryption (KP-ABE) scheme for general (monotone) Boolean circuits based on secret sharing and on a very particular and simple form of leveled multilinear maps,

called chained multilinear maps. The number of decryption key components is substantially reduced in comparison with the current scheme based on leveled multilinear maps, and the size of the multilinear map (in terms of bilinear map components) is less than the Boolean circuit depth, while it is quadratic in the Boolean circuit depth for the current scheme based on leveled multilinear map. Moreover, it is much easier to find chained multilinear maps than leveled multilinear maps. Selective security of the proposed schemes in the standard model is proved, under the decisional multilinear Diffie-Hellman assumption.

*15:17* [Pub][ePrint]
(Leveled) Fully Homomorphic Signatures from Lattices, by Sergey Gorbunov and Vinod Vaikuntanathan
In a homomorphic signature scheme, given a vector of signatures $\\vec{\\sigma}$ corresponding to a dataset of messages $\\vec{\\mu}$, there is a {\\it public} algorithm that allows to derive a signature $\\sigma\'$ for message $\\mu\'=f(\\vec{\\mu})$ for any function $f$. Given the tuple $(\\sigma\', \\mu\', f)$ anyone can {\\it publicly}

verify the result of the computation of function $f$.

Along with the standard notion of unforgeability

for signatures, the security of homomorphic signatures guarantees that no adversary is able to make a forgery $\\sigma^*$ for $\\mu^* \\neq f(\\vec{\\mu})$.

We construct the first homomorphic signature scheme for evaluating arbitrary functions. In our scheme, the public parameters and the size of the resulting signature grows linearly

with the depth of the circuit representation of $f$. Our scheme is secure in the standard model assuming hardness of

finding {\\it Small Integer Solutions} in hard lattices.

Furthermore, our construction has asymptotically fast verification

which immediately leads to a new solution for verifiable outsourcing with pre-processing phase. Previous state of the art constructions were limited to evaluating polynomials of constant degree, secure in random oracle model

without asymptotically fast verification.

*15:17* [Pub][ePrint]
Semi-Adaptive Attribute-Based Encryption and Improved Delegation for Boolean Formula, by Jie Chen and Hoeteck Wee
We consider *semi-adaptive* security for attribute-based encryption,where the adversary specifies the challenge attribute vector after

it sees the public parameters but before it makes any secret key

queries. We present two constructions of semi-adaptive

attribute-based encryption under static assumptions with *short*

ciphertexts. Previous constructions with short ciphertexts either

achieve the weaker notion of selective security, or require

parameterized assumptions.

As an application, we obtain improved delegation schemes for Boolean

formula with *semi-adaptive* soundness, where correctness of the

computation is guaranteed even if the client\'s input is chosen

adaptively depending on its public key. Previous delegation schemes

for formula achieve one of adaptive soundness, constant

communication complexity, or security under static assumptions; we

show how to achieve semi-adaptive soundness and the last two

simultaneously.

*15:17* [Pub][ePrint]
On a new properties of number sequences ,a randomness test and a new RC4\'s key scheduling algorithm., by Samir Bouftass and Abdelhak Azhari
In this paper, we introduce the concept of the derivative of sequence of numbers and define new statistical indices by which we discoverd new properties of randomly generated number sequences.We also build a test for pseudo random generators based on these properties and use it to confirm the weakness of RC4 key scheduling algorithm that has been reported in the litterature.

In this rescpect we publish a new RC4\'s key scheduling algorithm that don\'t have this weakness.

*12:17* [Pub][ePrint]
Single-shot security for one-time memories in the isolated qubits model, by Yi-Kai Liu
One-time memories (OTM\'s) are simple, tamper-resistant cryptographic devices, which can be used to implement sophisticated functionalities such as one-time programs. Can one construct OTM\'s whose security follows from some physical principle? This is not possible in a fully-classical world, or in a fully-quantum world, but there is evidence that OTM\'s can be built using \"isolated qubits\" -- qubits that cannot be entangled, but can be accessed using adaptive sequences of single-qubit measurements.Here we present new constructions for OTM\'s using isolated qubits, which improve on previous work in several respects: they achieve a stronger \"single-shot\" security guarantee, which is stated in terms of the (smoothed) min-entropy; they are proven secure against adversaries who can perform arbitrary local operations and classical communication (LOCC); and they are efficiently implementable.

These results use Wiesner\'s idea of conjugate coding, combined with error-correcting codes that approach the capacity of the q-ary symmetric channel, and a high-order entropic uncertainty relation, which was originally developed for cryptography in the bounded quantum storage model.

*12:17* [Pub][ePrint]
Verified Implementations for Secure and Verifiable Computation, by José Bacelar Almeida and Manuel Barbosa and Gilles Barthe and Guillaume Davy and François Dupressoir and Benjamin Grégoire and Pie
Formal verification of the security of software systems is gradually moving from the traditional focus on idealized models, to the more ambitious goal of producing verified implementations. This trend is also present in recent work targeting the verification of cryptographic software, but the reach of existing tools has so far been limited to cryptographic primitives, such as RSA-OAEP encryption, or standalone protocols, such as SSH. This paper presents a scalableapproach to formally verifying implementations of higher-level cryptographic systems, directly in the computational model.

We consider circuit-based cloud-oriented cryptographic protocols for secure and verifiable computation over encrypted data. Our examples share as central component Yao\'s celebrated transformation of a boolean circuit into an equivalent garbled form that can be evaluated securely in an untrusted environment. We leverage the foundations of garbled circuits set forth by Bellare, Hoang, and Rogaway (CCS 2012, ASIACRYPT 2012) to build verified implementations of garbling schemes, a verified implementation of Yao\'s secure

function evaluation protocol, and a verified (albeit partial) implementation of the verifiable computation protocol by Gennaro, Gentry, and Parno (CRYPTO 2010). The implementations are formally verified using EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, and critically rely on two novel features: a module and theory system that supports compositional reasoning, and a code extraction mechanism for generating

implementations from formalizations.

*12:17* [Pub][ePrint]
Automated Analysis of Cryptographic Assumptions in Generic Group Models, by Gilles Barthe and Edvard Fagerholm and Dario Fiore and John Mitchell and Andre Scedrov and Benedikt Schmidt
We initiate the study of principled, automated, methods for analyzing hardness assumptions in generic group models, following the approach of symbolic cryptography. We start by defining a broad class of generic and symbolic group models for differentsettings---symmetric or asymmetric (leveled) k-linear groups---and by

proving \"computational soundness\" theorems for the symbolic models.

Based on this result, we formulate a very general master theorem that formally relates the hardness of a (possibly interactive) assumption in these models to solving problems in polynomial algebra. Then, we systematically analyze these problems. We identify different classes of assumptions and obtain decidability and undecidability results.

Then, we develop and implement automated procedures for verifying the conditions of master theorems, and thus the validity of hardness assumptions in generic group models. The concrete outcome of this work is an automated tool which takes as input the statement of an assumption, and outputs either a proof of its

generic hardness or shows an algebraic attack against the assumption.