Definición
Un protocolo debe tener 3 caracteristicas:
- Sintaxis (¿Cómo se comunica?) Orden en que se agrupan los datos para formar el mensaje.
- Semántica (¿Qué se comunica?) Significado de cada parte del mensaje.
- Temporización (¿Cuándo se comunica?) Cuándo se debe enviar el mensaje.
En los protocolos de seguridad existen además 2 elementos importantes, cada uno con sis propieas caracteristicas:
- Mensaje:
- Confidencialidad
- Integridad
- Autenticación
- No repudio
- Entidades que se comunican:
- Realizan autenticación
Un protocolo de seguridad se compone habitualmente de dos partes:
- Criptográfica: que es el cifrado de los datos
- Lógica: que define la estructura y el orden de los mensajes.
Protocolos de seguridad y lógica de primer orden
La mayoría de las debilidades en un protocolo se encuentran en la parte lógica debido a que no es posible analizar todas las aplicaciónes que éste pueda tener, entonces las pruebas se limitan a suposiciones de cómo el protocolo será utilizado y bajo qué condiciones.
La lógica de primer orden permite realizar un análisis previo a la liberación del protocolo.
- Que el protocolo consigue sus objetivos (postcondiciones) cuando se ejecuta cada uno de los pasos especificados en el diseño (casos de uso del protocolo).
- Que no hay posibilidad de un ataque (es decir, no se puede usar el protocolo de forma fraudulenta).
Analicemos el caso del protocolo RSA, la parte criptográfica consiste en los siguientes pasos:
- Se eligen dos primos muy grandes p y q.
- Se calcula n = (p) (q), el cual será el módulo para cifrado y descifrado.
- Se calcula φn = (p − 1) (q − 1).
- Se elige un número aleatorio e y se calcula d, de forma que d = e-1 mod φn.
- La pareja de numeros (e, n) forman la clave pública.
- La pareja de números (d, n) forman la clave privada.
Los mensajes se cifran con (e, n) y sólo se puede descifrar con (d, n) y viceversa.
La seguridad del protocolo RSA depende del tamaño de n, ya que, dada la clave pública es posible obtener la clave privada factorizando n.
La parte lógica del protócolo, por ejemplo, trata las siguientes cuestiones:
- ¿Cómo saber si el usuario que dice ser Bob es realmente Bob?
- ¿Es suficiente utilizar una contraseña?
- ¿La contraseña debe ser cifrada con la clave pública del servidor?
- Analizar confidencialidad, integridad, autenticación, no repudio.
La exactitud del protocolo (que éste sea correcto) se analiza definiendo axiomas y reglas de inferencia comunes de la logica de primer orden y adicionalmente se agregan axiomas que represetan las caracteristicas y propiedades de seguridad que debe tener el protocolo. Mediante esta sintaxis es posible demostrar algunas de las propiedades de seguridad del protocolo directamente.
Estas pruebas logicas garantizan que las propiedades sean verdaderas y comprueba que el protocolo es robusto.
En éste protocolo cada mensaje se puede interpretar como una acción que modifica el estado de creencia de los individuos que intervienen en la comunicación
Se necesitan enviar 3 mensajes para establecer una comunicación segura, cuando se han enviado los tres mensajes cada uno de los agentes sabe que el otro es quien dice ser.
Las condiciones iniciales del protocolo son las siguientes:
Protocolo simétrico de Needham-Schroeder
En éste protocolo cada mensaje se puede interpretar como una acción que modifica el estado de creencia de los individuos que intervienen en la comunicación
Se necesitan enviar 3 mensajes para establecer una comunicación segura, cuando se han enviado los tres mensajes cada uno de los agentes sabe que el otro es quien dice ser.
Las condiciones iniciales del protocolo son las siguientes:
- S es un servidor confiado por ambas partes
- KAS es una clave simétrica que conocen sólo A y S
- KBS es una clave simétrica que conocen sólo B y S
- NA y NB son nonces (número, puede ser pseudoaleatorio, de un solo uso que se usa como un sencillo método adicional de autenticación).
Las propiedades del protocolo, utilizando la lógica de primer orden, se escriben de la siguiente forma:
- A → S : A,B,NA
- S → A : {NA, KAB, B, {KAB, A}KBS}KAS
- ==============================================
- A → B : {KAB, A}KBS
- B → A : {NB}KAB
- A → B : {NB-1}KAB
El protocolo se lee de la siguiente forma:
- Alice se comunica con el servidor, se identifica a si misma y a Bob y envía un nonce. (Solicta comunicarse con Bob)
- Servidor responde a Alice, genera la clave KAB y la envía a Alice junto con el nonce y la autenticación de Bob, además envía un paquete con la clave KAB y la autenticación de Alice, cifrado con la clave KBS (que solo Bob y el servidor conocen). La totalidad de la información esta cifrada con la clave que solo Alice y el servidor conocen.
Los tres mensajes de autenticación consisten en lo siguiente:
- Alice decifra la información, recupera el nonce (garantiza que la información corresponde a su sesión y que es reciente), la clave KAB y la autenticación de Bob. Como hay un paquete cifrado con KBS el paquete se envía a Bob para que también tenga su copia de la clave KAB. y de la autenticación de Alice.
- Bob responde a Alice con un nonce cifrado con KAB (clave que solo conocen Alice y Bob), con ello demuestra que recibio la clave.
- Alice responde a Bob con un nonce modificado (mediante una operación simple) cifrado con la clave , con ello demuestra que tiene la clave también.
Asi queda comprobado que Alice y Bob son quien dicen ser.
Protocolo de clave pública de Needham-Schroeder
Las condiciones iniciales para éste protocolo son:
- KPA y KSA claves pública y privada de Alice.
- KPB y KSB claves pública y privada de Bob.
- KPS y KSS claves pública y privada del servidor.
Utilizando lógica de primer orden, el protocolo se representa de la siguiente forma:
- A → S : A, B
- S → A : {KPB, B}KSS
- A → B : {NA, A}KPB
- B → S : B, A
- S → B : {KPA, A}KSS
- B → A : {NA, NB}KPA
- A → B : {NB}KPB
El protocolo se lee:
- Alice solicita al servidor la clave pública de Bob
- El servidor responde con la cláve pública de Bob y con si identidad, la información esta cifrada con la clave secreta del servidor.
- Alice conoce la clave pública del servidor, decripta la información y envía un nonce a Bob con su identidad, todo cifrado con la clave publica de Bob.
- B solicita al servidor la cláve pública de Alice.
- El servidor responde con la cláve pública de Alice y con si identidad, la información esta cifrada con la clave secreta del servidor.
- Bob genera otro nonce y lo envía a Alice junto con el nonce que recibio de Alice, la información va encriptada con la clave pública de Alice.
- Alice reponde a Bob con el nonce recibido NB, encriptado con la clave pública de Bob.
Al finalizar el protocolo, Alice y Bob estan seguros de ser quien decían ser.
Lógica de BAN
Es un método formal que permite difinir y analizar las propiedades de los protocolos. Fue
desarrollado con los aportes de Michael Burrows, Martin Abadi y Roger Needham.
Es una extensión de la lógica de primer orden que se basa en creencias de los agentes que participan en el protocolo.
Objetivo
Lógica de BAN intenta responder las siguientes preguntas:
- ¿Cuál es el objetivo del protocolo a analizar?
- ¿El protocolo necesita mas suposiciones que algún otro?
- ¿El protocolo realiza una acción innecesaria que puede eliminarse sin debilitarlo?
- ¿El protocolo encripta información que puede ser enviada en texto plano sin debilitarlo?
Limitaciones
La principal limitación es que siempre asume una criptografia perfecta:
- Los agentes nunca publican la información secreta, pero no se encarga de verificar que se cumpla.
- Los agentes reconocen los fallos, pero no verifica la ausencia de los mismos.
- Los agentes reconocen o ignoran mensajes enviados por ellos mismos.
- Los agentes son honestos.
- Agentes comprometidos no estan considerados
- Los atacantes no tienen claves válidas.
Sintaxis
- Identificadores para los agentes. (A, B, C, ...)
- Identificadores para las llaves. (k)
- Identificadores para funciones atomicas. (n)
- Conjunto de formulas. (X , Y, Z, ...)
Las formulas pueden ser expresadas por ejemplo: "A cree que k es una llave compartida entre A y B", y dan siempre como resultado verdad o falso.
Formulas
- P cree X: P tiene razones para creer que el mensaje X es verdad.
- P ve X: P puede ver el mensaje X y puede reproducirlo.
- P dijo X: En algún momento P envió el mensaje X.
- Fresco(X): El mensaje X pertenece al presente (sesión actual) y no ha sido utilizado antes.
- P controla X: P tiene pertenencia sobre X. (Tiene, controla, o conoce)
- P y Q comparten la llave K, K es buena para establecer comunicación entre ambos.
- P tiene la clave pública K
- X es un secreto solo y solo entre P y Q
- X combinada con la función Y.
- {X}K : X encriptada con la llave K
Algunos ejemplos donde se aplican las anteriores formulas son las siguientes formulas:
 |
