Explorador de ruido
Noise Explorer es un motor en línea para el razonamiento sobre los patrones de apretón de manos del marco de protocolo de ruido. La herramienta de línea de comandos del Explorador de ruido puede analizar patrones de apretón de manos de ruido de acuerdo con la especificación original. Puede generar modelos criptográficos para la verificación formal, incluidas consultas de seguridad, procesos de nivel superior y entidades de seguridad malintencionadas, para realizar pruebas contra un atacante activo o pasivo. Noise Explorer también puede generar implementaciones discretas totalmente funcionales para cualquier patrón de apretón de manos de ruido, escrito en los lenguajes de programación Go y Rust. Noise Explorer también puede representar los resultados de la salida ProVerif en un formato HTML elegante y fácil de leer: los resultados del patrón que se pueden explorar en el Explorador de ruido se generaron mediante la herramienta de línea de comandos de Noise Explorer. Noise Explorer le permite: Diseño de patrones de apretón de manos de ruido. Obtenga comprobaciones de validez que verifiquen si su diseño se ajusta a la especificación. Generar modelos de verificación formal. Genere instantáneamente modelos simbólicos completos en el cálculo pi aplicado para cualquier patrón de apretón de manos de ruido que introduzca. Usando ProVerif, estos modelos se pueden analizar contra atacantes pasivos y activos con entidades de seguridad maliciosas. El proceso de nivel superior del modelo y las consultas sofisticadas se generan específicamente para ser relevantes para su patrón de apretón de manos de ruido, incluidas pruebas de un fuerte frente al débil secreto hacia adelante y resistencia a la suplantación de compromiso clave. Explore un Compendio de Resultados de Verificación Formal. Dado que la verificación formal de los patrones complejos de apretón de manos de ruido puede tomar tiempo y requerir hardware de CPU rápido, Noise Explorer viene con un compendio que detalla los resultados completos de todos los patrones de apretón de manos de ruido descritos en la especificación original. Estos resultados se presentan con un modelo de seguridad que es aún más completo que la especificación original, ya que incluye la participación de un principal malicioso. Generar implementaciones de software seguras. Noise Explorer puede generar automáticamente una implementación segura del diseño de patrón de apretón de manos de ruido elegido, escrito en Go o Rust.
