Foundations of provably secure browser-based protocols

The growing proliferation of digital services on the Internet led to a development of numerous Web-based applications (e.g. ecommerce, online banking) in the past years. Browsers place the most important interface to these applications while the underlying security protocols lay the foundations for their safe deployment. Surprisingly, the security of existing browser-based protocols was hardly analyzed in a formal way although contemporary cryptography makes numerous models and methods available. In this thesis we lay the foundations for the rigorous analysis of browser-based protocols. The presented model is based on the paradigm of Universal Composition, which divides protocols into functionalities and enables the analysis of these functionalities in an isolated manner. Security is guaranteed under concurrent composition with arbitrary participants. We present a framework of functionalities to carry out modular design and analysis of browser-based protocols. We construct various protocols and prove security under the assumption that the adversary contaminated some functionalities of the composed protocol. Our protocols are efficient and practicable. They are realizable without relevant changes in existing browser implementations. Security proofs are based on cryptographic standard assumptions.