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

Re: [MirageOS-devel] Security Protocol Analyzers

Le mardi, 15 dÃcembre 2015 à 09:00, Michele Orrà a Ãcrit :
> 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?

Sure it's a start, but I would hardly call that a "proof of the security of the 
component". This is why I'm asking about the specifics of your ideas.  

Talking about proving programs without asking what is actually being proved can 
be quite misleading in general. I guess in the future we'll see people claim 
they have "proved" their programs as much as we nowaday have people claiming 
they are doing "functional programming" with their imperative spaghettis...  



MirageOS-devel mailing list



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