Hispanopedia Wiki
Articulo de referencia

Verificación profesional

ProVerif es una herramienta de software para el razonamiento automático sobre las propiedades de seguridad de los protocolos criptográficos . La herramienta ha sido desarrollada...

Hispanopedia WikiContenido en espanolLectura gratuita

ProVerif es una herramienta de software para el razonamiento automático sobre las propiedades de seguridad de los protocolos criptográficos . La herramienta ha sido desarrollada por Bruno Blanchet y otros.

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 de firma. La herramienta es capaz de evaluar propiedades de accesibilidad, afirmaciones de correspondencia y equivalencia observacional . Estas capacidades de razonamiento son particularmente útiles para el dominio de la seguridad informática, ya que permiten el análisis de propiedades de secreto y autenticación. También se pueden considerar propiedades emergentes como privacidad, trazabilidad y 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 reconstruir ataques: cuando no se puede probar una propiedad, se construye un rastro de ejecución que falsifica la propiedad deseada.

Aplicabilidad de ProVerif

ProVerif se ha utilizado en los siguientes estudios de caso, que incluyen el análisis de seguridad de protocolos de red reales:

  • Abadi y Blanchet [2] utilizaron afirmaciones de correspondencia para verificar el protocolo de correo electrónico certificado. [3]
  • Abadi, Blanchet y Fournet [4] analizan el protocolo Just Fast Keying [5] , que era uno de los candidatos a sustituir a Internet Key Exchange (IKE) como protocolo de intercambio de claves en IPsec , combinando pruebas manuales con pruebas de correspondencia y equivalencia ProVerif.
  • Blanchet y Chaudhuri [6] estudiaron la integridad del sistema de archivos Plutus [7] en un almacenamiento no confiable, utilizando afirmaciones de correspondencia, lo que resultó en el descubrimiento y posterior reparación de debilidades en el sistema inicial.
  • Bhargavan et al. [8] [9] [10] utilizan ProVerif para analizar implementaciones de protocolos criptográficos escritos en F# ; en particular, se ha estudiado de esta manera el protocolo Transport Layer Security (TLS).
  • Chen y Ryan [11] evaluaron los protocolos de autenticación que se encuentran en el Módulo de Plataforma Confiable (TPM), un chip de hardware ampliamente implementado, y descubrieron vulnerabilidades .
  • Delaune, Kremer y Ryan [12] [13] y Backes, Hritcu y Maffei [14] formalizan y analizan las propiedades de privacidad de la votación electrónica utilizando equivalencia observacional.
  • Delaune, Ryan y Smyth [15] y Backes, Maffei y Unruh [16] analizan las propiedades de anonimato del esquema de computación confiable Direct Anonymous Attestation (DAA) utilizando equivalencia observacional.
  • Kusters y Truderung [17] [18] examinan protocolos con exponenciación Diffie-Hellman y XOR .
  • Smyth, Ryan, Kremer y Kourjieh [19] formalizan y analizan las propiedades de verificabilidad para la votación electrónica utilizando la accesibilidad.
  • Google [20] verificó su protocolo de capa de transporte ALTS .
  • Sardar et al. [21] [22] verificaron los protocolos de certificació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 afirmaciones de accesibilidad y correspondencia), KISS (para equivalencia estática), YAPA (para equivalencia estática). CryptoVerif para la verificación de la seguridad contra adversarios de tiempo polinomial en el modelo computacional. Tamarin Prover es una alternativa moderna a ProVerif, con excelente soporte para razonamiento ecuacional de Diffie-Hellman y verificación de propiedades de equivalencia observacional.

