feat(Cryptography): formalise perfect secrecy and the one-time pad#464
feat(Cryptography): formalise perfect secrecy and the one-time pad#464fmontesi merged 12 commits intoleanprover:mainfrom
Conversation
Adds `Cslib.Cryptography.PerfectSecrecy` with information-theoretic private-key encryption schemes and perfect secrecy following Katz-Lindell, Chapter 2: - `EncScheme`: private-key encryption (Definition 2.1) - `PerfectlySecret`: perfect secrecy (Definition 2.3) - `perfectlySecret_iff_ciphertextIndist`: ciphertext indistinguishability characterization (Lemma 2.5) - `otp`: the one-time pad construction (Construction 2.9) - `otp_perfectlySecret`: the OTP is perfectly secret (Theorem 2.10) - `perfectlySecret_keySpace_ge`: Shannon's theorem, |K| ≥ |M| (Theorem 2.12)
|
I'd be quite interested in helping with future review in this |
linesthatinterlace
left a comment
linesthatinterlace
left a comment
There was a problem hiding this comment.
In general I think this is a good start on this stuff. My concern right now is about theorem organization and structure (including naming), and about whether any of the results you've proved should be Mathlib results or at least separated out (i.e. they are not really results about cryptographic concepts specifically).
Thanks for the feedback! I'll work on a follow up commit today that addresses each of these concerns. Re: Mathlib results, not totally sure how to approach it, I'll wait for more advice there. |
|
Regarding the directory name, is it open also to cryptology stuff in the future? If so, we could consider calling it simply 'Crypto'. |
Great idea. I was actually considering adding some of the ciphers from the first chapter of the book originally, that could be fun to have around pedagogically. |
Addresses reviewer comments from linesthatinterlace and fmontesi. Definitions and naming: - Define `CiphertextIndist` predicate for ciphertext indistinguishability - Define `posteriorMsgDist : PMF M` proving the posterior is a valid distribution, with `perfectlySecret_iff_posteriorEq` - Rename `backward`/`forward` to `perfectlySecret_of_ciphertextIndist` and `ciphertextIndist_of_perfectlySecret` - Extract `xor_right_eq_iff` and `encrypt_key_injective` as lemmas OTP and types: - Use `BitVec l` instead of `Fin l → Bool` for the one-time pad, with a `Fintype (BitVec n)` instance via `Fin (2^n)` Generalisations: - Weaken Shannon's bound from `[Fintype]` to `[Finite]` with `Nat.card` - Shorten `perfectlySecret_iff_indep` proof Housekeeping: - Add KatzLindell2020 to references.bib (3rd ed., CRC Press, 2020) - Fix citation key from KatzLindell2021 to KatzLindell2020 - Eliminate `PerfectSecrecy/PerfectSecrecy/` double directory - Remove umbrella re-export module (not a pattern used in cslib) - Revert unrelated CI workflow and .gitignore changes
|
I believe all the current feedback should be addressed now, let me know if there are more nits or issues. |
Replace the pointwise posteriorMsgProb definition with posteriorMsgDist (a proper PMF) and redefine PerfectlySecret as equality of distributions. Extract reusable PMF bind/posterior lemmas into PMFUtilities. Golf proofs across all PerfectSecrecy files (~16 lines removed).
| open PMF ENNReal | ||
|
|
||
| universe u | ||
| variable {α β : Type u} |
There was a problem hiding this comment.
Where possible these should be in different universes. You might need to specify them separately per theorem
There was a problem hiding this comment.
Given that these are going to be upstreamed anyways, I'll make this change in those/that PR/s rather than making this one more wordy.
There was a problem hiding this comment.
I think you want to have the most general version here. Upstreaming should not be anything more than a chore. Consider that the upatreaming process is a slow one and people will rely on this definition until upstreaming is complete.
There was a problem hiding this comment.
Reading through mathlib now, I feel like this might already be there in terms of kernels. I wonder if I can get rid of this entirely...
There was a problem hiding this comment.
Ah, no. I'd need to rephrase a lot more.
|
I think everyone's comments have been addressed. Let me know if there is any more feedback. |
|
@linesthatinterlace I made a PR to my fork of Mathlib with the posterior definition and friends here: SamuelSchlesinger/mathlib4#1. Hoping for some pre-review before bothering the mathlib reviewers for the first time :) |
|
LGTM. @linesthatinterlace @eric-wieser can anybody give me a ping of approval? Then I'll merge. |
|
As long as there is a plan to back-port relevant things to Mathlib and improve proof later, I am happy for this to merge. |
|
I have a PR to Mathlib to do so here: leanprover-community/mathlib4#37938. I'm happy to make a followup to Cslib once we have access to these. Let me know what other aspects of these proofs needs to be improved in the meantime. |
|
It got mad at my unicode caution symbols :) I'll delete those and run the lints locally to make sure everything works before I push back up. |
Head branch was pushed to by a user without write access
|
@fmontesi I think you might need to turn back on auto-merge and trigger the ci-checks again. |
|
I've put it back in the queue. |
|
Whoops, concurrent PR management, sorry. Back in the queue. :-) |
7 participants
Adds
Cslib.Cryptography.PerfectSecrecywith information-theoretic private-key encryption schemes and perfect secrecy following Katz-Lindell, Chapter 2:EncScheme: private-key encryption (Definition 2.1)PerfectlySecret: perfect secrecy (Definition 2.3)perfectlySecret_iff_ciphertextIndist: ciphertext indistinguishability characterization (Lemma 2.5)otp: the one-time pad construction (Construction 2.9)otp_perfectlySecret: the OTP is perfectly secret (Theorem 2.10)perfectlySecret_keySpace_ge: Shannon's theorem, |K| ≥ |M| (Theorem 2.12)For some context, Katz reviewed this in its original home: SamuelSchlesinger/introduction-to-modern-cryptography#1.