ProVerif es una herramienta de software para el razonamiento automatizado sobre las propiedades de seguridad que se encuentran en los protocolos criptográficos . La herramienta ha sido desarrollada por Bruno Blanchet.
Desarrollador (es) | Bruno Blanchet |
---|---|
Versión inicial | 1 de junio de 2002 |
Lanzamiento estable | 2.02pl1 / 2 de septiembre de 2020 |
Escrito en | OCaml |
Disponible en | inglés |
Licencia | Principalmente GNU GPL ; Binarios de Windows, licencias BSD |
Sitio web | prosecco |
Se proporciona soporte para primitivas criptográficas que incluyen: criptografía simétrica y asimétrica; firmas digitales; funciones hash; compromiso de bits; y pruebas de conocimiento firmadas. La herramienta es capaz de evaluar las propiedades de accesibilidad, las afirmaciones de correspondencia y la equivalencia observacional . Estas capacidades de razonamiento son particularmente útiles para el dominio de la seguridad informática, ya que permiten el análisis de las propiedades de confidencialidad y autenticación. También se pueden considerar propiedades emergentes como la privacidad, la trazabilidad y la verificabilidad. El análisis de protocolo se considera con respecto a un número ilimitado de sesiones y un espacio de mensajes ilimitado. La herramienta es capaz de atacar la reconstrucción: cuando una propiedad no puede probarse, se construye un rastro de ejecución que falsifica la propiedad deseada.
Aplicabilidad de ProVerif
ProVerif se ha utilizado en los siguientes casos de estudio, que incluyen el análisis de seguridad de protocolos de red reales:
- Abadi & Blanchet [1] utilizaron afirmaciones de correspondencia para verificar el protocolo de correo electrónico certificado. [2]
- Abadi, Blanchet & Fournet [3] analizan el protocolo Just Fast Keying [4] , que fue uno de los candidatos para reemplazar Internet Key Exchange (IKE) como protocolo de intercambio de claves en IPsec , combinando pruebas manuales con pruebas de correspondencia ProVerif y equivalencia.
- Blanchet & Chaudhuri [5] estudiaron la integridad del sistema de archivos Plutus [6] en el almacenamiento no confiable, utilizando aserciones de correspondencia, lo que resultó en el descubrimiento y subsiguiente corrección de debilidades en el sistema inicial.
- Bhargavan y col. [7] [8] [9] utilizan ProVerif para analizar implementaciones de protocolos criptográficos escritos en F Sharp (lenguaje de programación) ; en particular, el protocolo Transport Layer Security (TLS) se ha estudiado de esta manera.
- Chen & Ryan [10] han evaluado los protocolos de autenticación que se encuentran en el Módulo de plataforma segura (TPM), un chip de hardware ampliamente implementado, y han descubierto vulnerabilidades.
- Delaune, Kremer & Ryan [11] [12] y Backes, Hritcu & Maffei [13] formalizan y analizan las propiedades de privacidad para el voto electrónico utilizando la equivalencia observacional.
- Delaune, Ryan & Smyth [14] y Backes, Maffei & Unruh [15] analizan las propiedades de anonimato del esquema de computación confiable Direct Anonymous Attestation (DAA) utilizando equivalencia observacional.
- Kusters & Truderung [16] [17] examinan protocolos con exponenciación Diffie-Hellman y XOR .
- Smyth, Ryan, Kremer & Kourjieh [18] formalizan y analizan las propiedades de verificabilidad para el voto electrónico utilizando la accesibilidad.
- Google [19] verificó su protocolo de capa de transporte ALTS .
- Sardar y col. [20] [21] verificó los protocolos de atestación remota en Intel SGX .
Se pueden encontrar más ejemplos en línea: [1] .
Alternativas
Las herramientas de análisis alternativas incluyen: AVISPA (para aseveraciones de accesibilidad y correspondencia), KISS (para equivalencia estática), YAPA (para equivalencia estática). CryptoVerif para verificación de seguridad contra adversarios de tiempo polinomial en el modelo computacional. El Tamarin demostrador es una alternativa moderna a ProVerif, con un excelente soporte para Diffie-Hellman razonamiento ecuacional, y la verificación de las propiedades de equivalencia de observación.
Referencias
- ↑ Abadi, Martín; Blanchet, Bruno (2005). "Verificación asistida por ordenador de un protocolo para correo electrónico certificado". Ciencia de la Programación de Computadores . 58 (1–2): 3–27. doi : 10.1016 / j.scico.2005.02.002 .
- ^ Abadi, Martín; Glew, Neal (2002). Correo electrónico certificado con un tercero de confianza en línea ligero: diseño e implementación . Actas de la XI Conferencia Internacional sobre la World Wide Web . WWW '02. Nueva York, NY, EE.UU .: ACM. págs. 387–395. doi : 10.1145 / 511446.511497 . ISBN 978-1581134490.
- ^ Abadi, Martín; Blanchet, Bruno; Fournet, Cédric (julio de 2007). "Simplemente Teclado rápido en el cálculo de Pi". Transacciones ACM sobre seguridad de la información y del sistema . 10 (3): 9 – es. CiteSeerX 10.1.1.3.3762 . doi : 10.1145 / 1266977.1266978 . ISSN 1094-9224 .
- ^ Aiello, William; Bellovin, Steven M .; Blaze, Matt; Canetti, Ran; Ioannidis, John; Keromytis, Angelos D .; Reingold, Omer (mayo de 2004). "Teclado rápido: acuerdo clave en un interno hostil". Transacciones ACM sobre seguridad de la información y del sistema . 7 (2): 242–273. doi : 10.1145 / 996943.996946 . ISSN 1094-9224 .
- ^ Blanchet, B .; Chaudhuri, A. (mayo de 2008). Análisis formal automatizado de un protocolo para el intercambio seguro de archivos en almacenamiento que no es de confianza . Simposio IEEE 2008 sobre seguridad y privacidad (Sp 2008) . págs. 417–431. CiteSeerX 10.1.1.362.4343 . doi : 10.1109 / SP.2008.12 . ISBN 978-0-7695-3168-7.
- ^ Kallahalla, Mahesh; Riedel, Erik; Swaminathan, Ram; Wang, Qian; Fu, Kevin (2003). "Plutus: intercambio seguro escalable de archivos en almacenamiento que no es de confianza" . Actas de la 2ª Conferencia de USENIX sobre tecnologías de archivos y almacenamiento . FAST '03: 29–42.
- ^ Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D. (8 de septiembre de 2006). Implementaciones de referencia verificadas de protocolos WS-Security . Servicios web y métodos formales . Apuntes de conferencias en Ciencias de la Computación. Springer, Berlín, Heidelberg. págs. 88-106. CiteSeerX 10.1.1.61.3389 . doi : 10.1007 / 11841197_6 . ISBN 9783540388623.
- ^ Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D .; Swamy, Nikhil (2008). Implementaciones verificadas del Protocolo de gestión de identidad federada de la tarjeta de información . Actas del Simposio ACM de 2008 sobre seguridad de la información, las computadoras y las comunicaciones . ASIACCS '08. Nueva York, NY, EE.UU .: ACM. págs. 123-135. doi : 10.1145 / 1368310.1368330 . ISBN 9781595939791.
- ^ Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D .; Tse, Stephen (diciembre de 2008). "Implementaciones interoperables verificadas de protocolos de seguridad". Transacciones ACM sobre lenguajes y sistemas de programación . 31 (1): 5: 1–5: 61. CiteSeerX 10.1.1.187.9727 . doi : 10.1145 / 1452044.1452049 . ISSN 0164-0925 .
- ^ Chen, Liqun; Ryan, Mark (5 de noviembre de 2009). Ataque, solución y verificación de datos de autorización compartidos en TCG TPM . Aspectos formales en seguridad y confianza . Apuntes de conferencias en Ciencias de la Computación. Springer, Berlín, Heidelberg. págs. 201–216. CiteSeerX 10.1.1.158.2073 . doi : 10.1007 / 978-3-642-12459-4_15 . ISBN 9783642124587.
- ^ Delaune, Stéphanie; Kremer, Steve; Ryan, Mark (1 de enero de 2009). "Verificación de las propiedades de tipo privacidad de los protocolos de votación electrónica". Revista de seguridad informática . 17 (4): 435–487. CiteSeerX 10.1.1.142.1731 . doi : 10.3233 / jcs-2009-0340 . ISSN 0926-227X .
- ^ Kremer, Steve; Ryan, Mark (4 de abril de 2005). Análisis de un protocolo de votación electrónica en el cálculo de pi aplicado . Sistemas y lenguajes de programación . Apuntes de conferencias en Ciencias de la Computación. Springer, Berlín, Heidelberg. págs. 186-200. doi : 10.1007 / 978-3-540-31987-0_14 . ISBN 9783540254355.
- ^ Backes, M .; Hritcu, C .; Maffei, M. (junio de 2008). Verificación automatizada de protocolos de votación electrónica remota en el cálculo de pi aplicado . 2008 21º Simposio de Fundamentos de Seguridad Informática del IEEE . págs. 195–209. CiteSeerX 10.1.1.612.2408 . doi : 10.1109 / CSF.2008.26 . ISBN 978-0-7695-3182-3.
- ^ Delaune, Stéphanie; Ryan, Mark; Smyth, Ben (18 de junio de 2008). Verificación automática de propiedades de privacidad en el cálculo de pi aplicado . Gestión de la confianza II . IFIP - Federación Internacional para el Procesamiento de la Información. Springer, Boston, MA. págs. 263-278. doi : 10.1007 / 978-0-387-09428-1_17 . ISBN 9780387094274.
- ^ Backes, M .; Maffei, M .; Unruh, D. (mayo de 2008). Cero conocimiento en el cálculo de Pi aplicado y verificación automatizada del protocolo de atestación directa anónima . Simposio IEEE 2008 sobre seguridad y privacidad (Sp 2008) . págs. 202–215. CiteSeerX 10.1.1.463.489 . doi : 10.1109 / SP.2008.23 . ISBN 978-0-7695-3168-7.
- ^ Küsters, R .; Truderung, T. (julio de 2009). Uso de ProVerif para analizar protocolos con exponenciación Diffie-Hellman . 2009 22º Simposio de Fundamentos de Seguridad Informática del IEEE . págs. 157-171. CiteSeerX 10.1.1.667.7130 . doi : 10.1109 / CSF.2009.17 . ISBN 978-0-7695-3712-2.
- ^ Küsters, Ralf; Truderung, Tomasz (1 de abril de 2011). "Reducir el análisis de protocolo con XOR al caso libre de XOR en el enfoque basado en la teoría de Horn". Revista de razonamiento automatizado . 46 (3–4): 325–352. arXiv : 0808.0634 . doi : 10.1007 / s10817-010-9188-8 . ISSN 0168-7433 .
- ^ Kremer, Steve; Ryan, Mark; Smyth, Ben (20 de septiembre de 2010). Verificabilidad electoral en protocolos de votación electrónica . Seguridad informática - ESORICS 2010 . Apuntes de conferencias en Ciencias de la Computación. Springer, Berlín, Heidelberg. págs. 389–404. CiteSeerX 10.1.1.388.2984 . doi : 10.1007 / 978-3-642-15497-3_24 . ISBN 9783642154966.
- ^ "Seguridad de transporte de la capa de aplicación | Documentación" . Google Cloud .
- ^ Sardar, Muhammad Usama; Quoc, Do Le; Fetzer, Christof (agosto de 2020). "Hacia la formalización de la atestación remota basada en la identificación de privacidad mejorada (EPID) en Intel SGX" . 2020 23a Conferencia Euromicro sobre Diseño de Sistemas Digitales (DSD) . Kranj, Eslovenia: IEEE: 604–607. doi : 10.1109 / DSD51259.2020.00099 . ISBN 978-1-7281-9535-3.
- ^ Sardar, Muhammad Usama; Faqeh, Rasha; Fetzer, Christof (2020). Lin, Shang-Wei; Hou, Zhe; Mahony, Brendan (eds.). "Fundamentos formales para primitivas de atestación del centro de datos Intel SGX" . Métodos formales e ingeniería de software . Apuntes de conferencias en Ciencias de la Computación. Cham: Springer International Publishing. 12531 : 268-283. doi : 10.1007 / 978-3-030-63406-3_16 . ISBN 978-3-030-63406-3.
enlaces externos
- Página web oficial