Is lean4 a proof assistant

Stream: lean4

[Damien Carré]

Hello.

I made a theorem demontration for the purpose of my blog at: https://gogo2464.github.io/gogo-s-blog-cpe/from-0-to-crypto-by-projects/episode-2-proof-demonstration/

I want to ensure my theorem is correct Nobody wants to read it. Does lean4 answers to my needs please? I never ever used any proof assistant. I do not know if a proof assistant solves my issue actually.

[suhr]

Is lean4 a proof assistant

Yes, famously so.

I want to ensure my theorem is correct Nobody wants to read it. Does lean4 answers to my needs please?

Now that depends on your needs. Formalizing a proof in Lean is a good way to check if it's correct, but that does not immediately mean that people would like to read your work. The later also requires your work to be readable and interesting.

[Damien Carré]

Maybe I should use coq or Isabelle

[suhr]

You can, but the situation will be the same. Except in Lean you have Mathlib, which is a very good library of formalized mathematics.

Lean is also easier to learn: it has better tooling, better tutorials and more active community.

[Alex Meiburg]

Glancing at your blog post - If your central claim is "I have an efficient algorithm to break a cryptographic hash", then there are three main things to be aware of:

• (1) You should implement your algorithm. If you have a program (say, in Python or C) that can reverse the hash, that's already an excellent "proof". Find a string that gives the hash 0x123456789: this would be hard in general, so if you find such a string (like, "look! the string '29uojvinsdjkfgn1ar' gives that hash of 0x12356789") then that's good evidence you do in fact have such an algorithm.
• (2) Breaking cryptographic hashes is, in general, very hard. Or at least, it should be. Some hashes are not designed to be cryptographically secure (they're just fast and pseudorandom).
• (3) If the hash is supposed to be hard to break, then people will be skeptical of your claim; but because of (1), you can very easily given a simple proof; so if you don't do (1) and give people a clear example, they just won't believe you.

I don't now what the Cisco Vigenere hash is. If it's supposed to be cryptographically secure, you should start by trying to write an actual cracking program of your idea. If it's not supposed to be cryptographically secure, it might simply be that people aren't surprised or interested to hear that you broke it.

Anyway, the point: start by writing an implementation and getting a proof of concept! That's the best proof you'll get for sure!

[Damien Carré]

@Alex Meiburg

I have already reversed the hash in C++. cisco hash is a PROPRIETARY algorithm.

It has already broken. The break has been tested over 5 times on my github unit testing: https://gogo2464.github.io/gogo-s-blog-cpe/from-0-to-buffer-overflow-by-projects/episode-2-guessing-source-code-reverse-engineering-program/

[Alex Meiburg]

I see, ok! Well, it sounds like you reverse engineered it, found it was a fairly simple hash to invert, and broke it. Not knowing anything about Packet Tracer, it's hard to quickly see what the impact of this is. What is this hash used for? What are the security consequences of inverting it?

[Alex Meiburg]

You call it "Vigenere Cisco", but that doesn't seem to be a standard name. If you think this was an interesting fun project in reverse engineering, then I would call it a day and be satisfied. If you think this is a meaningful flaw in some Cisco software, then you should alert people; filing a report on some bug tracker would be appropriate.

I don't think anyone will reasonably question the fact that the hash is broken - it sounds clear - a mathematical proof won't get you anything extra. I would write something like this in a CVE report:

The hashing algorithm used in Cisco's Packet Tracer software for xxxxx seems to be a weak, handrolled hashing function that's trivial to invert. This means that xxxxxx is less secure. It is possible that the same hashing algorithm would be used in related Cisco products like xxxxxxxx. I think Cisco should switch to a secure hasing algorithm such as SHA256 and update this in the next version of Packet Tracker.

[Damien Carré]

Yes i did :). the impact is low. If i have remote access to a router i coild read passwords hashed in type7. It is all.

[Damien Carré]

It is the name according to cisco doc.

The hash is disrecommended since 50 yo then it sounds ok.

If you want to find 0days, you can search for proprietary algos. Sounds impossible as nobodu redo custom algos but actually some do it in cryptocurrencies!!

[Damien Carré]

for your information, custom crypto come back more often than I thank https://github.com/mit-dci/tangled-curl/blob/master/vuln-iota.md#2-disclosure-timeline

[Damien Carré]

do you want to look for custom crypto?