Daniel Bünzli <[email protected]> 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 [email protected] http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel
