Slides of the talk. [pdf]

*Abstract:* What is the shortest proof of a given statement?
Are there Boolean tautologies that require exponential-size proofs?
These are typical questions in propositional proof complexity.

In my short tutorial I will speak on two aspects of this topic. The first one concerns specific proof systems and lower bounds on the proof length there. The second one concerns structural questions: is there the "best" proof system?

*Abstract:* Language Engineering is an interdisciplinary area
addressing many problems related to computer languages. Parsing and
translation are the most widely known ones, but there are many more:
typing and other static analyses, creating IDEs, which includes syntax
highlighting, building outlines, code navigation, completion and
refactoring, and many more. Many of such problems are solved in a
generative fashion: we write high-level specifications (like grammars
with embedded semantic actions for parsing) and generate code from
them.

Now if we come up with a language (which is an everyday practice if you consider DSLs) we have to specify many things for it. The problem is that specification languages are built upon a grammar of the language in question (e.g. for parsing we embed semantic actions into grammar rules, other languages work the same way) and if we specify many solutions separately, we have to duplicate the grammar. The alternative approach is to attach all the specifications to the same grammar which leads to huge tangled specifications.

We propose a solution for this problem based on usage of a pointcut-advice language inspired by AspectJ to attach specifications to a grammar without mixing them together. This language was successfully applied to specify attributed translation, IDE features and grammar transformations.

Slides of the talk. [pdf]

*Abstract:* The Cantor (product) topology, which is the
default setting for cellular automata (CA) dynamics, has the
disadvantage of making the shift a chaotic map. Consequently, no
translation-invariant distance can induce the product topology.

To overcome this, Formenti et al. introduced in 1999 the Besicovitch and Weyl pseudo-distances on bi-infinite words. By identifying configurations at pseudo-distance zero, new topological spaces are obtained, whose properties are dramatically different from those of the Cantor space. Remarkably, 1D CA induce are well-defined over equivalence classes, and several properties of the induced functions on these new spaces are linked to those of the original CA.

In this talk, we illustrate the original formulation and the main results on 1D CA. We then switch to a generalization to higher dimension, and show how several of those results still hold. We will focus in particular on surjectivity, both of CA and of induced maps.

Slides of the talk. [pdf]

*Abstract:* Monads and the intimately related concept of
adjunctions are perhaps *the* central topic in category
theory. Mathematics and computer science are littered with examples of
them. Motivated by some persuasive examples that are nearly monads but
not quite, we generalise the theory of monads and adjunctions to allow
monads which are not endofunctors. In this talk, I will describe the
basic setup and some examples. (Joint work with Thorsten
Altenkirch and Tarmo Uustalu.)

Slides of the talk. [pdf]

*Abstract:* In *set system auctions*, a single auctioneer
needs to purchase services from multiple competing selfish providers
(agents), and the set of providers has a combinatorial structure; a
popular example is provided by shortest path auctions. Each agent
*i* can perform a simple task at some cost *c _{i}*
known only to himself. Based on the agents' bids

A truthful mechanism for winners selection and payments to them is
a mechanism, which forces each agent *i* to say
*c _{i}* for his bid

Slides of the talk. [pdf]

*Abstract:* We study the problem of generating a database and
parameters for a given parameterized SQL query satisfying a given test
condition. We introduce a formal background theory that includes
arithmetic, tuples, and sets, and translate the generation problem
into a satisfiability or model generation problem modulo the
background theory. We use the satisfiability modulo theories (SMT)
solver Z3 in the concrete implementation. We describe an application
of model generation in the context of the database unit testing
framework of Visual Studio. (Joint work with Margus Veanes, Peli de
Halleux, Nikolai Tillmann.)

Slides of the talk. [pdf]

*Abstract:* We will give a short introduction to circuit
complexity lower bounds -- one of the oldest and most difficult
branches of Theoretical Computer Science. We will first survey some
known lower bounds for various circuit models. Then we will
concentrate on the so-called gate elimination method. This is
essentially the only known method for proving lower bounds for
unrestricted circuits.

