The importance of knowing what type of traffic is flowing through a network is paramount to its success. Traffic shaping, Quality of Service, identifying critical business applications, Intrusion Detection Systems, as well as network administra- tion activities all require the base knowledge of what traffic is flowing over a network before any further steps can be taken. With SSL traffic on the rise due to applica- tions securing or concealing their traffic, the ability to determine what applications are running within a network is getting more and more difficult. Traditional methods of traffic classification through port numbers or deep packet inspection have been deemed inadequate by researchers thus making way for new methods. The purpose of this thesis is to investigate if a machine learning approach can be used with flow features to identify SSL in a given network trace. To this end, different machine learning methods are investigated without the use of port numbers, Internet Protocol addresses, or payload information. Various machine learning models are investigated including AdaBoost, Naive Bayes, RIPPER, and C4.5. The robustness of the results are tested against unseen datasets during training. Moreover, the proposed approach is compared to the Wireshark traffic analysis tool. Results show that the proposed ap- proach is very promising in identifying SSL traffic from a given network trace without using port numbers, Internet protocol addresses, or payload information.

TLS and IPsec are two protocols that provide secure communication on the Internet. They provide similar services but operate on different levels. This report compiles some of thecurrent known vulnerabilities that exist in those two protocols. It also describes attacks that exploit those vulnerabilities. Based on the vulnerabilities this paper gives guidelines onhow to avoid them when implementing TLS and IPsec. This paper also demonstrates a proof-of-concept that shows how IPsec can be configured to avoid some of the vulnerabilities. Theproof-of-concept also shows how IPsec can be used to setup a secure connection between two peers, using Near Field Communication, on an ad hoc network.

Recent progress in the field of quantum computers provide radically improved muscles to search and sort in lists, solve systems of equations and prime factorize – virtues that inflict an immediate threat to the most common systems for public key cryptography used in a vast proportion of today’s computer networks. NTRUEncrypt is a lattice-based cryptography system which inhibits quantum computers for breaking the algorithm in polynomial time. The cryptographic algorithm is one of the seventeen that passed the first round in the NIST Post-Quantum standardisation competition which serves an indication that this system is robust against the efforts from a cryptanalysist to compromise its security properties. With the development of a server and client application that is built using Python3 integrated with WolfSSL, the results obtained from the experiment show that the suggested model acquires the capabilities to overcome the quantum computers capacities, providing fast quantum-safe asymmetric encryption algorithm for TLS communication in smart homes. The handshake process with NTRUEncrypt and WolfSSL is proven to be significantly faster comparing to other algorithms tested.

This thesis concerns the security of tomorrow’s peer-to-peer real-time communication in heterogeneous networks. Because of the additional delay caused by inband handshake and the poor compatibilities of some transport protocols, it was determined that existing security protocols such as transport layer security (TLS) and datagram transport layer security (DTLS) are not suitable in such a user scenario and a new security protocol should be designed. This new security protocol is called transport encapsulation security payload (TESP). TESP not only has the advantage of low initialization delay, but also fully supports transport protocols including TCP, UDP, stream control transmission protocol (SCTP), and datagram congestion control protocol (DCCP). Also a security analysis of TESP was carried out and no security flaws were found. / Denna uppsats behandlar säkerheten för morgondagens "peer-to-peer" (P2P) realtidskommunikation i heterogena nät. På grund av den adderade fördröjning som orsakas av inbandssignalering och dålig kompabilitet hos många transportprotokoll, så kan man fastställa att existerande säkerhetsprotokoll, såsom "(Datagram) Transport Layer Security" (TLS och DTLS), inte är lämpade för denna typ av kommunikation och att ett nytt säkerhetsprotokoll bör tas fram. "Transport Encapsulation Security Payload" (TESP) är ett sådant protokoll. TESP har inte bara fördelar såsom låg uppstartsfördröjning, utan har också stöd för många transportprotokoll, t.ex. "Transport Control Protocol" (TCP), "User Datagram Protocol" (UDP), "Stream Control Transmission Protocol" (SCTP) och "Datagram Congestion Control Protocol" (DCCP). Även en säkerhetsanalys av TESP har gjorts, där inga säkerhetsproblem har kunnat påvisas.

