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

Re: [MirageOS-devel] Security Protocol Analyzers

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


MirageOS-devel mailing list



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