[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [MirageOS-devel] Security Protocol Analyzers

On 2015-12-15 09:00, Michele Orrà wrote:
Daniel BÃnzli <daniel.buenzli@xxxxxxxxxxxx> 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:


within which we find this snippet, in which the authors outline part of their contribution:

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."

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:


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):



MirageOS-devel mailing list



Lists.xenproject.org is hosted with RackSpace, monitoring our
servers 24x7x365 and backed by RackSpace's Fanatical Support®.