Formal Security Analysis of Web Protocols

Formal Security Analysis Of Web Protocols

Thursday 15A

Convener: Daniel Fett

Notes-taker(s): Daniel Fett

Tags for the session - technology discussed/ideas considered:

#formalmethods, #oauth, #oidc, #attacks, #proofs, #security

Discussion notes, key understandings, outstanding questions, observations, and, if appropriate to this discussion: action items, next steps:

Presentation slides: https://danielfett.de/download/thesis-defense.pdf

The work this presentation is based on, including the formal models and case studies: https://elib.uni-stuttgart.de/bitstream/11682/10214/1/%27An%20Expressive%20Formal%20Model%20of%20the%20Web%20Infrastructure.pdf

The formal analysis efforts resulted in improvements to the security of OAuth that are described in the new OAuth Security BCP RFC draft: https://tools.ietf.org/html/draft-ietf-oauth-security-topics-11

Summary of the new security recommendations: https://danielfett.de/download/locomocosec-2019-how-not-to-use-oauth.pdf