Para desarrollar sistemas distribuidos confiables, se han empleado técnicas de verificación y métodos formales, incluyendo enfoques ligeros y prácticos, para certificar el diseño o implementación de protocolos de seguridad. Los métodos formales ligeros ofrecen una alternativa más accesible a las técnicas tradicionales completamente formalizadas al centrarse en modelos simplificados y soporte de herramientas, lo que los hace más aplicables en entornos prácticos. Las ventajas técnicas de la verificación formal sobre las pruebas manuales son cada vez más reconocidas en la comunidad de ciberseguridad. Sin embargo, aplicar métodos formales, incluso en sus formas más prácticas, fuera de entornos de investigación altamente especializados sigue siendo un desafío. Para los profesionales, el modelado y la verificación formales a menudo son demasiado complejos y poco familiares para ser utilizados de manera rutinaria. En este artículo, presentamos un Entorno de Desarrollo Integrado de Eclipse para el diseño, verificación e implementación de protocolos de seguridad y evaluamos su efectividad, incluyendo la retroalimentación de los usuarios en entornos educativos. Ofrece asistencia amigable en el proceso de formalización como parte de un enfoque de Desarrollo Dirigido por Modelos. Este IDE se centra en la notación de Alice & Bob (AnB), el Compilador y Generador de Código AnBx, el verificador de modelos OFMC y el verificador de protocolos criptográficos ProVerif. Para la evaluación, identificamos los seis factores limitantes más prominentes para la adopción de métodos formales, basados en la literatura relevante en este campo, y consideramos la efectividad del IDE frente a esos criterios. Además, realizamos una encuesta estructurada para recopilar la retroalimentación de estudiantes universitarios que han utilizado el conjunto de herramientas para sus proyectos. Los hallazgos demuestran que esta contribución es valiosa como ayuda en el flujo de trabajo y ayuda a los usuarios a comprender conceptos esenciales de ciberseguridad, incluso para aquellos con conocimientos limitados de métodos formales o criptografía. Crucialmente, los usuarios informaron que el IDE ha sido un componente importante para completar sus proyectos y que lo volverían a utilizar en el futuro, si se les da la oportunidad.