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

Abstract

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.