Transport Layer Security (TLS) is a vital component to the security ecosystem and the most popular security protocol used on the Internet today. Despite the strengths of the protocol, numerous vulnerabilities result from its improper use in practice. Some of these vulnerabilities arise from weaknesses in authentication, from the rigidity of the trusted authority system to the complexities of client certificates. Others result from the misuse of TLS by developers, who misuse complicated TLS libraries, improperly validate server certificates, employ outdated cipher suites, or deploy other features insecurely. To make matters worse, system administrators and users are powerless to fix these issues, and lack the ability to properly control how their own machines communicate securely online. In this dissertation we argue that the problems described are the result of an improper placement of security responsibilities. We show that by placing TLS services in the operating system, both new and existing applications can be automatically secured, developers can easily use TLS without intimate knowledge of security, and security settings can be controlled by administrators. This is demonstrated through three explorations that provide TLS features through the operating system. First, we describe and assess TrustBase, a service that repairs and strengthens certificate-based authentication for TLS connections. TrustBase uses traffic interception and a policy engine to provide administrators fine-tuned control over the trust decisions made by all applications on their systems. Second, we introduce and evaluate the Secure Socket API (SSA), which provides TLS as an operating system service through the native POSIX socket API. The SSA enables developers to use modern TLS securely, with as little as one line of code, and also allows custom tailoring of security settings by administrators. Finally, we further explore a modern approach to TLS client authentication, leveraging the operating system to provide a generic platform for strong authentication that supports easy deployment of client authentication features and protects user privacy. We conclude with a discussion of the reasons for the success of our efforts, and note avenues for future work that leverage the principles exhibited in this work, both in and beyond TLS.

When performing fingerprinting attacks against websites in a controlled environment astudy may achieve very promising results. However, these can be misleading as the closedworld setting may not accurately represent the real-world. This is a problem many priorworks have been critiqued for, the inability to transfer their results from the closed-worldsetting to the real-world. Being able to do so is of great importance to establish what thereal-world consequences would be of fingerprint attacks. If unable to apply one’s findingsoutside of a tightly controlled environment it is difficult to gauge if these attacks types posea real threat or not. Thereby, this thesis has, contrary to previous work, based its settingon a real-world scenario to provide tangible insights into vulnerabilities of news websites.Furthermore, it targeted internal pages of websites, something understudied by previousliterature. All of this while presenting a novel classifier that is lightweight and requireslittle training, and a framework for automatically collecting and labelling encrypted TCPtraffic without the use of a proxy.

Governments, military, corporations, financial institutions and others exchange a great deal of confidential information using Internet these days. Protecting such confidential information and ensuring their integrity and origin authenticity are of paramount importance. There exist protocols and solutions at different layers of the TCP/IP protocol stack to address these security requirements. Application level encryption viz. PGP for secure mail transfer, TLS based secure TCP communication, IPSec for providing IP layer security are among these security solutions. Due to scalability, wide acceptance of the IP protocol, and its application independent character, the IPSec protocol has become a standard for providing Internet security. The IPSec provides two protocols namely the Authentication header (AH) and the Encapsulating Security Payload (ESP). Each protocol can operate in two modes, viz. transport and tunnel mode. The AH provides data origin authentication, connectionless integrity and anti replay protection. The ESP provides all the security functionalities of AH along with confidentiality. The IPSec protocols provide end-to-end security for an entire IP datagram or the upper layer protocols of IP payload depending on the mode of operation. However, this end-to-end model of security restricts performance enhancement and security related operations of intermediate networking and security devices, as they can not access or modify transport and upper layer headers and original IP headers in case of tunnel mode. These intermediate devices include routers providing Quality of Service (QoS), TCP Performance Enhancement Proxies (PEP), Application level Proxy devices and packet filtering firewalls. The interoperability problem between IPSec and intermediate devices has been addressed in literature. Transport friendly ESP (TF-ESP), Transport Layer Security (TLS), splitting of single IPSec tunnel into multiple tunnels, Multi Layer IPSec (ML-IPSec) are a few of the proposed solutions. The ML-IPSec protocol solves this interoperability problem without violating the end-to-end security for the data or exposing some important header fields unlike the other solutions. The ML-IPSec uses a multilayer protection model in place of the single end-to-end model. Unlike IPSec where the scope of encryption and authentication applies to the entire IP datagram, this scheme divides the IP datagram into zones. It applies different protection schemes to different zones. When ML-IPSec protects a traffic stream from its source to its destination, it first partitions the IP datagram into zones and applies zone-specific cryptographic protections. During the flow of the ML-IPSec protected datagram through an authorized intermediate gateway, certain type I zones of the datagram may be decrypted and re-encrypted, but the other zones will remain untouched. When the datagram reaches its destination, the ML-IPSec will reconstruct the entire datagram. The ML-IPSec protocol, however suffers from the problem of static configuration of zones and zone specific cryptographic parameters before the commencement of the communication. Static configuration requires a priori knowledge of routing infrastructure and manual configuration of all intermediate nodes. While this may not be an issue in a geo-stationary satellite environment using TCP-PEP, it could pose problems in a mobile or distributed environment, where many stations may be in concurrent use. The ML-IPSec endpoints may not be trusted by all intermediate nodes in a mobile environment for manual configuration without any prior arrangement providing the mutual trust. The static zone boundary of the protocol forces one to ignore the presence of TCP/IP datagrams with variable header lengths (in case of TCP or IP headers with OPTION fields). Thus ML-IPSec will not function correctly if the endpoints change the use of IP or TCP options, especially in case of tunnel mode. The zone mapping proposed in ML-IPSec is static in nature. This forces one to configure the zone mapping before the commencement of the communication. It restricts the protocol from dynamically changing the zone mapping for providing access to intermediate nodes without terminating the existing ML-IPSec communication. The ML-IPSec endpoints can off course, configure the zone mapping with maximum number of zones. This will lead to unnecessary overheads that increase with the number of zones. Again, static zone mapping could pose problems in a mobile or distributed environment, where communication paths may change. Our extension to the ML-IPSec protocol, called Dynamic Multi Layer IPSec (DML-IPSec) proposes a multi layer variant with the capabilities of dynamic zone configuration and sharing of cryptographic parameters between IPSec endpoints and intermediate nodes. It also accommodates IP datagrams with variable length headers. The DML-IPSec protocol redefines some of the IPSec and ML-IPSec fundamentals. It proposes significant modifications to the datagram processing stage of ML-IPSec and proposes a new key sharing protocol to provide the above-mentioned capabilities. The DML-IPSec supports the AH and ESP protocols of the conventional IPSec with some modifications required for providing separate cryptographic protection to different zones of an IP datagram. This extended protocol defines zone as a set of non-overlapping and contiguous partitions of an IP datagram, unlike the case of ML-IPSec where a zone may consist of non-contiguous portions. Every zone is provided with cryptographic protection independent of other zones. The DML-IPSec categorizes zones into two separate types depending on the accessibility requirements at the intermediate nodes. The first type of zone, called type I zone, is defined on headers of IP datagram and is required for examination and modification by intermediate nodes. One type I zone may span over a single header or over a series of contiguous headers of an IP datagram. The second type of zone, called type II zone, is meant for the payload portion and is kept secure between endpoints of IPSec communications. The single type II zone starts immediately after the last type I zone and spans till the end of the IP datagram. If no intermediate processing is required during the entire IPSec session, the single type II zone may cover the whole IP datagram; otherwise the single type II zone follows one or more type I zones of the IP datagram. The DML-IPSec protocol uses a mapping from the octets of the IP datagram to different zones, called zone map for partitioning an IP datagram into zones. The zone map contains logical boundaries for the zones, unlike physical byte specific boundaries of ML-IPSec. The physical boundaries are derived on-the-fly, using either the implicit header lengths or explicit header length fields of the protocol headers. This property of the DML-IPSec zones, enables it to accommodate datagrams with variable header lengths. Another important feature of DML-IPSec zone is that the zone maps need not remain constant through out the entire lifespan of IPSec communication. The key sharing protocol may modify any existing zone map for providing service to some intermediate node. The DML-IPSec also redefines Security Association (SA), a relationship between two endpoints of IPSec communication that describes how the entities will use security services to communicate securely. In the case of DML-IPSec, several intermediate nodes may participate in defining these security protections to the IP datagrams. Moreover, the scope of one particular set of security protection is valid on a single zone only. So a single SA is defined for each zone of an IP datagram. Finally all these individual zonal SA’s are combined to represent the security relationship of the entire IP datagram. The intermediate nodes can have the cryptographic information of the relevant type I zones. The cryptographic information related to the type II zone is, however, hidden from any intermediate node. The key sharing protocol is responsible for selectively sharing this zone information with the intermediate nodes. The DML-IPSec protocol has two basic components. The first one is for processing of datagrams at the endpoints as well as intermediate nodes. The second component is the key sharing protocol. The endpoints of a DML-IPSec communication involves two types of processing. The first one, called Outbound processing, is responsible for generating a DML-IPSec datagram from an IP datagram. It first derives the zone boundaries using the zone map and individual header field lengths. After this partitioning of IP datagram, zone wise encryption is applied (in case of ESP). Finally zone specific authentication trailers are calculated and appended after each zone. The other one, Inbound processing, is responsible for generating the original IP datagram from a DML-IPSec datagram. The first step in the inbound processing, the derivation of zone boundary, is significantly different from that of outbound processing as the length fields of zones remain encrypted. After receiving a DML-IPSec datagram, the receiver starts decrypting type I zones till it decrypts the header length field of the header/s. This is followed by zone-wise authentication verification and zone-wise decryption. The intermediate nodes processes an incoming DML-IPSec datagram depending on the presence of the security parameters for that particular DML-IPSec communication. In the absence of the security parameters, the key sharing protocol gets executed; otherwise, all the incoming DML-IPSec datagrams get partially decrypted according to the security association and zone mapping at the inbound processing module. After the inbound processing, the partially decrypted IP datagram traverses through the networking stack of the intermediate node . Before the IP datagram leaves the intermediate node, it is processed by the outbound module to reconstruct the DML-IPSec datagram. The key sharing protocol for sharing zone related cryptographic information among the intermediate nodes is the other important component of the DML-IPSec protocol. This component is responsible for dynamically enabling intermediate nodes to access zonal information as required for performing specific services relating to quality or security. Whenever a DML-IPSec datagram traverses through an intermediate node, that requires access to some of the type I zones, the inbound security database is searched for cryptographic parameters. If no entry is present in the database, the key sharing protocol is invoked. The very first step in this protocol is a header inaccessible message from the intermediate node to the source of the DML-IPSec datagram. The intermediate node also mentions the protocol headers that it requires to access in the body portion of this message. This first phase of the protocol, called the Zone reorganization phase, is responsible for deciding the zone mapping to provide access to intermediate nodes. If the current zone map can not serve the header request, the DML-IPSec endpoint reorganizes the existing zone map in this phase. The next phase of the protocol, called the Authentication Phase is responsible for verifying the identity of the intermediate node to the source of DML-IPSec session. Upon successful authentication, the third phase, called the Shared secret establishment phase commences. This phase is responsible for the establishment of a temporary shared secret between the source and intermediate nodes. This shared secret is to be used as key for encrypting the actual message transfer of the DML-IPSec security parameters at the next phase of the protocol. The final phase of the protocol, called the Security parameter sharing phase, is solely responsible for actual transfer of the security parameters from the source to the intermediate nodes. This phase is also responsible for updation of security and policy databases of the intermediate nodes. The successful execution of the four phases of the key sharing protocol enables the DML-IPSec protocol to dynamically modify the zone map for providing access to some header portions for intermediate nodes and also to share the necessary cryptographic parameters required for accessing relevant type I zones without disturbing an existing DML-IPSec communication. We have implemented the DML-IPSec for ESP protocol according to the definition of zones along with the key sharing algorithm. RHEL version 4 and Linux kernel version 2.6.23.14 was used for the implementation. We implemented the multi-layer IPSec functionalities inside the native Linux implementation of IPSec protocol. The SA structure was updated to hold necessary SA information for multiple zones instead of single SA of the normal IPSec. The zone mapping for different zones was implemented along with the kernel implementation of SA. The inbound and outbound processing modules of the IPSec endpoints were re-implemented to incorporate multi-layer IPSec capability. We also implemented necessary modules for providing partial IPSec processing capabilities at the intermediate nodes. The key sharing protocol consists of some user space utilities and corresponding kernel space components. We use ICMP protocol for the communications required for the execution of the protocol. At the kernel level, pseudo character device driver was implemented to update the kernel space data structures and necessary modifications were made to relevant kernel space functions. User space utilities and corresponding kernel space interface were provided for updating the security databases. As DML-IPSec ESP uses same Security Policy mechanism as IPSec ESP, existing utilities (viz. setkey) are used for the updation of security policy. However, the configuration of the SA is significantly different as it depends on the DML-IPSec zones. The DML-IPSec ESP implementation uses the existing utilities (setkey and racoon) for configuration of the sole type II zone. The type I zones are configured using the DML-IPSec application. The key sharing protocol also uses this application to reorganize the zone mapping and zone-wise cryptographic parameters. The above feature enables one to use default IPSec mechanism for the configuration of the sole type II zone. For experimental validation of DML-IPSec, we used the testbed as shown in the above figure. An ESP tunnel is configured between the two gateways GW1 and GW2. IN acts as an intermediate node and is installed with several intermediate applications. Clients C11 and C21 are connected to GW1 and GW2 respectively. We carried out detailed experiments for validating our solution w.r.t firewalling service. We used stateful packet filtering using iptables along with string match extension at IN. First, we configured the firewall to allow only FTP communication (using port information of TCP header and IP addresses of Inner IP header ) between C11 and C21. In the second experiment, we configured the firewall to allow only Web connection between C11 and C21 using the Web address of C11 (using HTTP header, port information of TCP header and IP addresses of Inner IP header ). In both experiments, we initiated the FTP and WEB sessions before the execution of the key sharing protocol. The session could not be established as the access to upper layer headers was denied. After the execution of the key sharing protocol, the sessions could be established, showing the availability of protocol headers to the iptables firewall at IN following the successful key sharing. We use record route option of ping program to validate the claim of handling datagrams with variable header lengths. This option of ping program records the IP addresses of all the nodes traversed during a round trip path in the IP OPTION field. As we used ESP in tunnel mode between GW1 and GW2, the IP addresses would be recorded inside the encrypted Inner IP header. We executed ping between C11 and C21 and observed the record route output. Before the execution of the key sharing protocol, the IP addresses of IN were absent in the record route output. After the successful execution of key sharing protocol, the IP addresses for IN were present at the record route output. The DML-IPSec protocol introduces some processing overhead and also increases the datagram size as compared to IPSec and ML-IPSec. It increases the datagram size compared to the standard IPSec. However, this increase in IP datagram size is present in the case of ML-IPSec as well. The increase in IP datagram length depends on the number of zones. As the number of zone increases this overhead also increases. We obtain experimental results about the processing delay introduced by DML-IPSec processing. For this purpose, we executed ping program from C11 to C21 in the test bed setup for the following cases: 1.ML-IPSec with one type I and one type II zone and 2. DML-IPSec with one type I and one type II zone. We observe around 10% increase in RTT in DML-IPSec with two dynamic zones over that of ML-IPSec with two static zones. This overhead is due to on-the-fly derivation of the zone length and related processing. The above experiment analyzes the processing delay at the endpoints without intermediate processing. We also analyzed the effect of intermediate processing due to dynamic zones of DML-IPSec. We used iptables firewall in the above mentioned experiment. The RTT value for DML-IPSec with dynamic zones increases by less than 10% over that of ML-IPSec with static zones. To summarize our work, we have proposed an extension to the multilayer IPSec protocol, called Dynamic Multilayer IPSec (DML-IPSec). It is capable of dynamic modification of zones and sharing of cryptographic parameters between endpoints and intermediate nodes using a key sharing protocol. The DML-IPSec also accommodates datagrams with variable header lengths. The above mentioned features enable any intermediate node to dynamically access required header portions of any DML-IPSec protected datagrams. Consequently they make the DML-IPSec suited for providing IPSec over mobile and distributed networks. We also provide complete implementation of ESP protocol and provide experimental validation of our work. We find that our work provides the dynamic support for QoS and security services without any significant extra overhead compared to that of ML-IPSec. The thesis begins with an introduction to communication security requirements in TCP/IP networks. Chapter 2 provides an overview of communication security protocols at different layers. It also describes the details of IPSec protocol suite. Chapter 3 provides a study on the interoperability issues between IPSec and intermediate devices and discusses about different solutions. Our proposed extension to the ML-IPSec protocol, called Dynamic ML-IPSec(DML-IPSec) is presented in Chapter 4. The design and implementation details of DML-IPSec in Linux environment is presented in Chapter 5. It also provides experimental validation of the protocol. In Chapter 6, we summarize the research work, highlight the contributions of the work and discuss the directions for further research.

Est-il possible de démontrer un théorème prouvant que l’accès aux données confidentielles d’un utilisateur d’un service Web (tel que GMail) nécessite la connaissance de son mot de passe, en supposant certaines hypothèses sur ce qu’un attaquant est incapable de faire (par exemple, casser des primitives cryptographiques ou accéder directement aux bases de données de Google), sans toutefois le restreindre au point d’exclure des attaques possibles en pratique?Il existe plusieurs facteurs spécifiques aux protocoles du Web qui rendent impossible une application directe des méthodes et outils existants issus du domaine de l’analyse des protocoles cryptographiques.Tout d’abord, les capacités d’un attaquant sur le Web vont largement au-delà de la simple manipulation des messages échangés entre le client et le serveur sur le réseau. Par exemple, il est tout à fait possible (et même fréquent en pratique) que l’utilisateur ait dans son navigateur un onglet contenant un site contrôlé par l’adversaire pendant qu’il se connecte à sa messagerie (par exemple, via une bannière publicitaire) ; cet onglet est, comme n’importe quel autre site, capable de provoquer l’envoi de requêtes arbitraires vers le serveur de GMail, bien que la politique d’isolation des pages du navigateur empêche la lecture directe de la réponse à ces requêtes. De plus, la procédure pour se connecter à GMail implique un empilement complexe de protocoles : tout d’abord, un canal chiffré, et dont le serveur est authentifié, est établi avec le protocole TLS ; puis, une session HTTP est créée en utilisant un cookie ; enfin, le navigateur exécute le code JavaScript retourné par le client, qui se charge de demander son mot de passe à l’utilisateur.Enfin, même en imaginant que la conception de ce système soit sûre, il suffit d’une erreur minime de programmation (par exemple, une simple instruction goto mal placée) pour que la sécurité de l’ensemble de l’édifice s’effondre.Le but de cette thèse est de bâtir un ensemble d’outils et de librairies permettant de programmer et d’analyser formellement de manière compositionelle la sécurité d’applicationsWeb confrontées à un modère plausible des capacités actuelles d’un attaquant sur le Web. Dans cette optique, nous étudions la conception des divers protocoles utilisés à chaque niveau de l’infrastructure du Web (TLS, X.509, HTTP, HTML, JavaScript) et évaluons leurs compositions respectives. Nous nous intéressons aussi aux implémentations existantes et en créons de nouvelles que nous prouvons correctes afin de servir de référence lors de comparaisons. Nos travaux mettent au jour un grand nombre de vulnérabilités aussi bien dans les protocoles que dans leurs implémentations, ainsi que dans les navigateurs, serveurs, et sites internet ; plusieurs de ces failles ont été reconnues d’importance critiques. Enfin, ces découvertes ont eu une influence sur les versions actuelles et futures du protocole TLS. / As ever more private user data gets stored on the Web, ensuring proper protection of this data (in particular when it transits through untrusted networks, or when it is accessed by the user from her browser) becomes increasingly critical. However, in order to formally prove that, for instance, email from GMail can only be accessed by knowing the user’s password, assuming some reasonable set of assumptions about what an attacker cannot do (e.g. he cannot break AES encryption), one must precisely understand the security properties of many complex protocols and standards (including DNS, TLS, X.509, HTTP, HTML,JavaScript), and more importantly, the composite security goals of the complete Web stack.In addition to this compositional security challenge, onemust account for the powerful additional attacker capabilities that are specific to the Web, besides the usual tampering of network messages. For instance, a user may browse a malicious pages while keeping an active GMail session in a tab; this page is allowed to trigger arbitrary, implicitly authenticated requests to GMail using JavaScript (even though the isolation policy of the browser may prevent it from reading the response). An attacker may also inject himself into honest page (for instance, as a malicious advertising script, or exploiting a data sanitization flaw), get the user to click bad links, or try to impersonate other pages.Besides the attacker, the protocols and applications are themselves a lot more complex than typical examples from the protocol analysis literature. Logging into GMail already requires multiple TLS sessions and HTTP requests between (at least) three principals, representing dozens of atomic messages. Hence, ad hoc models and hand written proofs do not scale to the complexity of Web protocols, mandating the use of advanced verification automation and modeling tools.Lastly, even assuming that the design of GMail is indeed secure against such an attacker, any single programming bug may completely undermine the security of the whole system. Therefore, in addition to modeling protocols based on their specification, it is necessary to evaluate implementations in order to achieve practical security.The goal of this thesis is to develop new tools and methods that can serve as the foundation towards an extensive compositional Web security analysis framework that could be used to implement and formally verify applications against a reasonably extensive model of attacker capabilities on the Web. To this end, we investigate the design of Web protocols at various levels (TLS, HTTP, HTML, JavaScript) and evaluate their composition using a broad range of formal methods, including symbolic protocol models, type systems, model extraction, and type-based program verification. We also analyze current implementations and develop some new verified versions to run tests against. We uncover a broad range of vulnerabilities in protocols and their implementations, and propose countermeasures that we formally verify, some of which have been implemented in browsers and by various websites. For instance, the Triple Handshake attack we discovered required a protocol fix (RFC 7627), and influenced the design of the new version 1.3 of the TLS protocol.