Marco Rocchetto's website
PhD Thesis
Methods and tools for design time and runtime formal analysis of security protocols and web applications
Abstract. The increasing complexity of web applications together with their underling
security protocols has rapidly increased the need of automatic security analysis methods and tools.
In this thesis, I address this problem by proposing two new
formal approaches for the security verification of security protocols and web applications.
The first is a design time interpolation-based method for security protocol verification.
This method starts from a protocol specification and combines Craig interpolation,
symbolic execution and the standard Dolev-Yao intruder model to search for
possible attacks on the protocol. Interpolants are generated as a response to search
failure in order to prune possible useless traces and speed up the exploration.
The second is a runtime (model-based) security analysis technique that searches
for logic and implementation flaws on concrete (web-based) systems. In particular,
I focused on how to use the Dolev-Yao intruder model to search for Cross-Site Request Forgery (CSRF) attacks.
CSRF is listed in the top ten list of the Open Web
Application Security Project (OWASP) as one of the most critical threats to web
security.
- Thesis (pdf) [last update May, 13 2015]
- Slides (pdf) [last update May, 13 2015]
- SPiM tool