Web session security : formal verification, client-side enforcement and experimental analysis

Abstract

Web applications are the dominant means to provide access to millions of on-line services and applications such as banking and e-commerce. To personalize users’ web experience, servers need to authenticate the users and then maintain their authentication state throughout a set of related HTTP requests and responses called a web session. As HTTP is a stateless protocol, the common approach, used by most of the web applications to maintain web session, is to use HTTP cookies. Each request belonging to a web session is authenticated by having the web browser to provide to the server a unique long random string, known as session identifier stored as cookie called session cookie. Taking over the session identifier gives full control over to the attacker and hence is an attractive target of the attacker to attack on the confidentiality and integrity of web sessions. The browser should take care of the web session security: a session cookie belonging to one source should not be corrupted or stolen or forced, to be sent with the requests, by any other source.

This dissertation demonstrates that security policies can in fact be written down for both, confidentiality and integrity, of web sessions and enforced at the client side without getting any support from the servers and without breaking too many web applications. Moreover, the enforcement mechanisms designed can be proved correct within mathematical models of the web browsers. These claims are supported in this dissertation by 1) defining both, end-to-end and access control, security policies to protect web sessions; 2) introducing a new and using exiting mathematical models of the web browser extended with confidentiality and integrity security policies for web sessions; 3) offering mathematical proofs that the security mechanisms do enforce the security policies; and 4) designing and developing prototype browser extensions to test that real-life web applications are supported.