Towards a Choreography for the Protocol Jungle

A challenge for the security of large standards like Open Identity Federation lies in their support for a jungle of options, and some unforeseen combination of these options can bear a vulnerability that is hard to spot. Formal verification can help, but only if all options are actually part of the formal model. We argue that it is hard to make a comprehensive model in medium- to low-level languages like process calculi and multi-set rewriting, and the higher-level Alice-and-Bob style languages lack the expressivity. We use the new cryptographic choreography language and tool CryptoChoreo to demonstrate an alternative approach with two case studies. The first represents an authorisation scenario with an identity provider where we use non-determinism and long-term memory to better represent the non-linear structure of such systems. The second studies a privacy-friendly escrow mechanism where we highlight the difference between a server API and its use in a protocol. Both are translated by CryptoChoreo to applied π-calculus and verified with ProVerif. These case studies show how to address some of the challenges in modeling and verifying complex identity systems by using a high-level language that allows for a bit of overview in the jungle.