20 August 2020, 16:00, online

Speaker

Martti Karvonen, University of Ottawa

Title

Towards categorical composable cryptography

Abstract

Modern cryptographic protocols are complicated pieces of software, and their security proofs are often no simpler than the protocols themselves. Given this complexity, it would be highly desirable to be able to design them and reason about them compositionally. However, traditional security definitions are often not composable. As a case in point consider quantum key distribution. Protocols for it were proposed in the 80s/90s, with first security proofs a decade later. However, a decade after that it was realized that the definitions of security were not composable: a protocol might be "secure" in the sense of satisfying the definition but insecure if one wanted to compose it with further protocols - or even use the produced keys. Since the 2000s, a standard way of achieving composable security definitions is by working in a specific framework of interacting machines (such as Canetti's UC-model), and as a result the frameworks are often complicated to reason with and it is not always clear if the results obtained apply more generally for slight variants of the model. Maurer and Renner's abstract cryptography tries to remedy this by working within an "algebraic theory of systems" that they have developed from scratch, but so far their approach hasn't won over the community. In this talk we discuss ongoing work on how to incorporate the key ideas of earlier approaches into a categorical framework that aims to be both general, flexible and still understandable to cryptographers. We formalize the standard real-world/ideal-world paradigm as a close variant of "resource theory of states" coming from a "partitioned process theory" in the sense of Coecke, Fritz and Spekkens. This results in a symmetric monoidal category where our objects are cryptographic resources such as secret keys or secure channels, and morphisms are protocols that securely construct the target resource from the starting resource(s). This allows one to formalize pictures already present in the cryptographic literature as string diagrams, thus making rigorous proofs out of what used to be merely heuristic figures. In particular, we will prove pictorially some (known) no-go results in the two-party setting. Besides explaining all of the above, we will discuss those aspects of our framework that are still under development and not thoroughly understood, such as good sources of starting categories, or the "almost"-enrichment in pseudometric spaces stemming from structures present in such categories.