Reconstruindo intrusos passivos Dolev-Yao a partir de capturas de tráfego de vigilância
Pesquisadores apresentam uma metodologia automatizada para reconstruir, a partir de capturas PCAP, a execução de protocolos de rede sob o modelo de intruso passivo Dolev-Yao. O framework extrai objetos serializados em Java, remonta sessões concorrentes e valida as reconstruções contra uma especificação formal do protocolo (AnBx), atingindo mais de 94% de sucesso em capturas de sessão única e cerca de 89% em cenários com sessões paralelas.
O artigo parte de um problema concreto de forense de rede: sistemas de vigilância e captura de tráfego em larga escala armazenam volumes enormes de pacotes, mas um PCAP bruto revela muito pouco sobre a semântica do protocolo que gerou aquele tráfego. Sem uma camada de interpretação, o analista fica com bytes crus, incapaz de responder perguntas investigativas como "quais mensagens pertencem à mesma sessão" ou "o que um atacante passivo conseguiria inferir observando esse tráfego". Os autores propõem uma ferramenta que fecha essa lacuna de forma automatizada, usando como entrada a captura de pacotes, uma especificação formal do protocolo na linguagem AnBx e metadados sobre a implantação.
Tecnicamente, o pipeline resolve três problemas de reconstrução distintos. Primeiro, extrai objetos serializados em Java diretamente dos fluxos TCP, lidando com o caso em que múltiplos objetos e referências cruzadas aparecem dentro do mesmo stream. Segundo, resolve a ambiguidade de atribuir conexões de rede entrelaçadas a sessões de protocolo concorrentes, um problema combinatório quando há duas ou três sessões simultâneas na mesma captura. Terceiro, gera automaticamente, a partir da especificação AnBx, um "intruso passivo" formal nos moldes Dolev-Yao, que tenta derivar logicamente quais segredos ou mensagens seriam dedutíveis apenas observando o tráfego — e usa esse modelo para validar semanticamente se a reconstrução proposta é consistente.
Os números de avaliação são relevantes para quem pensa em aplicar isso como ferramenta forense: em 121 protocolos do conjunto de testes AnBx, a extração via provedor criptográfico padrão do JDK recuperou 97,8% dos objetos esperados em capturas de sessão única, com 94,2% de reconstruções totalmente limpas. Em cenários mais realistas, com 112 protocolos capazes de execução paralela e duas ou três sessões concorrentes, a taxa de sucesso cai para 89,3%, ainda recuperando cerca de 97,2% dos objetos — e os autores testaram deliberadamente mapeamentos de papel incorretos e traces mutados para confirmar que as verificações Dolev-Yao geradas reagem a inconsistências semânticas reais, e não apenas a erros de parsing.
Na prática, isso importa porque boa parte da análise forense de rede hoje depende de inspeção manual ou de parsers específicos de protocolo escritos à mão, que não escalam para novos protocolos nem oferecem garantias formais sobre o que foi reconstruído. Uma abordagem guiada por especificação formal, que produz tanto a reconstrução da sessão quanto uma validação criptográfica do que um observador passivo poderia ter aprendido, dá ao perito uma base mais rigorosa para avaliar exposição de dados em tráfego capturado e para fundamentar a escolha de contramedidas — por exemplo, decidir se um protocolo legado precisa de cifragem adicional em campos específicos observados em uma investigação real.