Slides of the talk. [pdf]

*Abstract:* Reiter and Rubin's Crowds (TISSEC 1998) is a
system for communicating anonymously, using a peer-to-peer network (a
crowd) to pass messages. A related scheme, ADU, presented by Munoz Gea
et al. at ESORICS 2008, was claimed to improve on Crowds by
achieving lower message path length variance for the same mean
latency, without a compromise in security.

We present traffic analysis of the ADU anonymity scheme and show that optimal attacks are able to de-anonymize ADU messages more effectively than in the case of Crowds. We then generalize Crowds to support any path length distribution, while leaking the least possible information, and quantify the optimal attacks. This allows us to prove that the original Crowds anonymity system provides the best security for any given mean messaging latency and hence, the search of a "better" scheme is bound to fail. (Joint work with George Danezis, Claudia Diaz and Carmela Troncoso.)

Slides of the talk. [pdf]

*Abstract:* In this talk, we report the results of the formal
analysis performed on the Estonian Mobile-ID protocol (deployed since
2008), allowing citizens and permanent residents of Estonia to
authenticate themselves and issue digital signatures with the help of
a signature-capable SIM-card inside their mobile phone. We analyze the
resiliency of the protocol to network attacks under various threat
models (compromised infrastructure, client application, etc.,
confusing user interface) and give suggestions for improvement. (Joint
work with Meelis Roos.)

Slides of the talk. [pdf]

