A diagrammatic approach to information flow in encrypted communication (extended version)

TL;DR

This paper introduces a diagrammatic, categorical framework to analyze and verify information flow in encrypted communication protocols, enabling detailed reasoning about knowledge transfer and protocol variations.

Contribution

It presents a novel diagrammatic method using category theory to model and analyze information flow and protocol correctness in encrypted communications.

Findings

Able to model various cryptographic protocols including Diffie-Hellman

Can analyze the impact of protocol modifications on information flow

Provides a formal correctness criterion for communication analysis

Abstract

We give diagrammatic tools to reason about information flow within encrypted communication. In particular, we are interested in deducing where information flow (communication or otherwise) has taken place, and fully accounting for all possible paths. The core mathematical concept is using a single categorical diagram to model the underlying mathematics, the epistemic knowledge of the participants, and (implicitly) the potential or actual communication between participants. A key part of this is a `correctness' or `consistency' criterion that ensures we accurately & fully account for the distinct routes by which information may come to be known (i.e. communication and / or calculation). We demonstrate how this formalism may be applied to answer questions about communication scenarios where we have the partial information about the participants and their interactions. Similarly, we show how to analyse the consequences of changes to protocols or communications, and to enumerate the distinct orders in which events may have occurred. We use various forms of Diffie-Hellman key exchange as an illustration of these techniques. However, they are entirely general; we illustrate in an appendix how other protocols from non-commutative cryptography may be analysed in the same manner.