Verification of the Dynamic Authorization Protocol
Saved in:
| 主要作者: | |
|---|---|
| Publication Date: | 2019 |
| 格式: | Master thesis |
| 語言: | eng |
| Source: | Repositório Institucional da UnB |
| Download full: | https://repositorio.unb.br/handle/10482/37764 |
總結: | Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2019. |
| _version_ | 1871442483358990336 |
|---|---|
| author | Oliveira, Felipe Rodopoulos de |
| author_browse | Oliveira, Felipe Rodopoulos de |
| author_facet | Oliveira, Felipe Rodopoulos de |
| author_role | author |
| bitstream.checksum.fl_str_mv | d72d9610470d71835eb52e98abe7da14 bacfee268cc5d4f6aaa2e6e0066d38f5 |
| bitstream.checksumAlgorithm.fl_str_mv | MD5 MD5 |
| bitstream.url.fl_str_mv | http://repositorio.unb.br/bitstream/10482/37764/1/2019_FelipeRodopoulosdeOliveira.pdf http://repositorio.unb.br/bitstream/10482/37764/2/license.txt |
| collection | Repositório Institucional da UnB |
| contributor_str_mv | Nalon, Cláudia |
| dc.contributor.advisor1.fl_str_mv | Nalon, Cláudia |
| dc.contributor.author.fl_str_mv | Oliveira, Felipe Rodopoulos de |
| dc.date.accessioned.fl_str_mv | 2020-05-15T19:35:22Z |
| dc.date.available.fl_str_mv | 2020-05-15T19:35:22Z |
| dc.date.issued.fl_str_mv | 2020-05-15 |
| dc.date.submitted.none.fl_str_mv | 2019-07-26 |
| dc.identifier.citation.fl_str_mv | 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. |
| dc.identifier.uri.fl_str_mv | https://repositorio.unb.br/handle/10482/37764 |
| dc.language.iso.fl_str_mv | eng |
| dc.rights.driver.fl_str_mv | info:eu-repo/semantics/openAccess |
| dc.source.none.fl_str_mv | reponame:Repositório Institucional da UnB instname:Universidade de Brasília (UnB) instacron:UNB |
| dc.subject.keyword.pt_BR.fl_str_mv | Internet banking Protocolos de segurança Formalização de protocolos Transações bancárias Prova de teoremas |
| dc.title.pt_BR.fl_str_mv | Verification of the Dynamic Authorization Protocol |
| dc.type.driver.fl_str_mv | info:eu-repo/semantics/masterThesis |
| dc.type.status.fl_str_mv | info:eu-repo/semantics/publishedVersion |
| description | Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2019. |
| eu_rights_str_mv | openAccess |
| format | masterThesis |
| id | UNB_c0f490913aeee142d79befaf00a61dba |
| identifier_str_mv | 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. |
| instacron_str | UNB |
| institution | UNB |
| instname_str | Universidade de Brasília (UnB) |
| language | eng |
| network_acronym_str | UNB |
| network_name_str | Repositório Institucional da UnB |
| oai_identifier_str | oai:repositorio.unb.br:10482/37764 |
| publishDate | 2019 |
| publishDateSort | 2019 |
| reponame_str | Repositório Institucional da UnB |
| repository.mail.fl_str_mv | repositorio@unb.br |
| repository.name.fl_str_mv | Repositório Institucional da UnB - Universidade de Brasília (UnB) |
| repository_id_str | |
| spelling | Oliveira, Felipe Rodopoulos deNalon, Cláudia2020-05-15T19:35:22Z2020-05-15T19:35:22Z2020-05-152019-07-26OLIVEIRA, 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.https://repositorio.unb.br/handle/10482/37764Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2019.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.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.Instituto de Ciências Exatas (IE)Departamento de Ciência da Computação (IE CIC)Programa de Pós-Graduação em InformáticaengA 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.info:eu-repo/semantics/openAccessVerification of the Dynamic Authorization Protocolinfo:eu-repo/semantics/publishedVersioninfo:eu-repo/semantics/masterThesisInternet bankingProtocolos de segurançaFormalização de protocolosTransações bancáriasProva de teoremasreponame:Repositório Institucional da UnBinstname:Universidade de Brasília (UnB)instacron:UNBORIGINAL2019_FelipeRodopoulosdeOliveira.pdf2019_FelipeRodopoulosdeOliveira.pdfapplication/pdf732579http://repositorio.unb.br/bitstream/10482/37764/1/2019_FelipeRodopoulosdeOliveira.pdfd72d9610470d71835eb52e98abe7da14MD51open accessLICENSElicense.txtlicense.txttext/plain671http://repositorio.unb.br/bitstream/10482/37764/2/license.txtbacfee268cc5d4f6aaa2e6e0066d38f5MD52open access10482/377642025-12-26 17:09:30.966open accessoai:repositorio.unb.br:10482/37764QSBjb25jZXNzw6NvIGRhIGxpY2Vuw6dhIGRlc3RlIGl0ZW0gcmVmZXJlLXNlIGFvIHRlcm1vIGRlIGF1dG9yaXphw6fDo28gaW1wcmVzc28gYXNzaW5hZG8gDQpwZWxvIGF1dG9yIGNvbSBhcyBzZWd1aW50ZXMgY29uZGnDp8O1ZXM6DQoNCk5hIHF1YWxpZGFkZSBkZSB0aXR1bGFyIGRvcyBkaXJlaXRvcyBkZSBhdXRvciBkYSBwdWJsaWNhw6fDo28sIGF1dG9yaXpvIGEgVW5pdmVyc2lkYWRlIGRlIEJyYXPDrWxpYQ0KIGUgbyBJQklDVCBhIGRpc3BvbmliaWxpemFyIHBvciBtZWlvIGRvcyBzaXRlcyB3d3cuYmNlLnVuYi5iciwgd3d3LmliaWN0LmJyLA0KIGh0dHA6Ly9oZXJjdWxlcy52dGxzLmNvbS9jZ2ktYmluL25kbHRkL2NoYW1lbGVvbj9sbmc9cHQmc2tpbj1uZGx0ZCBzZW0gcmVzc2FyY2ltZW50byBkb3MgDQpkaXJlaXRvcyBhdXRvcmFpcywgZGUgYWNvcmRvIGNvbSBhIExlaSBuwrogOTYxMC85OCwgbyB0ZXh0byBpbnRlZ3JhbCBkYSBvYnJhIGRpc3BvbmliaWxpemFkYSwNCiBjb25mb3JtZSBwZXJtaXNzw7VlcyBhc3NpbmFsYWRhcywgcGFyYSBmaW5zIGRlIGxlaXR1cmEsIGltcHJlc3PDo28gZS9vdSBkb3dubG9hZCwgYSB0w610dWxvIGRlIA0KZGl2dWxnYcOnw6NvIGRhIHByb2R1w6fDo28gY2llbnTDrWZpY2EgYnJhc2lsZWlyYSwgYSBwYXJ0aXIgZGVzdGEgZGF0YS4=Repositório InstitucionalPUBhttps://repositorio.unb.br/oai/requestrepositorio@unb.bropendoar:2025-12-26T20:09:30Repositório Institucional da UnB - Universidade de Brasília (UnB) |
| spellingShingle | Verification of the Dynamic Authorization Protocol Oliveira, Felipe Rodopoulos de Internet banking Protocolos de segurança Formalização de protocolos Transações bancárias Prova de teoremas |
| status_str | publishedVersion |
| title | Verification of the Dynamic Authorization Protocol |
| title_full | Verification of the Dynamic Authorization Protocol |
| title_fullStr | Verification of the Dynamic Authorization Protocol |
| title_full_unstemmed | Verification of the Dynamic Authorization Protocol |
| title_short | Verification of the Dynamic Authorization Protocol |
| title_sort | Verification of the Dynamic Authorization Protocol |
| topic | Internet banking Protocolos de segurança Formalização de protocolos Transações bancárias Prova de teoremas |
| url | https://repositorio.unb.br/handle/10482/37764 |