Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adding a specification of hashes to the examples #1140

Merged
merged 4 commits into from
Sep 4, 2023
Merged

Adding a specification of hashes to the examples #1140

merged 4 commits into from
Sep 4, 2023

Conversation

konnov
Copy link
Contributor

@konnov konnov commented Sep 4, 2023

I have been thinking about a nice way of specifying hashes in Quint. One reason for not merging #975 yet is that I barely understand hashes in that spec myself. The best way would be introduce uninterpreted terms for hashing, e.g., h(text), h(h(text)). However, we do not allow for recursive types. Hence, I had to apply a trick: Wraps a list of bytes with a marker -1, which gets decreased whenever additional hashes are applied.

  • Tests added for any new code

@konnov konnov requested review from thpani and Kukovec September 4, 2023 09:43
@konnov konnov self-assigned this Sep 4, 2023
@konnov konnov added the example Language and specification examples label Sep 4, 2023
Copy link
Contributor

@Kukovec Kukovec left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, sugestions are purely for compactness

examples/cryptography/hashes.qnt Outdated Show resolved Hide resolved
examples/cryptography/hashes.qnt Outdated Show resolved Hide resolved
@konnov konnov merged commit 1c06f8a into main Sep 4, 2023
@konnov konnov deleted the igor/hashes branch September 4, 2023 13:47
@thpani thpani mentioned this pull request Sep 5, 2023
@amiller
Copy link

amiller commented Sep 8, 2023

I'm curious if the fact that it's not feasible to find two colliding hashes is expressed / exported as a property somehow? I see how incrementing the hashes by 1 as a concrete representation exhibits this, but not how it could be exposed in general as a property

@konnov
Copy link
Contributor Author

konnov commented Sep 8, 2023

I'm curious if the fact that it's not feasible to find two colliding hashes is expressed / exported as a property somehow? I see how incrementing the hashes by 1 as a concrete representation exhibits this, but not how it could be exposed in general as a property

This is an excellent question. I have been thinking about the same but have not come up with a good solution yet. If we were using an interactive theorem prover or a model checker that admits quantification over unbounded domains and supports recursive data types, that would be the way to go. For instance, we could write the following assumption:

// in Quint
assume(tuples(D, D).forall((x, y) => x == y iff hash(x) == hash(y)))
// in TLA+
ASSUME(\A x, y \in D: x = y <=> hash(x) = hash(y))

I can see how we could enforce this property in Apalache even though we use a quantifier-free fragment of SMT. It is less obvious to me, how we would do that in the random simulator. However, we could interpret hash symbolically in the simulator and avoid any computation at all.

If you have an example of a system where it was done right already, I would be very curious to see it. Now that I am thinking about it, maybe we should have a look at ACL2 or something similar.

@amiller
Copy link

amiller commented Sep 8, 2023

My experience is mainly with an early version of this production of Merkle Trees in F*. An early version defined a lemma injective_hash. But, when combined with an assumption that hashes have some fixed length, it seems vulnerable to disproving it by pigeonhole principle. (Not sure how this would matter for quint)
The current version avoids defining the assumption of collision resistance, instead just leaves it to the Merkle Tree application to show that it can produce a collision.
https://www.fstar-lang.org/tutorial/book/part2/part2_merkle.html

In EasyCrypt they actually define collisions as a game, they have some probability model to work with tho
https://github.com/EasyCrypt/easycrypt/blob/main/theories/crypto/assumptions/CRHash.ec

@konnov
Copy link
Contributor Author

konnov commented Sep 8, 2023

My experience is mainly with an early version of this production of Merkle Trees in F*. An early version defined a lemma injective_hash. But, when combined with an assumption that hashes have some fixed length, it seems vulnerable to disproving it by pigeonhole principle. (Not sure how this would matter for quint)
The current version avoids defining the assumption of collision resistance, instead just leaves it to the Merkle Tree application to show that it can produce a collision.

Right. The way they do it in F* is similar to what I would imagine in a proof system. I guess, there should be a way to execute code in F*. Would one have to provide some form of refinement of hash to make it executable? (I don't know much about F*, so this may be a very naive question :) )

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
example Language and specification examples
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants