game based (cryptographic) proofs

Stream: lean4

[Karolin Varner]

Is anybody working on creating a framework to formalize game based proofs in cryptography with?

[Mac Malone]

Do you mean a version of the Natural Number Game for cryptography?

[Jon Eugster]

I googled "game-based proof" and although I can't quite find a good definition, it seems to be a term in crypto modelling a hacker as a probabilistic function trying to solve a "game".

I think you get better answers when you help out with more details about the sorts of definitions and statements you are looking for (e.g. a reference to a definition). There is certainly a lot of maths in mathlib that might help.

There is also a docs#SetTheory.Game in mathlib, but I don't have the impression that's related.

[Matthew Ballard]

Possible: Is this being referenced?

[Matthew Ballard]

I just need to write a proposal for an Apple Vision Pro interface into Lean :)

[Adam Topaz]

have we learned nothing from https://en.wikipedia.org/wiki/The_Zero_Theorem ?

[Karolin Varner]

I was sitting at a conference on cryptography with the right experts including lean experts and none of us knew. Game based proofs are what @Jon Eugster explained its a term fammilliar to cryptographers, but little known outside.

It was a long shot to ask on this channel. Thank you for trying to answer, sorry for no tincluding more context wehn asking in the heat of the moment. Banging out jargon from a very nieche field is very confusing

[Karolin Varner]

https://crypto.stanford.edu/~ananthr/docs/crypto-proofs.pdf

[Karolin Varner]

Here is an intro to the subject, the topic is of limited interest outside cryptograhy though

[Henrik Böving]

Is that a WIP document or is 2.2-4.2 just not going to be filled?

[Mac Malone]

No worries, the term "game" is very overloaded term in ths space. :laughing: Just in the esponses above we have both a game-theory based notion of cryptographic proofs (by you and Jon) along with NNG-like gamification of formal verificaiton: (by Matthew).

[Karolin Varner]

Henrik Böving said:

Is that a WIP document or is 2.2-4.2 just not going to be filled?

Blasted PDF, why would it deceive me; I was on the go and just read the first few paragraphs and they seemed to have the right concepts down.

Have some proper references then:

• Proof by sequences of games, Victor Shoup – https://eprint.iacr.org/2004/332
• Bellare and Rogaway on game based proofs (those two wrote an astounding amount of fairly foundational papers in cryptography) – https://eprint.iacr.org/2004/331
• Novak formalizing some game based proofs in Coq – https://eprint.iacr.org/2007/199

[Horațiu Cheval]

Is this https://github.com/JoeyLupo/cryptolib what you are looking for? (it's Lean 3)

[Horațiu Cheval]

@Joey Lupo is the author

[Karolin Varner]

Horațiu Cheval said:

Is this https://github.com/JoeyLupo/cryptolib what you are looking for? (it's Lean 3)

That is a very cool finding. Thank you!