On 2015-12-15 09:00, Michele Orrù wrote:
Daniel Bünzli <[email protected]> writes:
So my question to you and Michele is what properties are you actually
interested to prove ? The notion of "full formal proof" for itself
doesn't make much sense.
This even more that most standard protocols out there neither have a
formal model of legal message exchange beyond a few ambiguous natural
language assertions, nor do they come up with an actual model in which
the properties they are supposed to guarantee can be asserted.
This may be right, but - and please correct me if I'm wrong - for
example you can still try to prove formally¹ that a Dolev-Yao adversary
is never able to retrieve the shared key in a DH key exchange, or in a
TLS session the master secret is never leaked.
It's not much as it doesn't require a statistical or computational
assumptions, but it's a start isn't it?
¹ by "prove formally X" I specifically mean "show that the closure on
the
reductions (specified by $MODEL adversary) of the messages transmitted
has property $PROPERTY".
Hi Michele, I think you're right -- and I also agree with Daniel on the
importance of clarifying what proving "security" means, since different
methods might rely on different assumptions/models, and provide
different guarantees.
For example, consider this article on the current state of the art:
https://www.smacktls.com/smack.pdf
within which we find this snippet, in which the authors outline part of
their contribution:
<quote>
VII. TOWARDS SECURITY THEOREMS FOR OPENSSL
In the previous section, we verified the functional correctness of our
state machine for OpenSSL (a refinement) and proved that our logical
specification is unambiguous (a consistency check). We did not, however,
prove any integrity or confidentiality properties."
</quote>
I think that the kind of setup you described above (in which _secrecy_
appears to be the property of interest) could be served by an "inductive
method"-style approach, as described in this article:
http://www.cl.cam.ac.uk/~lp15/papers/Auth/lics.pdf
I'll take this opportunity to plug a workshop that takes place in Spring
in Cambridge, about the application of formal methods to cryptographic
functions (including protocols):
http://www.cl.cam.ac.uk/research/srg/netos/events/cryptoforma-spring-2016/
Best,
Nik
_______________________________________________
MirageOS-devel mailing list
[email protected]
http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel
