Methods and tools for design time and runtime formal analysis of security protocols and web applications

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.