Title: Security and Privacy by Typing in Cryptographic Systems
The security of modern distributed systems is an important and complex challenge, which has attracted the interest
of a growing research community over the last decade. The cryptographic protocols used to securely transmit data
over an untrusted network, and even more so their software implementations, are extraordinarily difficult to design
and to prove secure, as witnessed by the continuously growing list of discovered vulnerabilities. The complexity of
cryptographic systems stem from several factors and has significantly increased over the years. First of all, while
early academic protocols mostly consisted of simple combinations of signature and encryption schemes, modern ones
rely on much more sophisticated, and arguably fascinating, cryptographic primitives, such as zero-knowledge proofs
and secure multiparty computations. Secondly, the security and privacy properties required by modern applications
go well beyond the well-understood secrecy and authenticity properties, covering, e.g., indistinguishability
relations and differential privacy.
Language-based techniques, and type systems in particular, lived up to the challenge, constituting a solid and
expressive framework for the verification and design of cryptographic systems. While early academic cryptographic
protocols required relatively simple type and effect systems, modern cryptography called for more powerful
techniques, such as refinement types, union and intersection types, linear types, and relational refinements.
The goal of this talk is to guide the audience through the literature on type theory for cryptographic
applications, giving a consolidated view of the research development in this field and establishing bridges with
various subdisciplines of interest to the logic, semantics, and verification community (e.g., type theory, SMT
solving, linear logic, proof-carrying authorization, relational verification, and concurrent programming), with the
final goal of fostering cross-fertilizing research ideas.
Title: The Archimedean Property: New Horizons and Perspectives Joint work with Antonio Ledda and Constantine Tsinakis
Although there have been repeated attempts to define the concept of an Archimedean algebra for individual classes of residuated lattices, there is no all-purpose definition that suits the general case. We suggest as a possible candidate the notion of a normal-valued and $e$-cyclic residuated lattice that has the \emph{zero radical compact property} --- namely, a normal-valued and $e$-cyclic residuated lattice in which every principal convex subuniverse has a trivial radical (understood as the intersection of all its maximal convex subuniverses). We characterize the Archimedean members in the variety of $e$-cyclic residuated lattices, as well as in various special cases of interest. A theorem to the effect that each Archimedean and prelinear GBL-algebra is commutative, subsuming as corollaries several analogous results from the recent literature, is grist to the mill of our proposal's adequacy.
Title: A unified view of modal and substructural logics
It is well known that context dependent logical rules can be problematic both to implement and reason about. This is one of the factors driving the quest for better behaved, i.e., local, logical systems. In this work we investigate such a local system for linear logic (LL) based on linear nested sequents (LNS). Relying on that system, we propose a cut-free, general framework for modularly describing systems combining, coherently, substructural behaviors inherited from LL with simply dependent multimodalities. This class of systems includes linear, elementary, affine and subexponential linear logics and extensions of multiplicative additive linear logic (MALL) with normal modalities, as well as general combinations of them. The resulting LNS systems can be adequately encoded into (plain) linear logic, supporting the idea that LL is, in fact, a “universal framework” for the specification of logical systems. From the theoretical point of view, we give a uniform presentation of LL featuring different axioms for its modal operators. From the practical point of view, our results lead to a generic way of constructing theorem provers for different logics, all of them based on the same grounds. This opens the possibility of using the same logical framework for reasoning about all such logical systems.
This is a joint work with Björn Lellmann and Carlos Olarte.
Title: Logic as a modelling technology: resource semantics, systems modelling, and security
The development of BI, the logic of bunched implications, together with
its resource semantics, led to the formulation of Separation Logic, which forms the
basis of the Infer program analyser deployed in Facebook's code production. However, this
rather successful story sits within a broader, quite systematic logical context. I will
review the (family of) logics, including process logics, that are supported by resource
semantics, explaining their more-or-less uniform meta-theoretic basis and illustrating
their uses in a range of modelling applications, including access control, systems
security, and workflow simulation.
Title: A proof theory for dual nominal quantifiers
One approach in relating logic and process calculus is via the formula-as-process interpretation, where process constructors are interpreted by logical connectives. In this talk I will discuss a problem of embedding the pi-calculus in linear logic, and highlight some problems with the interpretation of the restriction operator of the pi-calculus as a quantifier in logic. In particular, I will show that self-dual nominal quantifiers, such as Gabbay and Pitts's new quantifier or Miller and Tiu's nabla quantifier are both unsuitable in this setting. A key requirement seems to be that the nominal quantifier must not distribute over the par connective. This motivated a recent work on the introduction of a dual pair of nominal quantifiers, called `new' and `wen', where the distributivity property of par is absent. The proof rules for the `new' quantifier have a similar flavour to the universal quantifier rules, whereas the `wen' quantifier rules are similar to the existential ones, except that the wen-quantified variable can only be instantiated with a fresh name. I will present a proof system featuring these dual nominal quantifiers, extending the BV proof system for a non-commutative multiplicative linear logic. I will sketch the cut-elimination proof and show how one can interpret pi-processes in logic such that implication gives rise to a process pre-order. I will then discuss some open problems, in particular, in the interaction between the nominal quantifiers and the sequential operator of BV.
This talk is based on a joint work with Ross Horne, Bogdan Aman, and Gabriel Ciobanu.
Continuing a line of work by Abramsky (1994), by Bellin and Scott (1994),
and by Caires and Pfenning (2010), among others, this paper presents CP, a
calculus in which propositions of classical linear logic correspond to
session types. Continuing a line of work by Honda (1993), by Honda, Kubo,
and Vasconcelos (1998), and by Gay and Vasconcelos (2010), among others,
this paper presents GV, a linear functional language with session types, and
presents a translation from GV into CP. The translation formalises for the
first time a connection between a standard presentation of session types and
linear logic, and shows how a modification to the standard presentation
yield a language free from deadlock, where deadlock freedom follows from the
correspondence to linear logic.