The Coq mailing list

[Wilayat Khan <wilayatk AT gmail.com>]

Dear Hutton

  Am interested in publishing my thesis in your journal. Please find enclosed abstract and other details. We have used

theorem prover Coq to build formal model of web browser and proved interesting security properties of web sessions. 

Best, 

Wilayat 

-------------------------------------------------------------------------------------

-------------------------------------------------------------------------------------

o Web Session Security: Formal Verification, Client-Side Enforcement and Experimental

                                    Analysis

o Student: Wilayat Khan

o Awarding institution: Università Ca’ Foscari di Venezia, Italy

o Feb 13, 2015

o Advisor/supervisor: Prof Michele Bugliesi

o Dissertation URL: http://dspace.unive.it/bitstream/handle/10579/5646/955962-1173399.pdf?sequence=2

o Dissertation 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.

Virus-free. www.avast.com