Re: [MirageOS-devel] Security Protocol Analyzers

[Michele Orrà <lists@xxxxxxxxxxxxxxx>]

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
MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel