http://repositorio.unb.br/handle/10482/37764
Fichier | Description | Taille | Format | |
---|---|---|---|---|
2019_FelipeRodopoulosdeOliveira.pdf | 715,41 kB | Adobe PDF | Voir/Ouvrir |
Titre: | Verification of the Dynamic Authorization Protocol |
Auteur(s): | Oliveira, Felipe Rodopoulos de |
Orientador(es):: | Nalon, Cláudia |
Assunto:: | Internet banking Protocolos de segurança Formalização de protocolos Transações bancárias Prova de teoremas |
Date de publication: | 15-mai-2020 |
Data de defesa:: | 26-jui-2019 |
Référence bibliographique: | OLIVEIRA, Felipe Rodopoulos de. Verification of the Dynamic Authorization Protocol. 2019. xvii, 112 f., il. Dissertação (Mestrado em Informática)—Universidade de Brasília, Brasília, 2019. |
Résumé: | Questões em segurança compõem grande parte dos desafios das soluções de internet banking. Diferentes protocolos de segurança foram projetados visando prover confiabilidade para transações bancárias online. O Protocolo de Autorização Dinâmica segue um esquema onde uma chave compartilhada entre o banco e o usuário é estabelecida para uso em futuras transações bancárias online. Em cada transação, o usuário é desafiado a recuperar e apresentar uma chave de transação única ao servidor, usando um smartphone como uma entidade externa de validação que escaneia um QR-code para testes de integridade. Dessa forma o usuário consegue realizar operações em um computador inseguro e validá-las em um canal offline. Entretanto, o protocolo não é formalmente verificado. Neste trabalho, utilizamos a teoria do Método Indutivo para formalizar e verificar as propriedades do protocolo. Uma extensão desta teoria foi necessário para modelar o funcionamento de smartphones e sua interação com os usuários. Parte das propriedades do protocolo foram validadas, enquanto alguns problemas relativos a privacidade e clareza nas mensagens foram identificados. |
Abstract: | Security issues are one of the biggest internet banking challenges, as such systems are highly targeted by ciber criminals. Distinct security protocols were designed in order to provide reliability to online banking transactions. The Dynamic Authorization Protocol is an interesting approach, where a shared key is defined between the User and the Bank for use in future online banking transactions. For each transaction, the User is challenged to retrieve a unique transaction code, using a smartphone as a third-party validation entity, scanning a QR-code for integrity checks, for being able to carry operations in a untrusted computer. However, the protocol is not formally checked. In this work, we used the Inductive Method theory for formalizing and verifying the protocol and its properties. An extension to this theory was necessary in order to reason about the smartphones and their interaction with users. Some protocol properties were confirmed, although some issues with privacy and message clearness were identified. |
metadata.dc.description.unidade: | Instituto de Ciências Exatas (IE) Departamento de Ciência da Computação (IE CIC) |
Description: | Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2019. |
metadata.dc.description.ppg: | Programa de Pós-Graduação em Informática |
Licença:: | A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor com as seguintes condições: Na qualidade de titular dos direitos de autor da publicação, autorizo a Universidade de Brasília e o IBICT a disponibilizar por meio dos sites www.bce.unb.br, www.ibict.br, http://hercules.vtls.com/cgi-bin/ndltd/chameleon?lng=pt&skin=ndltd sem ressarcimento dos direitos autorais, de acordo com a Lei nº 9610/98, o texto integral da obra disponibilizada, conforme permissões assinaladas, para fins de leitura, impressão e/ou download, a título de divulgação da produção científica brasileira, a partir desta data. |
Collection(s) : | Teses, dissertações e produtos pós-doutorado |
Tous les documents dans DSpace sont protégés par copyright, avec tous droits réservés.