Protocolo criptográfico
| Protocolo criptográfico | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|
| |||||||||||
| |||||||||||
| Wikidata | |||||||||||
Un protocolo criptográfico é un protocolo abstracto ou concreto que realiza unha función relacionada coa seguridade e aplica métodos criptográficos, a miúdo como secuencias de primitivas criptográficas. Un protocolo describe como se deben usar os algoritmos e inclúe detalles sobre estruturas de datos e representacións, o que permite implementar múltiples versións interoperables dun programa.[1]
Os protocolos criptográficos empréganse amplamente para o transporte seguro de datos no nivel de aplicación. Un protocolo criptográfico adoita incorporar polo menos algúns destes aspectos:
- Establecemento de chaves, incluído o acordo de chaves
- Autenticación de entidades, talvez usando un protocolo de autenticación
- Construción de material de chaves para cifraxe simétrica e autenticación de mensaxes
- Transporte seguro de datos no nivel de aplicación
- Métodos de non repudio
- Métodos de compartición de segredos
- Computación multipartita segura
Transport Layer Security (TLS) é un exemplo de protocolo que protexe as conexións web HTTPS. A negociación inicial establece os parámetros e o material de chaves co que se protexe o tráfico posterior. TLS 1.3 admite autenticación con certificados e modalidades con chaves precompartidas; estas últimas poden combinarse con Diffie–Hellman. Polo tanto, non todas as configuracións usan certificados X.509 nin o mesmo mecanismo de establecemento de chaves.[2]
Un protocolo de aplicación pode incorporar outros protocolos criptográficos. Por exemplo, TLS pode empregar Diffie–Hellman para acordar material de chaves, pero tamén require autenticación, protección da negociación e regras para o transporte posterior dos datos.[2]
Protocolos criptográficos avanzados
[editar | editar a fonte]Os protocolos criptográficos tamén poden protexer outras propiedades dunha colaboración. As sinaturas cegas utilízanse na construción de sistemas de diñeiro electrónico e credenciais anónimas. O selado dixital de tempo permite acreditar que uns datos existían nun momento determinado. A computación multipartita segura procura que as partes non aprendan información das entradas alleas alén da que se deduce da súa propia entrada e do resultado autorizado. Os sistemas de votación auditables combinan propiedades de privacidade e verificación; as sinaturas innegables incorporan protocolos interactivos de verificación e desmentido.[3]
A cifraxe negable permite presentar información alternativa compatible cun texto cifrado baixo unha situación de coacción. Non se define como ocultar a existencia da comunicación cifrada, senón como poder atribuírlla a outro texto en claro.[4] Os retransmisores anónimos procuran dificultar o rastrexo das comunicacións.
Verificación formal
[editar | editar a fonte]Os protocolos criptográficos poden ás veces verificarse formalmente nun nivel abstracto. Cando se fai, cómpre formalizar o contorno no que opera o protocolo para identificar ameazas. Isto faise con frecuencia mediante o modelo Dolev-Yao.
Algúns formalismos usados para o razoamento formal dos protocolos de seguridade:
- Lóxica de Burrows-Abadi-Needham (lóxica BAN)
- Modelo Dolev-Yao
- Cálculo pi
- Lóxica de composición de protocolos (PCL)
- O formalismo strand spaces, que representa secuencias de emisión e recepción de mensaxes.[5]
Algúns proxectos de investigación e ferramentas usados para a verificación formal dos protocolos de seguridade:
- Automated Validation of Internet Security Protocols and Applications (AVISPA) e o proxecto de continuación AVANTSSAR.[6][7]
- Casper[11]
- CryptoVerif
- Cryptographic Protocol Shapes Analyzer (CPSA)[12]
- Knowledge In Security protocolS (KISS)[13]
- Maude-NRL Protocol Analyzer (Maude-NPA)[14]
- ProVerif
- Scyther[15]
- Tamarin Prover[16]
- Squirrel[17]
- StrandsRocq[18]
Noción de protocolo abstracto
[editar | editar a fonte]- Artigo principal: Notación de protocolos de seguridade.
Para verificar formalmente un protocolo adoita abstraerse e modelarse usando a notación de Alice e Bob. Un exemplo simple é o seguinte:
Esta notación indica que Alice envía a Bob a mensaxe cifrada coa chave compartida .
Exemplos
[editar | editar a fonte]Notas
[editar | editar a fonte]Todas as referencias en inglés agás cando se indique o contrario.
- ↑ "Cryptographic Protocol Overview" (PDF) (en inglés). Arquivado dende o orixinal (PDF) o 29 de agosto de 2017. Consultado o 23 de outubro de 2015.
- 1 2 Eric Rescorla (agosto de 2018). "The Transport Layer Security (TLS) Protocol Version 1.3" (en inglés). IETF. RFC 8446. Consultado o 14 de setembro de 2026.
- ↑ Berry Schoenmakers. "Lecture Notes Cryptographic Protocols" (PDF) (en inglés).
- ↑ Ran Canetti; Cynthia Dwork; Moni Naor; Rafail Ostrovsky. "Deniable Encryption" (en inglés). Consultado o 14 de setembro de 2026.
- ↑ F. Javier Thayer Fábrega; Jonathan C. Herzog; Joshua D. Guttman (1998). "Strand Spaces: Why is a Security Protocol Correct?". Proceedings of the 1998 IEEE Symposium on Security and Privacy (en inglés). IEEE. pp. 160–171. doi:10.1109/SECPRI.1998.674832.
- ↑ "Automated Validation of Internet Security Protocols and Applications (AVISPA)" (en inglés). Arquivado dende o orixinal o 22 de setembro de 2016. Consultado o 14 de febreiro de 2024.
- ↑ Armando, A.; Arsac, W.; Avanesov, T.; Barletta, M.; Calvi, A.; Cappai, A.; Carbone, R.; Chevalier, Y. (2012). "The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures". En Flanagan, C.; König, B. Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science (en inglés) 7214. Springer. pp. 267–282. doi:10.1007/978-3-642-28756-5_19. Consultado o 14 de febreiro de 2024.
- ↑ "Constraint Logic-based Attack Searcher (Cl-AtSe)" (en inglés). Arquivado dende o orixinal o 8 de febreiro de 2017. Consultado o 17 de outubro de 2016.
- ↑ Open-Source Fixed-Point Model-Checker (OFMC)
- ↑ "SAT-based Model-Checker for Security Protocols and Security-sensitive Application (SATMC)" (en inglés). Arquivado dende o orixinal o 3 de outubro de 2015. Consultado o 17 de outubro de 2016.
- ↑ Casper: A Compiler for the Analysis of Security Protocols
- ↑ cpsa: Symbolic cryptographic protocol analyzer
- ↑ "Knowledge In Security protocolS (KISS)" (en inglés). Arquivado dende o orixinal o 10 de outubro de 2016. Consultado o 7 de outubro de 2016.
- ↑ Maude-NRL Protocol Analyzer (Maude-NPA)
- ↑ Scyther
- ↑ Tamarin Prover
- ↑ Squirrel Prover
- ↑ StrandsRocq
Véxase tamén
[editar | editar a fonte]Bibliografía
[editar | editar a fonte]- Ermoshina, Ksenia; Musiani, Francesca; Halpin, Harry (setembro de 2016). Bagnoli, Franco; et al., eds. End-to-End Encrypted Messaging Protocols: An Overview (PDF). Internet Science, INSCI 2016 (en inglés). Florencia, Italia: Springer. pp. 244–254. ISBN 978-3-319-45982-0. doi:10.1007/978-3-319-45982-0_22.