Referencias

  1. ^ Nueva versión: ProVerif 2.04 - Comunidad - OCaml
  2. ^ Abadi, Martín; Blanchet, Bruno (2005). "Verificación asistida por ordenador de un protocolo para correo electrónico certificado". Science of Computer Programming . 58 (1–2): 3–27. doi : 10.1016/j.scico.2005.02.002 .
  3. ^ Abadi, Martín; Glew, Neal (2002). "Correo electrónico certificado con un tercero de confianza en línea". Actas de la 11.ª conferencia internacional sobre la World Wide Web . WWW '02. Nueva York, NY, EE. UU.: ACM. pp. 387–395. doi :10.1145/511446.511497. ISBN 978-1581134490.S2CID 9035150  .
  4. ^ Abadi, Martín; Blanchet, Bruno; Fournet, Cédric (julio de 2007). "Simplemente tecleando rápidamente en el cálculo Pi". ACM Transactions on Information and System Security . 10 (3): 9–es. CiteSeerX 10.1.1.3.3762 . doi :10.1145/1266977.1266978. ISSN  1094-9224. S2CID  2371806. 
  5. ^ Aiello, William; Bellovin, Steven M.; Blaze, Matt; Canetti, Ran; Ioannidis, John; Keromytis, Angelos D.; Reingold, Omer (mayo de 2004). "Simplemente codificación rápida: acuerdo de claves en una red interna hostil". ACM Transactions on Information and System Security . 7 (2): 242–273. doi :10.1145/996943.996946. ISSN  1094-9224. S2CID  14442788.
  6. ^ Blanchet, B.; Chaudhuri, A. (mayo de 2008). "Análisis formal automatizado de un protocolo para compartir archivos de forma segura en almacenamiento no confiable". Simposio IEEE sobre seguridad y privacidad de 2008 (Sp 2008) . págs. 417–431. CiteSeerX 10.1.1.362.4343 . doi :10.1109/SP.2008.12. ISBN.  978-0-7695-3168-7.S2CID6736116  .​
  7. ^ Kallahalla, Mahesh; Riedel, Erik; Swaminathan, Ram; Wang, Qian; Fu, Kevin (2003). "Plutus: intercambio seguro y escalable de archivos en almacenamiento no confiable". Actas de la 2.ª Conferencia USENIX sobre tecnologías de archivos y almacenamiento . FAST '03: 29–42.
  8. ^ 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 clase en informática. Vol. 4184. Springer, Berlín, Heidelberg. págs. 88–106. CiteSeerX 10.1.1.61.3389 . doi :10.1007/11841197_6. ISBN .  9783540388623.
  9. ^ Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Swamy, Nikhil (2008). "Implementaciones verificadas del protocolo de gestión de identidad federada de tarjetas 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. Número de identificación del sujeto  6821014.
  10. ^ Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Tse, Stephen (diciembre de 2008). "Implementaciones interoperables verificadas de protocolos de seguridad". ACM Transactions on Programming Languages ​​and Systems . 31 (1): 5:1–5:61. CiteSeerX 10.1.1.187.9727 . doi :10.1145/1452044.1452049. ISSN  0164-0925. S2CID  14018835. 
  11. ^ 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 de la seguridad y la confianza . Apuntes de clase sobre informática. Vol. 5983. 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.
  12. ^ Delaune, Stéphanie; Kremer, Steve; Ryan, Mark (1 de enero de 2009). "Verificación de propiedades de tipo privacidad de protocolos de votación electrónica". Journal of Computer Security . 17 (4): 435–487. CiteSeerX 10.1.1.142.1731 . doi :10.3233/jcs-2009-0340. ISSN  0926-227X. 
  13. ^ Kremer, Steve; Ryan, Mark (4 de abril de 2005). "Análisis de un protocolo de votación electrónica en el cálculo Pi aplicado". Lenguajes y sistemas de programación . Apuntes de clase en informática. Vol. 3444. Springer, Berlín, Heidelberg. págs. 186–200. doi :10.1007/978-3-540-31987-0_14. ISBN . 9783540254355.
  14. ^ Backes, M.; Hritcu, C.; Maffei, M. (junio de 2008). "Verificación automática de protocolos de votación electrónica remota en el cálculo Pi aplicado". 21.° Simposio sobre fundamentos de seguridad informática del IEEE de 2008. págs. 195–209. CiteSeerX 10.1.1.612.2408 . doi :10.1109/CSF.2008.26. ISBN .  978-0-7695-3182-3.S2CID15189878  .​
  15. ^ Delaune, Stéphanie; Ryan, Mark; Smyth, Ben (18 de junio de 2008). "Verificación automática de propiedades de privacidad en el cálculo pi aplicado". Gestión de confianza II . IFIP – Federación Internacional para el Procesamiento de la Información. Vol. 263. Springer, Boston, MA. págs. 263–278. doi :10.1007/978-0-387-09428-1_17. ISBN . 9780387094274.
  16. ^ Backes, M.; Maffei, M.; Unruh, D. (mayo de 2008). "Conocimiento cero en el cálculo Pi aplicado y verificación automatizada del protocolo de atestación anónima directa". Simposio IEEE sobre seguridad y privacidad de 2008 (Sp 2008) . págs. 202–215. CiteSeerX 10.1.1.463.489 . doi :10.1109/SP.2008.23. ISBN .  978-0-7695-3168-7. Número de identificación del sujeto  651680.
  17. ^ Küsters, R.; Truderung, T. (julio de 2009). "Uso de ProVerif para analizar protocolos con exponenciación Diffie-Hellman". 22.º Simposio IEEE sobre fundamentos de seguridad informática de 2009. págs. 157-171. CiteSeerX 10.1.1.667.7130 . doi :10.1109/CSF.2009.17. ISBN.  978-0-7695-3712-2. Número de identificación del S2C:  14185888.
  18. ^ Küsters, Ralf; Truderung, Tomasz (1 de abril de 2011). "Reducción del análisis de protocolos con XOR al caso libre de XOR en el enfoque basado en la teoría de Horn". Journal of Automated Reasoning . 46 (3–4): 325–352. arXiv : 0808.0634 . doi :10.1007/s10817-010-9188-8. ISSN  0168-7433. S2CID  7597742.
  19. ^ Kremer, Steve; Ryan, Mark; Smyth, Ben (20 de septiembre de 2010). "Verificabilidad de elecciones en protocolos de votación electrónica". Seguridad informática – ESORICS 2010. Apuntes de clase sobre informática. Vol. 6345. 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.
  20. ^ "Seguridad de transporte de la capa de aplicación | Documentación". Google Cloud .
  21. ^ Sardar, Muhammad Usama; Quoc, Do Le; Fetzer, Christof (agosto de 2020). "Hacia la formalización de la certificación remota basada en identificación de privacidad mejorada (EPID) en Intel SGX". 2020 23.ª Conferencia Euromicro sobre diseño de sistemas digitales (DSD) . Kranj, Eslovenia: IEEE. págs. 604–607. doi :10.1109/DSD51259.2020.00099. ISBN . 978-1-7281-9535-3.S2CID222297511  .​
  22. ^ Sardar, Muhammad Usama; Faqeh, Rasha; Fetzer, Christof (2020). "Fundamentos formales para las primitivas de atestación de centros de datos Intel SGX". En Lin, Shang-Wei; Hou, Zhe; Mahony, Brendan (eds.). Métodos formales e ingeniería de software . Apuntes de clase en informática. Vol. 12531. Cham: Springer International Publishing. págs. 268–283. doi :10.1007/978-3-030-63406-3_16. ISBN 978-3-030-63406-3. Número de identificación del sujeto  229344923.
  • Sitio web oficial
Obtenido de "https://es.wikipedia.org/w/index.php?title=ProVerif&oldid=1206933627"