*Abstract:* First, we show how to express an arbitrary integer
interval $I = [0, H]$ as a sumset $I = \sum_{i=1}^\ell G_i * [0, u -
1] + [0, H']$ of smaller integer intervals for some small values
$\ell$, $u$, and $H' < u - 1$, where $b * A = \{b a : a \in A\}$ and
$A + B = \{a + b : a \in A \land b \in B\}$. We show how to derive
such expression of $I$ as a sumset for any value of $1 < u < H$, and
in particular, how the coefficients $G_i$ can be found by using a
non-trivial but efficient algorithm. This result may be interesting by
itself in the context of additive combinatorics.

Second, a range proof is a $\Sigma$-protocol that allows a prover to convince a verifier that a digitally committed value lies in a specified integer interval $I$. Given the sumset-representation of $I$, we show how to decrease the communication complexity of the recent range proof of Camenisch, Chaabouni and Shelat from ASIACRYPT 2008 by the factor of $2$. (Joint work with Rafik Chaabouni, Abhi Shelat).

Slides of the talk. [pdf]

*Abstract:* In cryptography, one-way functions and trapdoor
functions are the basic primitives for constructing private-key and
public-key cryptosystems, respectively. Unfortunately, it is not yet
proved that there exists a one-way (or trapdoor) function (not
breakable by any polynomial-time adversary).

However, it is possible to prove the existence of "feebly" secure one-way and trapdoor functions where adversary is guaranteed to spend more time (in terms of circuit complexity) than the honest parties by a constant factor (Hiltgen, ASIACRYPT '92; Hirsch and Nikolenko, CSR 2009). In this talk I review old and present new improved constructions of feebly secure cryptographic primitives both in the worst-case and in the average-case setting.

Slides of the talk. [pdf]

*Abstract:* In search for a foundational framework for
reasoning about observable behavior of programs that may not
terminate, we have previously designed a trace-based coinductive
big-step semantics for While, accounting for both terminating and
nonterminating program runs. In this talk I present a Hoare logic
counterpart of our coinductive trace-based semantics, which is proved
sound and complete. Our logic generalizes both the partial
correctness Hoare logic and the total correctness Hoare logic:
derivations in these logics can be meaningfully transformed into
derivations in our logic. However expressivity of our logic goes
beyond that of the partial and the total correctness Hoare logics. I
demonstrate this point by a search algorithm example, inspired by
Markov's principle. Our logic can constructively prove the algorithm
is not nonterminating. (Joint work with Tarmo Uustalu.)

Slides of the talk. [pdf]

*Abstract:* Attack trees are a method of analyzing security
threats by decomposing them into sub-threats. We consider a
two-parameter financial threat model where an adversary can perform
the sub-attacks one after the other, always knowing what happened on
the previous sub-attacks. It turns out that under some restrictions on
the order of attacks this model can in fact be computed in linear time
and that even after many sensible generalizations the model still
remains polynomial-time computable. This presents a substantial step
forward in the state of the art as the best previously known model
required exponential time. (Joint work with Aivo Jürgenson and Jan
Willemson.)

Slides of the talk. [pdf]

*Abstract:* We consider the Boolean circuit satisfiability
problem in full binary basis (CIRCUIT SAT).

Similarly to the SAT problem, no approaches are known for proving
upper bounds in form of *c ^{n}* (

We introduce a recursive algorithm, that runs in time
*O(2 ^{0.4058m})*.

The algorithm has very much in common with typical splitting algorithms for SAT and also uses the xor-chains technique earlier applied to prove lower bounds on the circuit complexity of certain Boolean functions.

Slides of the talk. [pdf]

*Abstract:* In multi-party computation (MPC) the task is to
compute a function, or, more generally, evaluate a reactive
functionality, among a number of parties, each giving input or
receiving output. An MPC is secure if it computes the correct result
(correctness), no party learns anything but the result (privacy), and
it terminates (robustness), even if parties are corrupted and
maliciously deviate from their prescribed program or protocol.

We present approaches to tolerating a majority of corrupted participants in secure MPC. As shown by Cleve (STOC '86) fully secure general MPC is not attainable if more than half of the participants are corrupted. However, this result does not preclude every function from being computable with full security, nor does it preclude functions from being computable with weaker security. Thus, we explore which classes of functions are actually computable with full information-theoretic (IT) security, while tolerating arbitrarily many corrupted parties. Furthermore, we examine weaker notions than full IT security. For instance, we discuss long-term security without robustness, where we admit computational assumptions for the duration of a computation, but require IT privacy once the computation is concluded.

*Abstract:* Several parties care about scientific publishing:
researchers, publishers and funders. But their motives are wildly
different. Over the last 15 years or so, scientific publishing and the
world around it have rapidly undergone some very significant changes
and these have amplified the intrinsic conflict to a state of
unprecedented controversy. I will review some of the issues and would
then like to hear a hot debate on matters like meaningfulness of
citation indexes and bibliometrics, who protects who from what in
rights protection, what has caused the mushrooming of fake publication
venues, who should pay for the costs of publishing, and the ethics of
the enterprise.

Slides of the talk. [pdf]

*Abstract:* Everybody loves Race Detection! I will discuss the
techniques we have devised to detect races in operating system code,
placing this work in the wider context of race detection techniques
for dynamically allocated memory. Our methods are based on various
pointer analyses which we have used successfully in isolation, but our
ultimate goal is to exploit the synergy among these analyses and
integrate them all into a coherent race detection tool, the Goblint
1.0! (Joint work with Kalmer Apinis, Helmut Seidl, and Varmo Vene.)

Slides of the talk. [pdf]

*Abstract:* This talk covers the first linear hull and a
revisit of the algebraic cryptanalysis of reduced-round variants of
the block cipher PRESENT, under known-plaintext and ciphertext-only
settings. We introduce a pure algebraic cryptanalysis of 5-round
PRESENT and in one of our attacks we recover half of the bits of the
key in less than three minutes using an ordinary desktop PC. PRESENT
is a design by Bogdanov et al. presented in CHES 2007 and aimed at
RFID tags and sensor networks. Our linear attacks reach up to 26-round
PRESENT and improve on previously reported attacks in terms time, data
or memory complexities. Additionally, this talk includes linear hulls
computed in practice for the original PRESENT cipher, which
corroborated and even improved on the predicted bias (and the
corresponding attack complexities) of conventional linear relations
based on a single linear trail. (Joint work with Jorge Nakahara Jr.,
Pouyan Sepehrdad, Meiqin Wang.)

Peeter Laud

Helger Lipmaa

Tarmo Uustalu

Varmo Vene

Viimane uuendus 23.10.2009