This dissertation tackles crucial issues of web browser security. Web
browsers are now a central part of the trusted code base of any
end-user computer system, as more and more usage shifts to services
provided by web sites that are accessed through those
browsers. Towards this goal we identify three key aspects of web
browser security: (i) the \emph{machine-to-user communication}, (ii)
\emph{internal browser security concerns} and (iii)
\emph{machine-to-machine communication}.

We address aspects (i) and (ii) by developing a methodology that
creates a formal model of a web browser and analyzes that model. We
showcase this on the graphical user interface of both Internet
Explorer and the Illinois Browser Operating System (IBOS) web
browsers. Internal security aspects are addressed in the IBOS browser
for the same origin policy.

For aspect (iii) we look at the formal analysis of cryptographic
protocols, independent of any particular browser.  We focus on the
formal analysis of protocols \emph{modulo algebraic properties} of
their cryptographic functions, since it is well-known the protocol
verification methods that ignore such algebraic properties using a
standard Dolev-Yao model can verify as correct protocols that can be
in fact broken using the algebraic properties. We adopt a symbolic
approach and use the Maude-NPA cryptographic protocol analysis tool,
which has extended unification capabilities modulo theories based on
the new narrowing strategy we developed. We present case studies
showing that appropriate protocols can be analyzed so that either
attacks are found, or the absence of attacks can be proven.