If you suspend your transcription on amara.org, please add a timestamp below to indicate how far you progressed! This will help others to resume your work!
Please do not press “publish” on amara.org to save your progress, use “save draft” instead. Only press “publish” when you're done with quality control.
<p>Using the recent <a href="https://en.wikipedia.org/wiki/BREACH_%28security_exploit%29">BREACH</a> exploit as an example, I will present how to represent attacks and security notions within the Type Theory of <a href="http://wiki.portal.chalmers.se/agda/">Agda</a>.</p>
<p>Using security notions such as semantic security (<code>IND-CPA</code>, <code>IND-CCA</code>), it is intuitive to show how the use of compression leads to a not semantically secure encryption, and thus potential issues. Indeed the length of the ciphertext can now be controlled by the adversary who can control the plaintext. I will show how this intuitive result can be formalized using <a href="http://wiki.portal.chalmers.se/agda/">Agda</a>.</p>
<p>A note on <a href="http://wiki.portal.chalmers.se/agda/">Agda</a>: It is both a programming language and a proof system. The programming language features pure, exhaustive, and terminating functions over rich user defined data types (inductive and co-inductive). This powerful λ-calculus is equipped with a rich type-system featuring dependent-types. Through the Curry-Howard correspondence this programming language can also be used as a proof system. With such a combined system it becomes possible to write programs and proofs about these programs in a unified way. Additionally using this approach, one can start proving properties starting only with programming skills and gradually learn more proof techniques by exploring the type system.</p>
<p>I claim that functional programming and dependent types can be of a great help to formalize cryptography and thus privacy enhancing tools. I will present how functions are convenient at describing these games and adversaries. I will also give an overview of the crypto-agda project: how type-isomorphisms can ease probabilistic reasoning; how circuits can help capturing the requirements on the complexity bounds; and how all of these aspects can fit together thanks to polymorphism!</p>