Utilização de traços simbólicos e SMT solvers para a verificação de equivalência observacional em segurança e Privacidade de protocolos

• Ano de defesa: 2020
• Autor(a) principal: Carvalho, Abraão Aires Urquiza de
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal da Paraíba; Brasil; Informática; Programa de Pós-Graduação em Informática; UFPB
• Palavras-chave em Português: Equivalência observacional; Verificação automática de protocolos de segurança; Análise de tráfego; Ataque de temporização; Observacional equivalence; Automated verification of security protocols; Traffic analysis; Timing attack; CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO
• Link de acesso: https://repositorio.ufpb.br/jspui/handle/123456789/20956

Attackers and malicious users have at their disposal several techniques to acquire sensitive information. Among them, timing attacks and traffic analysis generate a number of security breaches. The automated verification of this attacks is not as straightforward as usual reachability properties, due to the nature of the problem. Instead of having an inherently bad state, i.e., a state where an intruder possess secret intel, the attacker compares two distincts configurations. The attack happens when one of the configurations presents a behavior that distinguish it from the other configuration. This work proposes a formal definition based on trace equivalence for automated verification of observacional equivalence of time and traffic. This definition could be used in the development of a system capable of automated verification of security and privacy breaches in security protocols. Furthermore, we present a prototype of such system and presents the implementation of some examples as proof-of-concept.