Some weeks ago I found an interesting bug in Chrome and spent the weekend trying to come up with a clever exploit. In the talk, I will explain the details of this exploit.

In this talk I will show you how to use standard playing cards in order to run cryptographic protocols in a visual and easy way. We will focus on the problem of "Multi-party computation", which I introduce with the following question: How can two millionaires learn who is richer without revealing the actual amount of money they have? The talk will be interactive and accessible to everyone. You will learn how to run the protocols and play with cards during the talk. I hope you will improve your knowledge and interest in Cryptography. References: Report 2017/423 and Report 2017/863.

Software verification comes in two flavors: static and dynamic. Static program verification takes place during program analysis and/or compilation, and it aims to prove the correctness of the program w.r.t. some criteria. Dynamic one takes place at run time and it's purpose is to detect undesirable program behaviors. Nowadays these two tasks are typically addresses by systems that offer programmers a combination of language-level constructs (procedure-level annotations such as assertions/contracts, gradual types, etc.) and associated tools (such as static code analyzers and run-time verification frameworks). However, it is often the case that these constructs and tools are not used to their full extent in practice due to a number of limitations such as excessive run-time overhead and/or limited expressiveness. This issue is especially prominent in the context of dynamic languages without an underlying strong type system, such as Prolog. In this talk several practical solutions for minimizing the run-time overhead associated with assertion-based verification while keeping the correctness guarantees provided by run-time checks will be discussed. Additionally, a proposal of extending the expressiveness of first-order specifications to higher-order software specifications will be described. The solutions will be presented in the context of the Ciao system (developed here at IMDEA Software), where a combination of an abstract interpretation-based static analyzer and run-time verification framework is available, although our proposals can be straightforwardly adapted to any other similar system.

For type checking of functional programming languages, it is fundamental to be able to check equality of types, or in other words, to check whether two types are convertible. This becomes more tricky for dependently-typed languages, since equality of types depends on equality of terms. An important aspect is that this conversion checking algorithm is correct. Since a type theory can be seen as a programming language, a question is whether these aspects about type theory can be proven inside type theory. In this talk I will present a proof of correctness for a practical conversion checking algorithm for a dependent type theory with one universe à la Russell, natural numbers, and η-equality for Π types. This proof uses a logical relation parameterized by equivalence relations for types and terms. The logical relation is then instantiated twice, once to prove canonicity and injectivity of type formers, and once again to prove completeness of the algorithm. The proof uses inductive-recursive definitions and has been formalized in the proof assistant Agda.

Attribute-based credentials are a privacy-enhancing technology that allow users to prove things about themselves in a privacy-friendly manner: they allow a user to only reveal the minimal amount of information necessary. To make these credentials easy to use, we recently proposed to place them in a smart phone application. But, what if such a smart-phone is lost or hacked? All of a sudden an attacker may be able to use these credentials to impersonate the user. Threshold cryptography is often touted as a mechanism to protect keys by sharing the key among different parties. It seems then that threshold cryptography is an excellent candidate to secure the keys of sensitive attribute-based credentials. The challenge, however, is finding trusted parties to distribute keys to. Not everyone has a second device readily available. A central server seems a convenient highly-available second party, however, as I’ll show this talk, the use of a central server is often subject to timing attacks, undermining the user's privacy. In the second part of my talk I’ll sketch a solution that makes using threshold cryptographic variants of attribute-based credentials with a phone and a central server privacy-friendly. This new approach protects the privacy of the user against malicious central servers, even if they collude with service providers. At the same time, this approach retain the benefits of threshold cryptography with a central server: it is possible to block keys, stopping attackers from impersonating users. For non-cryptographers: while this talk does feature a small amount of cryptography, the ideas should be understandable without a lot of experience with cryptography. For the cryptographers: while the ideas presented are simple, proving security and privacy thereof is quite challenging, feel free to ask difficult questions.

s(ASP) is a system which computes stable models of logic programs extended with negation (i.e., a logic program with no negation has a unique minimal model, but logic programs with negation may have multiple incompatible models). Traditional methods, such as Answer Set Programming (ASP) solvers, compute the stable models of a programs from an equivalent ground (variable-free) program, therefore, only programs with a finite grounding are supported. Unlike, the s(ASP) method is goal-directed, therefore, the program does not have to be grounded either before or during the execution, and the range of valid program is extended (e.g., s(ASP) supports the use of list as argument and the domain of the variables does not have to be finite). However, the current prototype of s(ASP), developed by K. Marple et al. at the University of Texas at Dallas (UTD), does not support programs with left-recursion or programs with constraints. During my stay at the UTD, we re-implemented the s(ASP) interpreter using Modular TCLP (a framework that allows the integration of Constraint Solvers with the tabling engine of Ciao). The new implementation is a meta-interpreter for goal-directed ASP, called TCLP(ASP), that also support programs with left-recursion and / or constrains (e.g., CLP(Q), CLP(R) and CLP(FD)).

The Split State Model allows to obtain tamper and leakage resilience against a big class of attackers. In this model the secret material is divided in two halves that the attacker can only manipulate/leak independently. In the first part of the talk I will introduce the model, showing the peculiarities and the limits. Then I will introduce the concepts of Leakage-Resilient Codes (LRC) and Non-Malleable Codes (NMC) in the split-state model. In the second part of the talk I will introduce two new primitives which extend the notions of LRC and NMC and allows to get stronger form of security.

Attribute-based encryption (ABE) is a cryptographic primitive which supports fine-grained access control on encrypted data, making it an appealing building block for many applications. In this pa- per, we propose, implement, and evaluate fully automated methods for proving security of ABE in the Generic Bilinear Group Model (Boneh, Boyen, and Goh, 2005, Boyen, 2008), an idealized model which admits simpler and more efficient constructions, and can also be used to find attacks. Our method is applicable to Rational- Fraction Induced ABE, a large class of ABE that contains most of the schemes from the literature, and relies on a Master Theorem, which reduces security in the GGM to a (new) notion of symbolic security, which is amenable to automated verification using constraint-based techniques. We relate our notion of symbolic security for Rational- Fraction Induced ABE to prior notions for Pair Encodings. Finally, we present several applications, including automated proofs for new schemes.

Procedure specifications are useful in many software development tasks. As one example, in automatic test case generation they can guide testing, act as test oracles able to reveal bugs, and identify illegal inputs. Whereas formal specifications are seldom available in practice, it is standard practice for developers to document their code with semi-structured comments such as Doxygen, Javadoc, RDoc, and Sphinx. These comments express the procedure specification with a mix of predefined tags and natural language. In this talk I will present present Toradocu, an approach that combines natural language parsing, pattern matching, and semantic similarity to translate Javadoc comments into executable procedure specifications written as Java expressions. The tool achieves better accuracy than the other similar tools in the state of the art. Moreover, it is the only one with an actual semantic awareness, through which it can translate even complex comments.