(Avoiding) Boilerplate reduction proofs in cryptography - can we learn from F*-based techniques?

Add to your list(s) Download to your calendar using vCal

• Chris Brzuska (Hamburg)
• Thursday 22 June 2017, 11:00-12:00
• Computer Science, The Sloman Lounge (UG).

If you have a question about this talk, please contact Dr Garfield Benjamin.

Real-life protocols combine cryptographic primitives in a multitude of ways whose “local” analysis (a.k.a. ``game hop’‘) is conceptually straightforward. This leads to the unfortunate case that protocol analysis papers often contain 30 or more pages of reductions. Most of the game hops and reductions are conceptually trivial, but need to handle the simulation of a huge, complex protocol. Therefore, we often make the infeasible attempt to argue about the soundness of a complex simulation that we cannot fully grasp in a single thought, because we need to simulate 5 or 10 stateful oracles simultaneously.

Firstly, the complexity of real-life protocols makes simulation arguments fairly vague and makes it hard to catch subtleties, i.e., cases, where the reduction appears straightforward, but is actually not. Most of us who produce hand-written proofs of real-life protocols make the painful experience of revisiting our paper proofs again and again in order to discover subtle conceptual issues and formal gaps that we overlooked before. Sometimes, we learn about those issues and gaps only through a colleague or a reviewer.

Secondly, it is also difficult to convey the conceptually interesting insights to the reader. As the reader is less intimately familiar with the protocol and the proof, the writer needs to guide the reader through the ``intuitive’’ part of the simulation and also needs to communicate the conceptually interesting insights to the reader. Unfortunately, there is no ``good’’ point in the paper to discuss the interesting insights, because seemingly, understanding the insights requires to comprehend the complex simulations before. The writer is left with (a) the choice to hide the conceptually interesting insights in the bulk of the boring, conceptually trivial, long and vague simulation steps of the proof or (b) the choice to emphasize what is interesting and new at the price of overwhelming the reader.

In fact, even as the authors of our own papers, we have difficulties phrasing our conceptual insights in a crisp clear way that is easy to understand for ourselves (let alone someone else). When we forget our insights, we often need hours and several people to recover our original insight. Our failure to communicate with our future selves is actually related to a third issue: Wasting time, space and attention on local trivialities distracts readers and writers alike from focusing on the big picture, i.e., the protocol that we actually aim to analyze as well as its overall security (definition).

Computer-automatization of proofs in a formal language is only a partial solution: It makes proofs precise, even formal, and it provides many of the code-writers with insights, but it doesn’t provide the human reader with insights – the code-writers can communicate their insights to the readers, but this requires a different language, and indeed, previous papers on miTLS have employed a different language to communicate their insights. It turns out that the different language is not merely a means of communication. Actually, the language can be made precise in order to “import” techniques from miTLS in the world of hand-written reductions. We present and refine the language as well as the state of our ongoing effort to transport techniques from F*-based verification into hand-written cryptographic proofs. In the talk, we will see some very useful trivialities that reduce the efforts in hand-written proofs and put the focus on interesting proof steps.”

This talk is part of the Computer Security Seminars series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, The Sloman Lounge (UG)
• Computer Security Seminars
• computer sience

Note that ex-directory lists are not shown.