A diagrammatic approach to information flow in encrypted communication (extended version)
This work provides a formal framework for cryptographers and security analysts to reason about information leakage and protocol security in encrypted systems, though it appears incremental as it builds on existing categorical methods.
The paper tackles the problem of analyzing information flow in encrypted communication by introducing diagrammatic tools based on categorical diagrams to model mathematics, epistemic knowledge, and communication, enabling deduction of information flow paths and analysis of protocol changes, with demonstrations using Diffie-Hellman key exchange and other cryptographic protocols.
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.