Verification of the Dynamic Authorization Protocol
Autor(a)
Oliveira, Felipe Rodopoulos de
Orientador(a) Coorientador(a)
Nalon, Cláudia
Data de aceite
2020-05-15
Data de disponibilizacao
2020-05-15
Data de publicacao
2020-05-15
Data de defesa submissao
2019-07-26
Citacao
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.
Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2019.
Resumo Portugues
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.
Resumo Ingles
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.
Unidade academica
Instituto de Ciências Exatas (IE)
Departamento
Departamento de Ciência da Computação (IE CIC)
Programa de Pos-Graduacao
Programa de Pós-Graduação em Informática
Idioma
eng
Tipo de documento
Dissertação
Formato
application/pdf
Direitos de acesso
Acesso Aberto
Termo de licenca
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.
Palavras-chave
Internet banking||Protocolos de segurança||Formalização de protocolos||Transações bancárias||Prova de teoremas
