Desmascarando Vulnerabilidades: Uma Investigação Formal sobre o Impacto dos Fatores Humanos no Model Context Protocol

Abstract

Garantir a segurança de assistentes de Inteligência Artificial que executam ações em nome do operador torna-se um desafio complexo quando se considera apenas a robustez criptográfica do protocolo subjacente, sem atender às decisões humanas que autorizam descoberta de servidores e execução de ferramentas. A adoção do Model Context Protocol (MCP), padrão aberto para conectar modelos de linguagem a sistemas externos, amplia essa superfície de ataque à medida que a IA deixa de ser um oráculo passivo e passa a agir de forma integrada no fluxo de trabalho do usuário. A análise tradicional de protocolos costuma modelar participantes apenas como honestos ou maliciosos, o que dificulta capturar falhas que emergem da interação humano-computador, em que modelos mentais imprecisos induzem autorizações inseguras mesmo na ausência de quebra criptográfica. Para abordar esse problema, a literatura de Cerimônias de Segurança propõe tratar o operador humano como participante da cerimônia, e as Máscaras Pirandellianas permitem discretizar perfis comportamentais plausíveis dentro de uma verificação formal. O objetivo deste trabalho é investigar a segurança do MCP sob essa perspectiva sociotécnica, empregando o Tamarin Prover para integrar a máquina de estados do protocolo à dinâmica variável de seus operadores. A metodologia modela descoberta de servidores e aprovação de ações sob três perfis (Attentive, Busy e Careless), submete os cenários aos vetores de Namespace Typosquatting e Indirect Prompt Injection e organiza a verificação em fase baseline, para obtenção de contraexemplos, e fase mitigada, com registro de servidores e fricção contextual na interface. Os resultados mostram que perfis desatentos violam propriedades de integridade na descoberta e na execução, enquanto intervenções estruturais restauram as garantias desejadas sem presumir comportamento perfeito do operador. O trabalho oferece base analítica reprodutível para antecipar vulnerabilidades em sistemas de IA agênticos e orientar o desenho de interações que harmonizem segurança e usabilidade.

Ensuring the security of Artificial Intelligence assistants that execute actions on behalf of the operator becomes a complex challenge when only the cryptographic robustness of the underlying protocol is considered, without accounting for the human decisions that authorize server discovery and tool execution. The adoption of the Model Context Protocol (MCP), an open standard for connecting language models to external systems, expands this attack surface as AI ceases to be a passive oracle and becomes integrated into the user’s workflow. Traditional protocol analysis typically models participants as merely honest or malicious, which makes it difficult to capture failures that emerge from human-computer interaction, where imprecise mental models induce insecure authorizations even in the absence of cryptographic compromise. To address this problem, the Security Ceremonies literature proposes treating the human operator as a ceremony participant, and Pirandellian Masks enable discretizing plausible behavioral profiles within formal verification. The objective of this work is to investigate MCP security from this sociotechnical perspective, employing the Tamarin Prover to integrate the protocol’s state machine with the variable dynamics of its operators. The methodology models server discovery and action approval under three profiles (Attentive, Busy, and Careless), subjects the scenarios to Namespace Typosquatting and Indirect Prompt Injection attack vectors, and organizes verification into a baseline phase for obtaining counterexamples and a mitigated phase with server registration and contextual friction in the interface. The results show that inattentive profiles violate integrity properties during discovery and execution, while structural interventions restore the desired guarantees without assuming perfect operator behavior. This work provides a reproducible analytical basis for anticipating vulnerabilities in agentic AI systems and guiding the design of interactions that harmonize security and usability.