Re: [TLS] Formal Verification of TLS 1.3 Full Handshake Protocol Using ProVerif (Draft-11)

Hi Ilari, Thank you for your kind comments. We will try to commented cases. Regards, Shin’ichiro Matsuo > On Feb 25, 2016, at 12:11 PM, Ilari Liusvaara > wrote: > > On Thu, Feb 25, 2016 at 08:05:58AM -0800, Shin'ichiro Matsuo wrote: > >> >> - >> >> [Wha

Re: [TLS] Formal Verification of TLS 1.3 Full Handshake Protocol Using ProVerif (Draft-11)

On Thu, Feb 25, 2016 at 08:05:58AM -0800, Shin'ichiro Matsuo wrote: > > - > > [What's checked] > We checked the TLS draft-11 full handshake protocol for the following two > properties. > * Secrecy of payload: Can the attacker know the encrypted payload? > * A

[TLS] Formal Verification of TLS 1.3 Full Handshake Protocol Using ProVerif (Draft-11)

Hi all, [Introduction] CELLOS (Cryptographic protocol Evaluation toward Long-Lived Outstanding Security) forms a team for formal verification of TLS. It has modeled TLS 1.3 draft specification and conducted verification by using ProVerif. Until now, we have modeled the full handshake protocol