I would also expect that e.g. if you were to describe almost any existing practical system with purported provable security, it would be straightforward for a layperson with theoretical background (e.g. me) to describe possible attacks that are not precluded by the security proof, and that it wouldn’t even take that long.
I guess SSH itself would be an interesting test of this, e.g. comparing the theoretical model of this paper to a modern implementation. What is your view about that comparison? e.g. how do you think about the following possibilities:
There is no material weakness in the security proof.
A material weakness is already known.
An interested layperson could find a material weakness with moderate effort.
An expert could find a material weakness with significant effort.
My guess would be that probably we’re in world 2, and if not that it’s probably because no one cares that much (e.g. because it’s obvious that there will be some material weakness and the standards of the field are such that it’s not publishable unless it actually comes with an attack) and we are in world 3.
(On a quick skim, and from the author’s language when describing the model, my guess is that material weaknesses of the model are more or less obvious and that the authors are aware of potential attacks not covered by their model.)
In my other response to your comment I wrote:
I guess SSH itself would be an interesting test of this, e.g. comparing the theoretical model of this paper to a modern implementation. What is your view about that comparison? e.g. how do you think about the following possibilities:
There is no material weakness in the security proof.
A material weakness is already known.
An interested layperson could find a material weakness with moderate effort.
An expert could find a material weakness with significant effort.
My guess would be that probably we’re in world 2, and if not that it’s probably because no one cares that much (e.g. because it’s obvious that there will be some material weakness and the standards of the field are such that it’s not publishable unless it actually comes with an attack) and we are in world 3.
(On a quick skim, and from the author’s language when describing the model, my guess is that material weaknesses of the model are more or less obvious and that the authors are aware of potential attacks not covered by their model.)