Enforcing Session Integrity in the World "Wild" Web

Over the last years, client-side attacks against web sessions covered a relevant subset of web security incidents. Existing solutions proposed in the literature and by web standards, though interesting, typically address only specific classes of attacks and thus fall short of providing robust foundations to reason on web authentication security. In this thesis we provide such foundations by introducing a novel notion of web session integrity, which allows to capture many existing attacks and spot some new ones. We present FF+, a formal model of a security-enhanced browser that provides a complete and provably sound enforcement of web session integrity. Our theory serves as a basis for the development of SessInt, a client-side solution, implemented as a Google Chrome extension, which provides a level of security very close to FF+, while keeping an eye at usability and user experience.