Actualmente es innegable la importancia de los medios electrónicos en las aplicaciones comerciales. Bajo este contexto, es vital asegurar que la información transmitida no haya sido comprometida por agentes maliciosos. Existen numerosas primitivas criptográficas que ayudan a proteger información sensible, la cual se transmite en secuencias ordenadas de mensajes denominadas protocolos de seguridad. Presentamos una extensión que permite detectar ataques del tipo type flaw a un modelo en lógica de primer orden del protocolo y un algoritmo de resolución que permite de forma totalmente automática detectar dichos ataques sin limitar el número de sesiones del protocolo.