Análisis del protocolo de establecimiento de TLS
Como parte de una asignatura hemos tenido que analizar el establecimiento de sesión del protcolo TLS, es decir el TLS Handshake Protocol. En este post voy a dar una visión del funcionamiento de este protocolo haciendo uso de narraciones informales de una versión algo simplificada del protocolo.
Supondremos que tenemos dos partes implicadas en el protocolo, A y B (de Alice y Bob ), y una autoridad de certificación CA, cuya clave pública es conocida bajo Kca. Con esto, el establecimiento de una sesión TLS mediante la cual se negocia una clave vendría a ser algo como:
A -> B: A, Na, emptyId
B -> A: Nb, Sid
B -> A: {|B, KB |}Kca^-1
A -> B*: {|A, KA |}Kca^-1
A generates a random PMS (Pre Master Secret)
A begins ClientAuth(A, PMS)*
A -> B: {|PMS|}Kb
B begins ServerAuth(B, PMS)
A -> B*: {|#(Nb, B, PMS)|}Ka^-1
B ends ClientAuth(A, PMS)*
A and B generate:
M = PRF(PMS, Na, Nb), finished = #(M, Sid, Na, Nb, A, B).
A -> B: {finished}ClientK(Na,Nb,M)
B -> A: {finished}ServerK(Na,Nb,M)
A ends ServerAuth(B, PMS)
Donde {|m|}k significa cifrar el mensaje m con la clave k mediante criptografía asimétrica. Por tanto, cuando usamos kb estamos cifrando, mientras que si usamos kb^-1 estamos usando la clave privada y por tanto firmando. Además, #(m) significa un hash criptográfico del mensaje m, y {m}k significa cifrar m mediante la clave simétrica k.
Como se puede observar, el cliente inicia la sesión enviando un nonce y un identificador de sesión vacío. Un nonce es un número aleatorio con el objetivo de garantizar la frescura de la sesión y de la clave generada por ésta. Además, aunque lo he obviado aquí, se envían preferencias de cifrado con las opciones que soporta el cliente para el cifrado asimétrico, simétrico y el hashing.
El servidor responde con un nuevo nonce y un nuevo identificador de sesión. Además también añade sus preferencias criptográficas, que son seleccionadas en base a las del cliente y determinan los algoritmos usados en la sesión. Como ya he dicho, se ha obviado y asumismo que están de acuerdo (o que solo existe una posible opción).
Seguidamente el servidor manda su certificado ( es decir, su identidad y clave pública firmadas por la autoridad de certificación), y el cliente opcionalmente el suyo (el * significa opcional). Después el cliente envía PMS cifrado con la clave pública del servidor; el pre master secret (PMS), que es una cadena aleatoria de 48 bits, se supone secreto y compartido entre ambas partes, y será la base para generar la nueva clave de sesión.
Tras esto, si el cliente mandó su certificado (si se requería autenticación del cliente) se manda un hash de algunos elementos recibidos firmados con su clave privada, para que el servidor pueda verificar su identidad.
Seguidamente, ambas partes crean un nuevo Master secret, M, con una función pseudoaleatoria en base a los nonces y el PMS. Además, crean finished como un hash de todos los mensajes anteriores e intercambian el valor de finished mediante las nuevas claves para ver que ambos han llegado al mismo resultado.
Como se puede ver, se utilizan dos claves distintas para servidor y cliente. Además se generan dos claves para usarlas en códigos de autenticación de mensajes que no se muestran aquí ya que no se han usado. Todas las claves se generan en base al PMS y los nonces. De esta forma, todas las partes pueden influenciar de la misma manera la clave, y una sola parte no es capaz de predeterminar una clave concreta.
Los begin y ends son lo que llamamos aserciones de correspondencia (traducido on-the-fly de correspondence assertions 😆 ). Sirven para especificar objetivos de autenticación al analizar el protocolo, y se debe probar que para que ocurra la finalización del evento ( end xxx(a,b,c) ) debe haber ocurrido antes un begin xxx(a,b,c). De esta forma, cuando el servidor hace "B begins ServerAuth(B, PMS)", se inicia una sesión de autenticación del servidor ante el cliente. Cuando el cliente puede asumir que está hablando con el servidor B, entonces puede hacer el end correspondiente. Si se consigue que ocurra un end antes que su correspondiente start significa que de alguna forma un atacante ha hecho que el cliente asuma que está hablando con el servidor de confianza mientras que éste no ha iniciado la sesión.
Por último, el protocolo permite resumir una sesión simplemente reusando un identificador de sesión en el primer mensaje en lugar de mandar el identificador nulo. En este caso, la narración queda así
A -> B: A, Na, Sid
B -> A: Nb, Sid
A and B generate: PMS is looked up in a database
M = PRF(PMS, Na, Nb), finished = #(M, Sid, Na, Nb, A, B).
A -> B: {finished}ClientK(Na,Nb,M)
B -> A: {finished}ServerK(Na,Nb,M)
Como se puede ver, lo único que se obtiene de la sesión anterior es el PMS, mientras que M es generado de nuevo con los nuevos nonces. De esta forma, se crean nuevas claves que serán presumiblemente seguras incluso si las anteriores han podido ser obtenidas, siempre que PMS haya permanecido secreto.
Esto es todo de momento, a ver si puedo poner nuestro modelo de ProVerif de este protocolo para que veáis más o menos cómo funciona... pero primero esperaré a tener la corrección del profesor ;-). Si algo no está bien explicado o no queda claro de este post, no dudéis en decirlo en los comentarios 🙂