P cree que la llave K esta compartida con Q. P vee que X esta encriptado con la llave pública K. Entonces P cree que Q dijo X. |
 |
P cree que Q tiene la llave publica K. P vee que X esta encriptado con la llave privada K-1. Entonces P cree que Q dijo X. |
 |
P cree que Y es un secreto entre él y Q. P vee que X se utiliza en la fórmula Y. Entonces P cree que Q dijo X |
 |
P cree que X fue mencionado recientemente. Q alguna vez dijo X. Entonces P cree que Q cree en X. |
 |
P cree que a Q le pertenece X. P cree que Q cree en X. Entonces P cree en X. |
Fuente: A Logic of Authentication
Protocolo Needham-Schroeder y Lógica de BAN
Como ejemplo, vamos a analizar el protocolo Needham-Schroeder (especificado más arriba) utilizando la lógica de BAN.
Recordando las condiciones iniciales:
KA y KA-1 claves pública y privada de Alice.
KB y KB-1 claves pública y privada de Bob.
KS y KS-1 claves pública y privada del servidor.
Las propiedades del protocolo quedarían de la siguiente forma:
Recordando las condiciones iniciales:
Las propiedades del protocolo quedarían de la siguiente forma:
| A cree que tiene la llave pública KA | B cree que tiene la llave pública KB |
| A cree que S tiene la llave pública KS | B cree que S tiene la llave pública KS |
| S cree que A tiene la llave pública KA | S cree que B tiene la llave pública KB |
| S cree que tiene la llave pública KS | |
| A cree que S conoce la llave de B | B cree que S conoce la llave de A |
| A cree que su nonce NA es reciente (fresco) | B cree que su nonce NB es reciente (fresco) |
| A cree que su nonce NA es un secreto entre él y B | B cree que su nonce NB es un secreto entre él y A |
| A cree que el mensaje con la llave pública de B, KB es reciente | B cree que el mensaje con la llave pública de A, KA es reciente |
En resumen, cada uno A y B tienen un par de llaves las cuales con conocidas por S. Los nonces son creados para esa sesión especifica y cada uno conoce su nonce. Ambos utilizan sus llaves públicas durante la sesión de comunicación.
Ahora, la debilidad del protocolo se encuentra justamente en las 2 ultimas creencias, a pesar de que son llaves públicas, A y B no conocen las llaves del otro hasta que cada uno la envía al otro, esto provoca que dicho mensaje no sea fresco, sino que pudo haber sido envíado por un tercero quien lo encripto previamente. Para solucionar este problema de agregan 4 creencias más:
| A cree que B tiene la llave pública KB | B cree que A tiene la llave pública KA |
| A cree que B cree que el nonce NA es un secreto entre ellos | B cree que A cree que el nonce NB es un secreto entre ellos |
Ahora, ambos confirman su llave pública mutuamente y además intercambian su nonce para asegurar que es fresco en ambos casos, ahora ambos creen que el otro dice la verdad por lo que pueden continuar el intercambio de información.
Referencias
- Wikipedia: Protocolo de Needham-Schroeder
- University of Cambridge Computer Laboratory: A Logic of Authentication
- BAN Logic: A Logic of Authentication by Sape J. Mullender
- Verification of Security Protocols Chapter 6: BAN Logic by Christian Haack
- Métodos formales para la verificación de protocolos: http://grupo.us.es/ghum609/php/system/files/fernando1.pdf
- Protocolos de seguridad: http://ldc.usb.ve/~poc/Seguridad/protocolos.pdf
Bien; 10.
ResponderEliminar