Slides of the talk. [pdf]
Abstract: I will try to explain why one needs something as mindboggling complicated as weak ω-groupoids to model Type Theory and report on our attempts to define this concept within Type Theory.
Slides of the talk. [ppt]
Abstract: Non-local games are cooperative games played by 2 or more players who cannot communicate against a referee. They are studied in the context of quantum information, as simple examples of information-theoretic models which show the difference between quantum mechanics and the classical world.
There are several known examples of non-local games which can be won by quantum strategies with a higher probability than classically. We show that the advantage for quantum strategies is very wide-spread. Namely, we look at random instances of nonlocal games, chosen randomly among all 2-player XOR games (a commonly studied class of non-local games). We discover that, for large n, the quantum value of a random 2-player XOR game with n questions to every player is at least 1.21... times the classical value, for 1-o(1) fraction of all 2-player XOR games.
(Joint work with Artus Backurs, Kaspars Balodis, Dmitry Kravchenko, Juris Smotrovs and Madars Virza.)
Slides of the talk. [pdf]
Abstract: Stated and proved by Edward F. Moore in 1962, the Garden-of-Eden theorem was the first formal result in the field of cellular automata. Wonderfully simple in its statement---a two-dimensional CA with two mutually erasable patterns has an unreachable pattern---it gave the start to a long series of results, linking surjectivity of the global map to other noteworthy properties.
This talk will illustrate several of the above, and also some of our contributions, which go in the direction of the recent theorem by Laurent Bartholdi showing that Moore's Garden-of-Eden property characterizes an important class of groups.
(Joint work with Pierre Guillon (CNRS & IML Marseille) and Jarkko Kari (University of Turku).)
Slides of the talk. [pdf]
Abstract: As there may be a need to change a part of a message without invalidating a digital signature, many sanitizable signature schemes have been proposed. Chameleon hashes may be used to modify a message by creating collisions in the hash using a secret trapdoor key; the hash is computed using the sanitizer's public key. In addition, we are interested in maintaining forward security due to the possibility of key exposure, a topic well studied in digital signature schemes. We explore constructions in both the identity-based setting as well as the public-key setting. In the identity-based setting where an entity's public key is that entity's name, our aim is to allow sanitizations in digital signature schemes which provide forward security. The public key of the key generation center and all private keys are updated during each time period. Then, if time allows, we propose a construction of a chameleon hash scheme in the public-key setting.
(Joint work with Peeter Laud.)
Slides of the talk. [ppt]
Abstract: Probabilistically checkable proofs make it possible to spot-check a proof in random locations instead of reading the entire proof. We will use this property to build short non-interactive zero-knowledge proofs that allow a prover to send a proof to a verifier to convince him of the truth of a statement without revealing any other information. While PCPs have been used in interactive zero-knowledge proofs, the use in non-interactive zero-knowledge proofs is somewhat counterintuitive because the lack of interaction means the verifier cannot communicate to the prover which spots he wishes to check. Instead the verifier will actually check all places in the PCP, but due to the properties of the PCP this can be done in a sloppier way than usual resulting in a performance improvement.
As another contribution we will discuss efficient ways to implement a hidden random string, i.e., a string of uniformly random bits that are hidden to the verifier and that the prover can choose to disclose individually. Using a factoring-based encryption scheme such as Naccache-Stern this can be accomplished with only a logarithmic overhead. Combining our two new techniques we can build NIZK proofs that have very good asymptotic efficiency.
Slides of the talk. [pdf]
Abstract: DPLL (named in the honour of the authors: Davis, Putnam, Logemann and Loveland) algorithms are one of the most popular approach to the problem of satisfiability of Boolean formulas (SAT). DPLL algorithm is a recursive algorithm that takes the input formula F, uses a procedure A to choose a variable x, uses a procedure B to chooses the value a ∈ {0,1} for the variable x that would be investigated first, and makes two recursive calls on inputs F[x:=a] the F[x:=1-a].
We will overview known results on lower bounds for DPLL algorithms on unsatisfiable and satisfiable instances and discuss connection of lower bounds for satisfiable instances with cryptography. We will also consider DPLL algorithms with a cut heuristic that may decide that some branch of the splitting tree will not be investigated and suggest lower bounds for this model.
Slides of the talk. [pdf]
Abstract: A Boolean function f : F2n → F2 is called an affine disperser of dimension d, if f is not constant on any affine subspace of F2n of dimension at least d. Recently Ben-Sasson and Kopparty gave an explicit construction of an affine disperser for sublinear d. The main motivation for studying such functions comes from extracting randomness from structured sources of imperfect randomness. In the talk, we will show another application -- a very simple proof of a 3n-o(n) lower bound on the circuit complexity (over the full binary basis) of affine dispersers for sublinear dimension. The same lower bound 3n-o(n) (but for a completely different function) was given by Blum in 1984 and is still the best known.
Slides of the talk. [odp]
Abstract: We consider an object-oriented distributed language with asynchronous method calls, futures and intra-object synchronization. We show how to translate this language into a dialect of applied π-calculus. Our translation preserves all possible observations that can be made about the program, even in the presence of an active adversary in the environment.
Abstract: We propose a new pairing-based non-interactive perfectly zero-knowledge shuffle argument that has smaller communication and is based on more standard computational cryptographic assumptions than the only previously known efficient non-interactive zero-knowledge shuffle argument by Groth and Lu. Differently from Groth and Lu who only prove the culpable soundness (a weaker version of computational soundness) of their argument, we provide a proof of the computational soundness. Due to well-known impossibility results this means that we also have to use a knowledge assumption. We first construct an efficient permutation matrix argument by using recent non-interactive zero-knowledge techniques of Groth and Lipmaa, and then use it to construct a non-interactive shuffle argument for a knowledge version of the Boneh-Boyen-Shacham cryptosystem.
(Joint work with Bingsheng Zhang.)
Slides of the talk. [pdf]
Abstract: In the Infrastructure-as-a-Service (IaaS) cloud computing market, spot instances refer to virtual servers that are rented via an auction. Spot instances allow IaaS providers to sell spare capacity while enabling IaaS users to acquire virtual servers at a lower pricer than the regular market price (also called "on demand" price). Users bid for spot instances at their chosen limit price. Based on the bids and the available capacity, the IaaS provider sets a clearing price. A bidder acquires their requested spot instances if their bid is above the clearing price. However, these spot instances may be terminated by the IaaS provider impromptu if the auction's clearing price goes above the user's limit price. In this context, this paper addresses the following question: Can spot instances be used to run paid web services while achieving performance and availability guarantees? In this talk I will examine the problem faced by a Software-asa-Service (SaaS) provider who rents spot instances from an IaaS provider and uses them to provide a web service on behalf of a paying customer. The SaaS provider incurs a monetary cost for renting computing resources from the IaaS provider, while charging its customer for executing web service transactions and paying penalties to the customer for failing to meet performance and availability objectives. To address this problem, a bidding scheme and server allocation policies designed to optimize the average revenue earned by the SaaS provider per time unit are proposed.
Slides of the talk. [pdf]
Abstract: In transfinite semantics, programs can continue running after infinite loops from some limit states. Transfinite semantics provides a way to overcome so-called semantic anomaly in program transformation such as slicing. Semantic anomaly rises if infinite loops can be cut out from programs by the transformation, whence a resulting program can reach farther in the code than the original program can ever do during any finite period.
Transfinite semantics have been criticized because in the forms they have been proposed, they have often had rather artificial construction and lacked of desired properties such as compositionality and substitutivity. In our ongoing work, we construct a compositional (and hence also substitutive) transfinite semantics suitable for use in program slicing theory. We show that standard trace semantics is its straightforward abstraction and, on the other hand, establish its connection to transfinite semantics given in the form of greatest fixpoint.
Slides of the talk. [pdf]
Abstract: We propose a new approach to practical two-party computation secure against an active adversary. All prior practical protocols were based on Yao's protocol. We use an OT-based approach and get efficiency via OT extension. To get a practical protocol we introduce a number of novel techniques for relating the outputs and inputs of OTs in a larger computation. We also report on an implementation of this approach that shows that our protocol is more efficient than any previous one. As an example, evaluating a Boolean circuit of about 34000 gates (oblivious AES encryption) takes less than 2 seconds using our protocol.
Slides of the talk. [ppt]
Abstract: Bilinear mappings are quite powerful mathematical structures that can be used in cryptography. They allow constructing cryptographic primitives that would be otherwise ineffective or even impossible. In formal cryptography, the protocols are based on term algebras and process calculi, and can be represented through Horn clauses for analysis purposes. The security of these protocols can be tested with analyzers based on resolution methods. However, there are problems with realization of arithmetic operations. It is easy to compute g^a if the values of both g and a are known, but the values are usually undefined in the protocols. Some research works have been written about the representation of exponentiation in formal model, but there are still many things that should be done. In this work, an attempt to implement an analysis of bilinear mappings in formal cryptography has been done.
Slides of the talk. [pdf]
Abstract: We present an information-flow type system for a distributed object-oriented language with active objects, asynchronous method calls and futures. The variables of the program are classified as high and low. We allow while cycles with high guards to be used but only if they are not followed (directly or through synchronization) by an assignment to a low variable. To ensure the security of synchronization, we use a high and a low lock for each concurrent object group (cog). In some cases, we must allow a high lock held by one task to be overtaken by another, if the former is about to make a low side effect but the latter cannot make any low side effects. This is necessary to prevent synchronization depending on high variables from influencing the order of low side effects in different cogs. We have proved a non-interference result for our type system.
(Joint work with Peeter Laud, to be presented at SOFSEM 2012.)
Slides of the talk. [pdf]
Abstract: In this talk, we will present the first results on AIDA/cube side-channel attacks on variable number of rounds of all members of the KATAN flamily of block ciphers. Our cube attacks reach 60, 40 and 30 rounds of KATAN32, KATAN48 and KATAN64, respectively. We show how to perform side channel attacks on the full 254-round KATAN32 with one-bit information leakage from the internal state by cube attacks.
(Joint work with G. V. Bard, N. Courtois, J. Nakahara and P. Sepehrdad.)
Slides of the talk. [pdf]
Abstract: We show that every regular language defines a unique nondeterministic finite automaton (NFA), which we call "átomaton", whose states are the "atoms" of the language, that is, non-empty intersections of complemented or uncomplemented left quotients of the language.
We introduce "atomic" NFAs, in which the right language of every state is a union of some atoms. This class of automata is a generalization of residual automata in which the right language of any state is a left quotient (which we prove to be a union of atoms), and includes also átomata (where the right language of any state is an atom), trim DFAs, and the trim parts of universal automata.
Our main result is a characterization of the class of NFAs for which the subset construction yields a minimal DFA. More specifically, we show that the subset construction applied to a trim NFA produces a minimal DFA if and only if the reverse automaton of that NFA is atomic. This is a generalization of Brzozowski's method for DFA minimization by double reversal.
(Joint work with Janusz Brzozowski, presented at DLT 2011.)
Abstract: Increasing attention has recently been given to the formal verification of the source code of cryptographic protocols. The standard approach is to use symbolic abstractions of cryptography that make the analysis amenable to automation. This leaves the possibility of attacks that exploit the mathematical properties of the cryptographic algorithms themselves.
In this talk we explain how to leverage so-called computational soundness results to perform a verification on the source code level (F# in this case) that takes into account the properties of the actual cryptographic algorithms.
Slides of the talk. [pdf]
Abstract: Bove and Capretta's popular method for justifying function definitions by general recursive equations is based on the observation that any structured general recursion equation defines an inductive subset of the intended domain (the "domain of definedness") for which the equation has a unique solution. To accept the definition, it is hence enough to prove that this subset contains the whole intended domain.
This approach works very well for "terminating" definitions. But it fails to account for "productive" definitions, such as typical definitions of stream-valued functions. I will argue that such definitions can be treated in a similar spirit, proceeding from a different unique solvability criterion. Any structured recursion equation defines a coinductive relation between the intended domain and intended codomain (the "coinductive graph"). This relation in turn determines a subset of the intended domain and a quotient of the intended codomain with the property that the equation is uniquely solved for the subset and quotient. The equation is therefore guaranteed to have a unique solution for the intended domain and intended codomain whenever the subset is the full set and the quotient is by equality.
Slides of the talk. [pdf]
Abstract: In an attempt to create a presentation with the messiest title for these Theory Days, we consider the problem of building an oblivious shuffle protocol as a series of resharing steps. For each step, a defender set consisting of some miner nodes of the underlying secret sharing scheme is selected, and the database is reshared among them. It turns out that the problem of selecting the optimal structure of the defender sets is a non-trivial one. In this talk we define the problem combinatorially and give some exact values and some bounds for the threshold case. There will be many open ends available for the mathematically-minded audience to explore.
Slides of the talk. [pptx]
Abstract: In classical Arthur-Merlin games (AM), the class of languages whose membership proofs can be verified by Arthur using logarithmic space coincides with the class P. In this note, we show that if Arthur has a fixed-size quantum register (the size of the register does not depend on the length of the input) instead of another source of random bits, membership in any language in NP can be verified with any desired error bound.
(Joint work with A. C. Cem Say.)