Programme

We formalize the simulation paradigm of cryptography in terms of category theory and show that protocols secure against abstract attacks form a symmetric monoidal category, thus giving an abstract model of composable security definitions in cryptography. Our model is able to incorporate computational security, set-up assumptions and various attack models such as colluding or independently acting subsets of adversaries in a modular, flexible fashion. We use the one time pad as our main example: in abstract terms, its composable security follows from the axioms of a Hopf algebra with an integral, which concretely speaking corresponds to a group structure on the message space and a uniformly random key. Time permitting, we will also discuss no-theorems concerning composable two- and three-party cryptography.

Joint work with Anne Broadbent, based on https://arxiv.org/abs/2208.13232.

Most security proofs of cryptographic constructions are reductions, where the security of one construction follows from the security of a simpler one. In these proofs we build machines that consume and produce the various resources from the definitions of security, as well as from our constructions. In my talk, I attempt to give an overview, what kinds of resources these proofs speak about, and what kind of compositions there exist.

I will present an ongoing work that aims to define hierarchies of private information of a single party as well as of private correlations among two parties. Both situations are analysed for classical and quantum registers. Our approach uses the framework of resource theories. The free operations for single party are ones that do not use any private information. In the two party case, several choices of free operations are relevant, mimicking the choice between LOCC and LOSR operations in the study of quantum entanglement. We prove basic properties of the resulting resource orderings and conjecture that the privacy ordering of classical correlations bears close analogy to the entanglement ordering of bipartite quantum states.

We introduce a minimalistic logic for message-passing protocols informed by category theory: its derivations form the free polarized normal monoidal symmetric multicategory over a set of objects. There exists an adjunction between symmetric monoidal categories and algebras for these derivations constructing a free message theory over a symmetric monoidal category. We argue this framework is an extension of Nester's free cornering construction, and we discuss a further extension to polycategories via the polycategorical Chu construction.

Adhesive and quasiadhesive categories provide a general framework for the study of algebraic graph rewriting systems. In a quasiadhesive category any two regular subobjects have a join which is again a regular subobject. Vice versa, if regular monos are adhesive, then the existence of a regular join for any pair of regular subobjects entails quasiadhesivity. It is also known (quasi)adhesive categories can be embedded in a Grothendieck topos via a functor preserving pullbacks and pushouts along (regular) monomorphisms.

In this talk we will show how to extend these results to M, N-adhesive categories, a concept recently introduced to generalize the notion of (quasi)adhesivity. The new notion of N-adhesive morphism, moreover, allows us to express M, N-adhesivity as a condition on the subobjects’s posets. This concept wll also provide us with a way to embed an M, N -adhesive category into a Grothendieck topos, preserving pullbacks and M, N -pushouts

Lax monoidal categories naturally arise in the study of (colored) operads (see [1], [2]). In my talk I will present a concrete description of a colimit process that turns an unbiased (co)lax monoidal category A to a strict one, denoted A′ . For instance, applying this process to the terminal monoidal category produces the strict monoidal category ∆ of finite ordinals and order-preserving maps. I will also describe a canonical adjunction that arises between A and A′ , with an important special case being the fact that every normal lax monoidal category can be coreflectively embedded to its strictification. Finally, I will pay attention to how multicategories (colored operads) appear in these constructions.

All these constructions are a part of a bigger picture of 2-category theory I have focused on during my Ph.D. studies.

Cryptographic protocols make use of a variety of computational effects which can be described algebraically. These include probability for randomization, global state for storing keys, input/output for communication, and nondeterminism for describing adversarial parties. In this talk, we explore how to model such algebraic effects from both the perspective of the caller (participant) and the resolver (environment), as respectively done by monads and comonads. We will look at how this may apply to examples of cryptographic protocols and security definitions. This talk is based on previous work, though the connection to cryptography is work in progress.

In this talk, I will present an abstract categorical setting that can be used to reason about cryptographic protocols based on the Kleisli construction for graded monads. Instantiating it with the right base category and graded monad, the morphisms out of the unit object can be viewed as protocols in a typed version of the (simple) UC framework. The universal composition operation then becomes regular composition, and the universal composition theorem follows from basic categorical reasoning.

Effectful streams are a coinductive semantic universe for effectful dataflow programming and traces. As an example, we formalise the stream cipher cryptographic protocol. In monoidal categories with conditionals and ranges, effectful streams particularize to families of morphisms satisfying a causality condition. Effectful streams allow us to develop notions of trace and bisimulation for effectful Mealy machines; bisimulation implies effectful trace equivalence. This is recent joint work with Filippo Bonchi and Mario Román.

We will recall the notions of skew monoidal category and algebraic weak factorisation system and explore some common features and analogies between them.