Re: [MirageOS-devel] Security Protocol Analyzers

[Nik Sultana <ns441@xxxxxxxxx>]

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:

  https://www.smacktls.com/smack.pdf

within which we find this snippet, in which the authors outline part of 
their contribution:
<quote>
VII. TOWARDS SECURITY THEOREMS FOR OPENSSL
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."
</quote>

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:
  http://www.cl.cam.ac.uk/~lp15/papers/Auth/lics.pdf

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):
  
http://www.cl.cam.ac.uk/research/srg/netos/events/cryptoforma-spring-2016/
Best,
Nik

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