Clarification of Skepticism

Wed Mar 3 01:48:11 EST 2021

Harvey Friedman wrote:

> As you can see from earlier postings, I got interested in where the
> intellectual JUMPS become inaccessible to proof assistants. So I went
> into toy situations where the challenges are in a comparatively pure
> form.

Despite being a passionate contributor to the formalization of mathematics
using proof assistants, e.g.,

- My formalization of "Banach-Steinhaus Theorem" (collaboration with Prof.
Unruh): https://www.isa-afp.org/entries/Banach_Steinhaus.html

- My formalization of Problem “ARITHMETIC PROGRESSIONS” from the Putnam
exam problems of 2002:
https://www.isa-afp.org/entries/Arith_Prog_Rel_Primes.html

I want to mention a field where JUMP may become inaccessible to proof
assistants. This field is the intersection between cryptography and complex
systems. In other words, the study of cryptographic protocols composed of
many parts, where the security of the protocol cannot be reduced to its
parts' security.

It is still an open problem whether one-way functions exist? These are
functions that are easy to evaluate but hard to invert, in a precise
complexity-theoretic sense:

https://www.wikiwand.com/en/One-way_function

For the sake of argument, assume that this problem is solved positively,
the proof is formalized in a proof assistant, and all the cryptographic
protocol incorporate a genuine one-way function (right now, there are only
conjectures about candidates for one-way functions). According to the
cryptographers N. Koblitz and A. Menezes,

Throughout the history of public-key cryptography, almost all of the
> effective attacks on the most popular systems have succeeded not by
> inverting the one- way function], but rather by finding a weakness in the
> protocol.

 Koblitz, Neal, and Alfred J. Menezes. "Another look at ‘provable
security."’Journal of Cryptology 20.1 (2007): 3-37.
https://eprint.iacr.org/2004/152.pdf

The important observation is that we do not know how, generically, the
length of the shortest security proof of a cryptographic protocol grows as
a function of the number of components. It may be the case that to find the
security proof of a given protocol requires the same computational effort
as to break the protocol by a brute force attack. This situation is similar
to verifying the so-called quantum supremacy: how to prove that a quantum
computer is superior to any classical computer if our only resource is
classical computers? In this last case, these difficulties are addressed
by Scott Aaronson and Alex Arkhipov in this reference:

https://www.scottaaronson.com/papers/response.pdf

Now, considering that, for cryptographic reasons, to find the security
proof of a complex protocol may be as hard as to break the protocol, how to
verify the security of real-life protocols? I propose to use the Lindy
effect, a phenomenon mentioned by B.B. Mandelbrot in his book "The fractal
geometry of Nature." The risk analyst N. Taleb popularized this phenomenon
in his book "Antifragile: Things That Gain from Disorder." Another
important reference is this article:

Eliazar, Iddo (15 November 2017). "Lindy's Law." Physica A. 486: 797–805.
https://doi.org/10.1016/j.physa.2017.05.077

According to the Lindy effect, a nonperishable system's future life
expectancy is proportional to its current age. To correctly use this
heuristic principle, the corresponding cryptographic protocol must be
exposed to the cryptographic community (especially hackers!), and there
must be a motivation to try to break it. If only a small part of this
community is trying to break this protocol, then the Lindy effect does not
apply, and any system relying upon this protocol will be fragile. This is
because the system satisfying the Lindy effect, in this case, is not just
the cryptographic protocol but also its interaction with the cryptographic
community.

Notice that, when using a proof assistant to verify security, the system
that improves itself is the security argument, not necessarily the
protocol. On the other hand, when the security relies on the Lindy effect,
it is the protocol that improves itself in time. Any attack will motivate
an improvement in the next version of the protocol, regardless of its
complexity. Ultimately, the protocol will evolve, almost in a Darwinist
sense, to a system that will be secure in practice. Still, it may be
extremely hard or maybe impossible to prove its security.

At this point, it may be interesting to read the description of the project
Certified Quantum Security.

Securing digital communication channels is crucial given the amount of
> sensitive data that we exchange every day. Until now, this was achieved by
> using cryptographic protocols, based on the assumption that it is very
> difficult for computers to perform certain mathematical operations. The
> advent of quantum computers will require abandoning classical cryptography
> for novel quantum protocols. Proving the mathematical propositions involved
> in their development will be quite challenging as human intuition is better
> adapted to reason within the classical world and is more prone to errors in
> the quantum realm. The EU-funded CerQuS project is developing new methods
> for verifying the cryptographic security of these mathematical proofs.
> Novel logics and software tools will be applied to secure both classical
> and quantum computers.

https://cordis.europa.eu/project/id/819317

At least to me, it seems likely that the intellectual JUMPS from the
probable security of a simple protocol to the probable security of a
complex protocol may become inaccessible to proof assistants for the same
complexity-theoretic reasons that cryptographic protocols are secure.
Furthermore, when dealing with quantum systems, the number of degrees of
freedom in a composition increases multiplicatively concerning the degrees
of freedom of the components, making the situation even harder for a proof
assistant.

Kind regards,
Jose M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210303/238709a4/attachment-0001.html>