A Study of Automated Verifiers for Security Protocols and Web Applications

Network security is essential because networks have become a basic element of communications. There are two critical parts of network security: security protocols and web applications. For security protocols, secrecy and authentication are two common properties that are usually checked by security protocol verifiers. Secrecy means that no unexpected agents could get the secret contents of messages. Authentication basically indicates that a message which appears to be from some agent is actually sent by the same agent. For web applications, there are many kinds of vulnerabilities. Between them, cross site scripting and injection flaws like SQL injection are the most common vulnerabilities summarized by OWASP. Cross site scripting allows attackers to execute script in the victim''s browser, which can steal user sessions, insert malicious context, and even control the browser. SQL injection inputs unexpected string as queries and can be used to operate the database without authorization.n this thesis, we review several representative verification methods for security protocols and web applications in detail. For security protocols, we study two projects in depth: AVISPA and ProVerif. The commonality of these two projects is that they are both state-exploration methods. However, the AVISPA project has some additional assistant mechanisms such as the lazy intruder to control over the state exploration. We also survey other methods using theorem proving, first-order logic, and model checking. For web applications, the two systems, PQL and WebSSARI, are summarized and discussed. PQL has its own query language to specify vulnerable patterns and utilizes static analysis, which guarantee no false negatives, and dynamic monitoring, which is based on the result of the static analysis. WebSSARI defines the tainted data and sinks in advance and transforms the verification into SAT. It also provides a strategy of efficiently sanitizing. Other related works like AspectJ, SQLCheck, and PTQL are also briefly explained. Finally, we compare AVISPA with ProVerif, and PQL with WebSSARI.