On Sat, Dec 5, 2015 at 8:18 PM, Peter Gutmann <pgut...@cs.auckland.ac.nz> wrote: > Watson Ladd <watsonbl...@gmail.com> writes: >>On Sat, Dec 5, 2015 at 6:54 PM, Peter Gutmann <pgut...@cs.auckland.ac.nz> >>wrote: >>> Hubert Kario <hka...@redhat.com> writes: >>> >>>>miTLS does accept Application Data when it is send between Client Hello and >>>>Client Key Exchange and rejects it when it is sent between Change Cipher >>>>Spec >>>>and Finished. >>> >>> Given that miTLS is a formally verified implementation, would this imply >>> that >>> there's a problem with the verification? "Beware of bugs in the above >>> code; I >>> have only proved it correct, not tried it"? >> >>Are you saying there is a security flaw with the behavior described? > > I hadn't even thought it through to that point, more that you're not supposed > to accept anything between Client Hello and Client Keyex except an optional > Client Certificate. > > (OK, I haven't gone through every extension RFC and draft to see what else you > could poke in there, but I'm pretty sure Application Data isn't one of them).
miTLS did not claim to be consistent with the RFC. Rather it claimed to be secure, and to interoperate with most other implementations in circumstances tested. The informal nature of the RFC makes it impossible to carry out formal verification against it. > > Peter. -- "Man is born free, but everywhere he is in chains". --Rousseau. _______________________________________________ TLS mailing list TLS@ietf.org https://www.ietf.org/mailman/listinfo/tls
