Un protocolo criptográfico es un protocolo abstracto o concreto que realiza una función relacionada con la seguridad y aplica métodos criptográficos , a menudo como secuencias de primitivas criptográficas . Un protocolo describe cómo se deben utilizar los algoritmos e incluye detalles sobre las 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 cifrado simétrico y autenticación de mensajes
- Transporte seguro de datos a nivel de aplicación
- Métodos de no repudio
- Métodos para compartir secretos
- Computación segura entre múltiples partes
Por ejemplo, Transport Layer Security (TLS) es un protocolo criptográfico que se utiliza para proteger las conexiones web ( HTTPS ). [2] Tiene un mecanismo de autenticación de entidades, basado en el sistema X.509 ; una fase de configuración de clave, donde 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 interconexiones importantes. TLS estándar no tiene soporte de no repudio.
Existen otros tipos de protocolos criptográficos, e incluso el término en sí tiene varias lecturas; los protocolos de aplicaciones criptográficas 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 en sí , 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 datos para asegurar también una variedad de otras características deseadas de la colaboración mediada por computadora. [3] Las firmas ciegas se pueden utilizar para dinero digital y 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 esa persona realizó transacciones. El sellado de tiempo digital seguro se puede utilizar para demostrar que los datos (incluso si son confidenciales) existían en un momento determinado. El cálculo multipartidario seguro se puede utilizar para calcular respuestas (como determinar la oferta más alta en una subasta) en función de datos confidenciales (como 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 extremo a extremo proporcionan conjuntos de propiedades deseables de privacidad y auditabilidad para realizar votaciones electrónicas . Las firmas innegables incluyen protocolos interactivos que permiten al firmante demostrar una falsificación y limitar quién puede verificar la firma. El cifrado denegable mejora el cifrado estándar al hacer imposible que un atacante pruebe matemáticamente la existencia de un mensaje de texto simple. Las mezclas digitales crean comunicaciones difíciles de rastrear.
Verificación formal
En ocasiones, los protocolos criptográficos pueden verificarse formalmente a un nivel abstracto. Cuando esto se hace, es necesario formalizar el entorno en el que opera el protocolo para identificar amenazas. Esto se hace con frecuencia mediante el modelo Dolev-Yao .
Lógicas, conceptos y cálculos utilizados para el razonamiento formal de 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 hebras [4]
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 en Internet (AVISPA) y proyecto de seguimiento AVANTSSAR. [5] [6]
- Buscador de ataques basado en lógica de restricciones (CL-AtSe) [7]
- Comprobador de modelos de punto fijo de código abierto (OFMC) [8]
- Comprobador de modelos basado en SAT (SATMC) [9]
- Casper [10]
- Verificación de criptomonedas
- Analizador de formas de protocolo criptográfico (CPSA) [11]
- Conocimiento en protocolos de seguridad (KISS) [12]
- Analizador de protocolo Maude-NRL (Maude-NPA) [13]
- Verificación profesional
- Guadaña [14]
- Probador de tamarinos [15]
Noción de protocolo abstracto
Para verificar formalmente un protocolo, se suele abstraer y modelar utilizando la notación Alice & Bob . Un ejemplo sencillo es el siguiente:
Esto indica que Alice desea enviar un mensaje a Bob que consiste en un mensaje cifrado bajo una clave compartida .
Ejemplos
- Intercambio de claves por Internet
- IPsec
- Kerberos
- Mensajería extraoficial
- Protocolo punto a punto
- Shell seguro (SSH)
- Protocolo de señal
- Seguridad de la capa de transporte
- ZRTP
Véase también
- Lista de criptosistemas
- Canal seguro
- Repositorio abierto de protocolos de seguridad
- Comparación de bibliotecas de criptografía
Referencias
- ^ "Descripción general del protocolo criptográfico" (PDF) . 23 de octubre de 2015. Archivado desde el original (PDF) el 29 de agosto de 2017. Consultado el 23 de octubre de 2015 .
- ^ Chen, Shan; Jero, Samuel; Jagielski, Mateo; Boldyreva, Alexandra; Nita-Rotaru, Cristina (01/07/2021). "Establecimiento de canal de comunicación seguro: TLS 1.3 (sobre TCP Fast Open) versus QUIC". Revista de criptología . 34 (3): 26. doi : 10.1007/s00145-021-09389-w . ISSN 0933-2790. S2CID 235174220.
- ^ Berry Schoenmakers. "Notas de clase sobre protocolos criptográficos" (PDF) .
- ^ Fábrega, F. Javier Thayer, Jonathan C. Herzog y Joshua D. Guttman., Strand Spaces: ¿Por qué es correcto un protocolo de seguridad?
{{citation}}: CS1 maint: multiple names: authors list (link) - ^ "Validación automatizada de protocolos y aplicaciones de seguridad en Internet (AVISPA)". Archivado desde el original el 22 de septiembre de 2016 . Consultado el 14 de febrero de 2024 .
- ^ Armando, A.; Arsac, W; Avanesov, T.; Barletta, M.; Calvi, A.; Cappai, A.; Carbone, R.; Chevalier, Y.; +12 más (2012). Flanagan, C.; König, B. (eds.). La plataforma AVANTSSAR para la validación automatizada de la confianza y la seguridad de las arquitecturas orientadas a servicios. Vol. 7214. LNTCS. págs. doi :10.1007/978-3-642-28756-5_19 . Consultado el 14 de febrero de 2024 .
{{cite book}}: CS1 maint: numeric names: authors list (link) - ^ "Buscador de ataques basado en lógica de restricciones (Cl-AtSe)". Archivado desde el original el 8 de febrero de 2017. Consultado el 17 de octubre de 2016 .
- ^ Comprobador de modelos de punto fijo de código abierto (OFMC)
- ^ "Comprobador de modelos basado en SAT para protocolos de seguridad y aplicaciones sensibles a la seguridad (SATMC)". Archivado desde el original el 2015-10-03 . Consultado el 2016-10-17 .
- ^ Casper: Un compilador para el análisis de protocolos de seguridad
- ^ cpsa: Analizador de protocolos criptográficos simbólicos
- ^ "Conocimiento 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)
- ^ Guadaña
- ^ Probador de tamarinos
Lectura adicional
- Ermoshina, Ksenia; Musiani, Francesca; Halpin, Harry (septiembre de 2016). "Protocolos de mensajería cifrada de extremo a extremo: una descripción general" (PDF) . En Bagnoli, Franco; et al. (eds.). Internet Science . INSCI 2016. Florencia, Italia: Springer. pp. 244–254. doi :10.1007/978-3-319-45982-0_22. ISBN . 978-3-319-45982-0.