Un protocolo de seguridad ( protocolo criptográfico o protocolo de cifrado ) es un extracto o de hormigón protocolo que realiza una seguridad función -relacionados y aplica criptográficas métodos, a menudo como secuencias de primitivas criptográficas . Un protocolo describe cómo se deben utilizar los algoritmos . Un protocolo suficientemente detallado incluye detalles sobre estructuras y representaciones de datos, momento en el que se puede utilizar para implementar múltiples versiones interoperables de un programa. [1]
Los protocolos criptográficos se utilizan ampliamente para el transporte seguro de datos a nivel de aplicación. Un protocolo criptográfico suele incorporar al menos algunos de estos aspectos:
- Acuerdo o establecimiento clave
- Autenticación de entidad
- Construcción de material de autenticación de mensajes y cifrado simétrico
- Transporte de datos seguro a nivel de aplicación
- Métodos de no repudio
- Métodos secretos para compartir
- Computación multipartita segura
Por ejemplo, Transport Layer Security (TLS) es un protocolo criptográfico que se utiliza para proteger las conexiones web ( HTTPS ). Tiene un mecanismo de autenticación de entidades, basado en el sistema X.509 ; una fase de configuración de la clave, en la que se forma una clave de cifrado simétrica empleando criptografía de clave pública; y una función de transporte de datos a nivel de aplicación. Estos tres aspectos tienen importantes interconexiones. TLS estándar no tiene soporte de no repudio.
También existen otros tipos de protocolos criptográficos, e incluso el término en sí tiene varias lecturas; Los protocolos de aplicación criptográfica a menudo utilizan uno o más métodos de acuerdo de claves subyacentes , que a veces también se denominan "protocolos criptográficos". Por ejemplo, TLS emplea lo que se conoce como intercambio de claves Diffie-Hellman , que aunque es solo una parte de TLS per se , Diffie-Hellman puede verse como un protocolo criptográfico completo en sí mismo para otras aplicaciones.
Protocolos criptográficos avanzados
Una amplia variedad de protocolos criptográficos van más allá de los objetivos tradicionales de confidencialidad, integridad y autenticación de los datos para asegurar también una variedad de otras características deseadas de la colaboración mediada por computadora. [2] Las firmas ciegas se pueden utilizar para el efectivo digital y las credenciales digitales para demostrar que una persona posee un atributo o derecho sin revelar la identidad de esa persona o las identidades de las partes con las que realizó la transacción. La marca de tiempo digital segura se puede utilizar para demostrar que los datos (incluso si son confidenciales) existieron en un momento determinado. El cálculo seguro de varias partes se puede utilizar para calcular las respuestas (como determinar la oferta más alta en una subasta) basándose en datos confidenciales (como las ofertas privadas), de modo que cuando el protocolo esté completo, los participantes solo conozcan su propia entrada y la respuesta. Los sistemas de votación auditables de un extremo a otro brindan conjuntos de propiedades deseables de privacidad y auditabilidad para llevar a cabo el voto electrónico . Las firmas innegables incluyen protocolos interactivos que permiten al firmante probar una falsificación y limitar quién puede verificar la firma. El cifrado denegable aumenta el cifrado estándar al hacer imposible que un atacante demuestre matemáticamente la existencia de un mensaje de texto sin formato. Las mezclas digitales crean comunicaciones difíciles de rastrear.
Verificación formal
En ocasiones, los protocolos criptográficos pueden verificarse formalmente en un nivel abstracto. Cuando se hace, es necesario formalizar el entorno en el que opera el protocolo para identificar las amenazas. Esto se hace con frecuencia a través del modelo Dolev-Yao .
Lógicas, conceptos y cálculos utilizados para el razonamiento formal de los protocolos de seguridad:
- Lógica de Burrows-Abadi-Needham (lógica BAN)
- Modelo Dolev – Yao
- π-cálculo
- Lógica de composición de protocolo (PCL)
- Espacio de hebra [3]
Proyectos de investigación y herramientas utilizadas para la verificación formal de protocolos de seguridad:
- Validación automatizada de protocolos y aplicaciones de seguridad de Internet (AVISPA) [4] y proyecto de seguimiento AVANTSSAR [5]
- Casper [9]
- CryptoVerif
- Analizador de formas de protocolo criptográfico (CPSA) [10]
- Conocimientos en protocolos de seguridad (KISS) [11]
- Analizador de protocolo Maude-NRL (Maude-NPA) [12]
- ProVerif
- Scyther [13]
- Prueba Tamarin [14]
Noción de protocolo abstracto
Para verificar formalmente un protocolo, a menudo se abstrae y modela utilizando la notación Alice & Bob . Un ejemplo sencillo es el siguiente:
Esto dice que Alice tiene la intención de un mensaje para Bob que consiste en un mensaje cifrado bajo clave compartida .
Ejemplos de
- Intercambio de claves de Internet
- IPsec
- Kerberos
- Mensajería no registrada
- Protocolo punto a punto
- Shell seguro (SSH)
- Protocolo de señal
- Transport Layer Security
- ZRTP
Ver también
- Canal seguro
- Repositorio abierto de protocolos de seguridad
Referencias
- ^ "Descripción general del protocolo criptográfico" (PDF) . 2015-10-23. Archivado desde el original (PDF) el 29 de agosto de 2017 . Consultado el 23 de octubre de 2015 .
- ^ Berry Schoenmakers. "Protocolos criptográficos de las notas de la conferencia" (PDF) .
- ^ Fábrega, F. Javier Thayer, Jonathan C. Herzog y Joshua D. Guttman., Strand Spaces: ¿Por qué es correcto un protocolo de seguridad?CS1 maint: varios nombres: lista de autores ( enlace )
- ^ "Validación automatizada de protocolos y aplicaciones de seguridad de Internet (AVISPA)" . Archivado desde el original el 22 de septiembre de 2016 . Consultado el 7 de octubre de 2016 .
- ^ AVANTSSAR
- ^ Buscador de ataques basado en lógica de restricción (Cl-AtSe)
- ^ Verificador de modelos de punto fijo de código abierto (OFMC)
- ^ "Model-Checker basado en SAT para protocolos de seguridad y aplicaciones sensibles a la seguridad (SATMC)" . Archivado desde el original el 3 de octubre de 2015 . Consultado el 17 de octubre de 2016 .
- ^ Casper: un compilador para el análisis de protocolos de seguridad
- ^ cpsa: analizador de protocolo criptográfico simbólico
- ^ "Conocimientos en protocolos de seguridad (KISS)" . Archivado desde el original el 10 de octubre de 2016 . Consultado el 7 de octubre de 2016 .
- ^ Analizador de protocolo Maude-NRL (Maude-NPA)
- ^ Scyther
- ^ Prueba Tamarin
Otras lecturas
- Ermoshina, Ksenia; Musiani, Francesca; Halpin, Harry (septiembre de 2016). "Protocolos de mensajería cifrada de extremo a extremo: descripción general" (PDF) . En Bagnoli, Franco; et al. (eds.). Ciencias de Internet . INSCI 2016. Florencia, Italia: Springer. págs. 244-254. doi : 10.1007 / 978-3-319-45982-0_22 . ISBN 978-3-319-45982-0.CS1 maint: ref duplica el valor predeterminado ( enlace )
enlaces externos
- Repositorio abierto de protocolos seguros