Análise formal encontra falhas em quatro protocolos de pagamento para agentes de IA
Pesquisadores formalizaram em Tamarin quatro protocolos emergentes de pagamento para agentes de IA (x402, MPP, ACP e AP2) e, a partir de 86 casos de verificação, encontraram 40 achados de inconsistência formal não documentados anteriormente, além de reproduzir 46 problemas já conhecidos. Dez desses achados foram validados com provas de conceito em implementações reais do x402.
Protocolos de pagamento para agentes são a camada de transação que está surgindo para permitir que agentes de IA comprem bens e serviços e executem pagamentos em nome de usuários. Diferente de fluxos de pagamento convencionais, eles distribuem intenção do usuário, autoridade delegada, uso de credenciais, liquidação e cumprimento entre múltiplos atores e etapas — criando dependências de segurança que nenhuma mensagem ou participante isolado consegue garantir sozinho.
Os autores modelaram quatro protocolos representativos (x402, MPP, ACP e AP2) usando uma abstração comum do ciclo de vida de pagamento por agente, com modelos fundamentados nas especificações originais, capturando papéis, estado, suposições de confiança e transições de cada protocolo. Em vez de assumir uma taxonomia de propriedades completa de antemão, eles usaram perguntas de verificação ancoradas nas fontes e contraexemplos gerados pelo Tamarin para expor vínculos ausentes, restrições de estado faltantes e correspondências entre etapas que não eram garantidas — consolidando tudo em 18 princípios de segurança compartilhados entre os quatro protocolos.
Dos 86 casos de verificação, 46 reproduziram problemas já conhecidos ou usados como calibração, mas 40 são achados de inconsistência formal inéditos. Para cada violação, os pesquisadores isolaram a relação de protocolo que faltava, construíram um modelo de referência minimamente reforçado e reverificaram a propriedade pretendida — metodologia que não apenas aponta o problema, mas indica a correção mínima necessária. Dez achados representativos sobre o x402 foram validados em três implementações reais, com provas de conceito em nível de SDK e esquema, cobrindo cinco dos princípios de segurança identificados.
O resultado prático central é que a autorização delegada precisa permanecer consistente com seus efeitos econômicos e de serviço resultantes em todos os atores, estados e etapas do protocolo — algo que as especificações atuais deixam implícito. Isso importa porque protocolos de pagamento por agente ainda estão em estágio inicial de adoção; achar essas lacunas agora, antes de uso em produção em larga escala, é significativamente mais barato do que corrigi-las depois que dinheiro real já estiver fluindo por essas implementações.