Re: [MirageOS-devel] Security Protocol Analyzers

[Daniel BÃnzli <daniel.buenzli@xxxxxxxxxxxx>]

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

Best,  

Daniel

_______________________________________________
MirageOS-devel mailing list
MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel