Many security protocols are built as the composition of an application-layer protocol and a secure transport protocol, such as TLS. There are many approaches to proving the correctness of such protocols. One popular approach is verification by abstraction, in which the correctness of the application-layer protocol is proven under the assumption that the transport layer satisfies certain properties, such as confidentiality. Following this approach, we adapt the strand spaces model in order to analyse application-layer protocols that depend on an underlying secure transport layer, including unilaterally authenticating secure transport protocols, such as unilateral TLS. Further, we develop proof rules that enable us to prove the correctness of application-layer protocols that use either unilateral or bilateral secure transport protocols. We then illustrate these rules by proving the correctness of WebAuth, a single-sign-on protocol that makes extensive use of unilateral TLS. In this thesis we also present a full proof of the model's soundness. In particular, we prove that, subject to a suitable independence assumption, if there is an attack against the application-layer protocol when layered on top of a particular secure transport protocol, then there is an attack against the abstracted model of the application-layer protocol. In contrast to existing work in this area, the independence assumption consists of eight statically-checkable conditions, meaning that it can be checked statically, rather than having to consider all possible runs of the protocol. Lastly, we extend the model to allow protocols that consist of an arbitrary number of layers to be proven correct. In this case, we prove the correctness of the intermediate layers using the high-level strand spaces model, by abstracting away from the underlying transport-layers. Further, we extend the above soundness results in order to prove that the multi-layer approach is sound. We illustrate the effectiveness of our technique by proving the correctness of a couple of simple multi-layer protocols.

Security is a major concern is today's online world. As online activities become increasingly sensitive, service providers rely on security protocols to ensure confidentiality, integrity and authentication of their users and data. Greater assurance is provided when these protocols are verified to be correct. Strand Spaces is a method to formally analyze security protocols. The arguments are based on the messages being transmitted and received while assuming that the underlying cryptographic primitives are secure. This thesis demonstrates that the protocols Luau, pwdArmor and Kiwi are secure using Strand Spaces methodology.

Orientador: Ricardo Dahab / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-13T10:57:18Z (GMT). No. of bitstreams: 1 Piva_FabioRogerio_M.pdf: 1281624 bytes, checksum: 2d4f949b868d1059e108b1cd79314629 (MD5) Previous issue date: 2009 / Resumo: Os protocolos de trocas justas foram propostos como solução para o problema da troca de itens virtuais, entre duas ou mais entidades, sem que haja a necessidade de confiança entre elas. A popularização da internet criou uma crescente classe de usuários leigos que diariamente participam de transações de troca, como comercio eletrônico (e-commerce), internet banking, redes ponto-a-ponto (P2P), etc. Com tal demanda por justiça, e preciso garantir que os protocolos de trocas justas recebam a mesma atenção acadêmica dedicada aos protocolos clássicos. Neste contexto, fazem-se necessárias diretrizes de projeto, ferramentas de verificação, taxonomias de ataques e quaisquer outros artefatos que possam auxiliar na composição de protocolos sem falhas. Neste trabalho, apresentamos um estudo sobre o problema de trocas justas e o atual estado da arte das soluções propostas, bem como a possibilidade de criar, a partir de técnicas para a verificação formal e detecção de falhas em protocolos clássicos, metodologias para projeto e correção de protocolos de trocas justas. / Abstract: Fair exchange protocols were first proposed as a solution to the problem of exchanging digital items, between two or more entities, without forcing them to trust each other. The popularization of the internet resulted in an increasing amount of lay users, which constantly participate in exchange transactions, such as electronic commerce (ecommerce), internet banking, peer-to-peer networks (P2P), etc. With such demand for fairness, we need to ensure that fair exchange protocols receive the same amount of attention, from academia, as classic protocols do. Within this context, project guideliness are needed, and so are verification tools, taxonomies of attack, and whatever other artifacts that may help correct protocol design. In this work we present a study on the fair exchange problem and the current state-of-the-art of proposed solutions, as well as a discussion on the possibility of building, from currently available formal verification and attack detection techniques for classic protocols, methods for fair exchange protocols design and correction. / Mestrado / Ciência da Computação / Mestre em Ciência da Computação