Score:3

What is an efficient cryptographic hash function in the λ-calculus?

ca flag

Most hash functions are designed to be fast in conventional processors, but there are contexts where machine integers either don't exist, or aren't the most efficient option. For example, zk-snark circuits don't have these, and brainfuck has only increment and decrement. If you needed fast hash functions on these environments, it is unlikely that sha2/keccak/blake would perform better than something designed for them.

I'm particularly looking for a hash function that is designed to be efficient on the pure untyped λ-calculus. Not just pure functional languages, which usually have machine integers, but the actual pure λ-calculus, which has only lambdas and applications. Without native integers, our best bet is to λ-encode the data, thus, the most powerful primitive we have is pattern-matching. The performance of a hash function could thus be measured, or approximated, by the amount of pattern-matches it performs. The question is: what are simple hash functions that performs well on such context?

fgrieu avatar
ng flag
Correct me if I err, but I think we don't know if there exists a (secure) polynomial-time cryptographic function in the usual λ-calculus, much less an efficient such function for any sharper definition of efficient. It would follow we can't prove there is one such function in whatever restriction of λ-calculus. Thus if we can answer this question with certainty, that must be by the negative. For the little I grasp about the restriction, it is so severe that intuitively, there's indeed not anything of crytographic interest that's allowed.
ca flag
@fgrieu there are polynomial-time cryptographic functions in the λ-calculus, though. As a practical example, my programming language [Kind](https://github.com/uwu-tech/kind) has an implementation of Keccak, and it compiles to the λ-calculus. Of course, when targeting the pure λ-calculus, the performance of Keccak is terrible, but it works regardless. Perhaps what I'm asking would be more familiar if I rephrased it as: *"how efficiently, at most, could we implement hash functions, if we could only use Haskell datatypes and case-of (i.e., no native ints)?"* (That's an equivalent question.)
fgrieu avatar
ng flag
I'm referring to: short of assuming P≠NP, we have no proof of existence of a secure cryptographic hash function implementable on a Turing machine (that is a hash family asymptotically undistinguishable from a random function family with non-vanishing probability by any PPT algorithm). In the case of Keccak I don't know a proof even when assuming P≠NP.
ca flag
@fgrieu oh, but I meant one equivalently secure to Keccak, Sha2 and similar. I don't get it though. I know there is no proof these functions are actually secure, but then what is the criteria used? Is it just: "mix enough bits and hope for the best"? Are modern hash functions essentially just algorithms obscured enough for nobody to know how to revert them... yet?
Mark avatar
ng flag
@MaiaVictor typically one evaluates the performance of the construction on known attacks. There are other things one can do as well (say build a hash out of a compression function, and prove that if the compression function is good then the hash is good).
Mark avatar
ng flag
@MaiaVictor can you possibly summarize some "standard" operations that are efficient in the pure untyped lambda-calculus? For example, certain better known operations which have low "pattern matching complexity"
mangohost

Post an answer

Most people don’t grasp that asking a lot of questions unlocks learning and improves interpersonal bonding. In Alison’s studies, for example, though people could accurately recall how many questions had been asked in their conversations, they didn’t intuit the link between questions and liking. Across four studies, in which participants were engaged in conversations themselves or read transcripts of others’ conversations, people tended not to realize that question asking would influence—or had influenced—the level of amity between the conversationalists.