2022.08.29 03:21:52 (1564060733129629696) from Daniel J. Bernstein, replying to "John Carlos Baez (@johncarlosbaez)" (1564058929046306816):
Define T = cost(brute-force search for all AES-128 keys). There are finitely many algorithms A with cost(A) <= T; cost includes len(A). Compute exact success probability of each A by running A on all sequences of coin flips of length fitting into cost T. Reflect into a proof. QED
2022.08.27 17:04:26 (1563542963044503555) from "John Carlos Baez (@johncarlosbaez)", replying to "John Carlos Baez (@johncarlosbaez)" (1563542394116616192):
There's an imaginable third alternative: we can imagine that cryptographers would prove that an encrypted text would take at least X amount of computational resources to decrypt. This seems more reasonable than demanding unconditional security, but... (4/n)
2022.08.27 17:08:00 (1563543861607010305) from "John Carlos Baez (@johncarlosbaez)", replying to "John Carlos Baez (@johncarlosbaez)" (1563542963044503555):
... as far as I know, this is never done for widely-used systems, because nobody knows how to prove things like this. (They might be unprovable in principle, but nobody knows that either.) Anyway, I would change the passage in question to something like this: (5/n)
2022.08.29 03:09:53 (1564057719434162176) from Daniel J. Bernstein, replying to "John Carlos Baez (@johncarlosbaez)" (1563543861607010305):
Your parenthetical sentence here is false. For example, there exists a proof of the minimal cost of an AES-128 attack, with standard formalizations of "cost"+"attack"+"proof". We don't know if there's a proof of length <2^L for any useful value of L; that's a different question.
2022.08.29 03:14:42 (1564058929046306816) from "John Carlos Baez (@johncarlosbaez)":
My parenthetical was trying to say say nobody has yet proved the *unprovability* of lower bounds on the difficulty of cracking certain ciphers. I think that's true. But outside the parentheses, I was asking for results like the one you just mentioned. Could I see a reference?