La lógica Burrows-Abadi-Needham (también conocida como lógica BAN ) es un conjunto de reglas para definir y analizar protocolos de intercambio de información. En concreto, la lógica BAN ayuda a sus usuarios a determinar si la información intercambiada es fiable, está protegida contra escuchas no autorizadas o ambas cosas. La lógica BAN parte de la suposición de que todos los intercambios de información se producen en medios vulnerables a la manipulación y al control público. Esto ha evolucionado hasta convertirse en el popular mantra de seguridad: "No confíes en la red".
Una secuencia lógica BAN típica incluye tres pasos: [1]
La lógica BAN utiliza postulados y definiciones (como todos los sistemas axiomáticos ) para analizar los protocolos de autenticación . El uso de la lógica BAN suele acompañar la formulación de la notación de un protocolo de seguridad y, a veces, se incluye en artículos.
La lógica BAN y las lógicas de la misma familia son decidibles : existe un algoritmo que toma hipótesis BAN y una conclusión propuesta, y que responde si la conclusión es o no derivable de las hipótesis. Los algoritmos propuestos utilizan una variante de los conjuntos mágicos . [2]
La lógica BAN inspiró muchos otros formalismos similares, como la lógica GNY. Algunos de ellos intentan reparar una debilidad de la lógica BAN: la falta de una buena semántica con un significado claro en términos de conocimiento y universos posibles. Sin embargo, a partir de mediados de la década de 1990, los protocolos criptográficos se analizaron en modelos operacionales (asumiendo una criptografía perfecta) utilizando verificadores de modelos, y se encontraron numerosos errores en protocolos que se "verificaron" con la lógica BAN y formalismos relacionados. [ cita requerida ] En algunos casos, se razonó que un protocolo era seguro según el análisis BAN, pero en realidad era inseguro. [3] Esto ha llevado al abandono de las lógicas de la familia BAN en favor de métodos de prueba basados en el razonamiento de invariancia estándar. [ cita requerida ]
Las definiciones y sus implicaciones se encuentran a continuación ( P y Q son agentes de red, X es un mensaje y K es una clave de cifrado ):
El significado de estas definiciones se recoge en una serie de postulados:
P debe creer que X es reciente. Si no se sabe si X es reciente, entonces podría tratarse de un mensaje obsoleto, reproducido por un atacante.
Con esta notación se pueden formalizar los supuestos en los que se basa un protocolo de autenticación. Mediante los postulados se puede demostrar que ciertos agentes creen que pueden comunicarse utilizando determinadas claves. Si la prueba falla, el punto de fallo suele indicar un ataque que compromete el protocolo.
Un protocolo muy simple –el protocolo Wide Mouth Frog– permite que dos agentes, A y B , establezcan comunicaciones seguras, utilizando un servidor de autenticación confiable, S, y relojes sincronizados en todas partes. Utilizando la notación estándar, el protocolo se puede especificar de la siguiente manera:
Los agentes A y B están equipados con claves K AS y K BS , respectivamente, para comunicarse de forma segura con S. Por lo tanto, tenemos las siguientes suposiciones:
El agente A desea iniciar una conversación segura con B. Por lo tanto , inventa una clave, K AB , que utilizará para comunicarse con B. A cree que esta clave es segura, ya que la ha creado él mismo:
B está dispuesto a aceptar esta clave, siempre que esté seguro de que proviene de A :
Además, B está dispuesto a confiar en que S le transmita con precisión las claves de A :
Es decir, si B cree que S cree que A quiere usar una clave particular para comunicarse con B , entonces B confiará en S y también lo creerá.
El objetivo es tener
A lee el reloj, obtiene la hora actual t , y envía el siguiente mensaje:
Es decir, envía su clave de sesión elegida y la hora actual a S , cifrada con su clave de servidor de autenticación privada K AS .
Dado que S cree que key( K AS , A ↔ S ) , y S ve { t , key( K AB , A ↔ B )} K AS , entonces S concluye que A en realidad dijo { t , key( K AB , A ↔ B )} . (En particular, S cree que el mensaje no fue inventado por algún atacante).
Dado que los relojes están sincronizados, podemos asumir
Dado que S cree que fresh( t ) y S cree que A dijo { t , key( K AB , A ↔ B )} , S cree que A realmente cree que key( K AB , A ↔ B ) . (En particular, S cree que el mensaje no fue reproducido por algún atacante que lo capturó en algún momento en el pasado).
S luego envía la clave a B :
Como el mensaje 2 está cifrado con K BS , y B cree en key( K BS , B ↔ S ) , B ahora cree que S dijo { t , A , A cree en key( K AB , A ↔ B )} . Como los relojes están sincronizados, B cree en fresh( t ), y por lo tanto fresh( A cree en key( K AB , A ↔ B ) ). Como B cree que la afirmación de S es fresh, B cree que S cree que ( A cree en key( K AB , A ↔ B ) ). Como B cree que S tiene autoridad sobre lo que A cree, B cree que ( A cree en key( K AB , A ↔ B ) ). Como B cree que A tiene autoridad sobre las claves de sesión entre A y B , B cree en key( K AB , A ↔ B ) . B ahora puede contactar a A directamente, utilizando K AB como clave de sesión secreta.
Ahora supongamos que abandonamos la suposición de que los relojes están sincronizados. En ese caso, S recibe el mensaje 1 de A con { t , key( K AB , A ↔ B )} , pero ya no puede concluir que t es reciente. Sabe que A envió este mensaje en algún momento en el pasado (porque está cifrado con K AS ) pero no que este es un mensaje reciente, por lo que S no cree que A necesariamente quiera seguir usando la clave K AB . Esto apunta directamente a un ataque al protocolo: un atacante que puede capturar mensajes puede adivinar una de las antiguas claves de sesión K AB . (Esto puede llevar mucho tiempo). El atacante luego reproduce el antiguo mensaje { t , key( K AB , A ↔ B )} y lo envía a S . Si los relojes no están sincronizados (quizás como parte del mismo ataque), S podría creer este antiguo mensaje y solicitar que B use nuevamente la antigua clave comprometida.
El documento original sobre Lógica de autenticación (cuyo enlace se encuentra a continuación) contiene este ejemplo y muchos otros, incluidos análisis del protocolo de enlace Kerberos y dos versiones del protocolo de enlace RPC de Andrew Project (una de las cuales es defectuosa).