Assuring next generation web security

Communications on the Internet are often protected by using security protocols. However, many security flaws have recently been found in widely-used protocols such as TLS/SSL. Such flaws may allow attackers to impersonate yourself and/or steal your information from the communications. In this work we analyze the next-generation web security protocols by using formal methods. Formal methods based on mathematical logics allow us to rigorously verify expected security of protocols as logical formulae and to find attacks (if any) that are hard to be found even by experts. We have shown that the QUIC protocol developed by Google does not satisfy certain security that has been "proved" in previous work, and also that TLS1.3, the next version of TLS, is secure with respect to our security definitions.

Please click the thumbnail image to open the full-size PDF file.