|
Title: Paper and Coq Code: Formal Idealizations of Cryptographic Hashing Post by: Bill White on January 18, 2015, 08:53:08 PM I've recently been formalizing some cryptocurrency concepts in the proof assistant Coq.
Edit (June 26 2015): The git repo is now available at qeditas.org: Code: git clone git://qeditas.org/qeditas.git I decided to post this in Altcoin Discussion for two reasons: 1. This is the first step in a process that could lead to formally specifying cryptocurrency concepts and formally proving related algorithms correct. It seems doubtful that such a project will be done for bitcoin, but it could lead to a way of creating very secure altcoins. 2. I am hoping there will be discussion that may help me as I continue this project. This first step is only about how to represent and reason about cryptographic hashing in an idealized way. In particular, we often informally argue about hashing functions as if they are injective. In other words, if the hash of m and the hash of n are the same, then m must be the same as n. Mathematically this assumption is in conflict with the pigeon hole principle since 2^256 (for example) is finite. In the paper I describe how one can represent hash values using an infinite type while at the same time wrapping it in an abstraction (a module type in Coq) that prevents the user from analyzing the hash value. The next step I'm working on involves representing cryptographic assets, transactions and ledgers in Coq. |