La lógica de Burrows-Abadi-Needham - Burrows–Abadi–Needham logic

La lógica de 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. Específicamente, la lógica BAN ayuda a sus usuarios a determinar si la información intercambiada es confiable, está protegida contra escuchas o ambas cosas. La lógica de BAN comienza con la suposición de que todos los intercambios de información ocurren en medios vulnerables a la manipulación y el monitoreo público. Esto se ha convertido en el popular mantra de seguridad, "No confíe en la red".

Una secuencia lógica BAN típica incluye tres pasos:

  1. Verificación del origen del mensaje
  2. La verificación de mensaje de frescura
  3. Verificación de la confiabilidad del origen.

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 a menudo acompaña a una formulación de notación de protocolo de seguridad de un protocolo y, a veces, se proporciona en documentos.

Tipo de idioma

La lógica BAN y las lógicas de la misma familia son decidibles : existe un algoritmo que toma hipótesis BAN y una supuesta conclusión, y que responde si la conclusión es o no derivable de las hipótesis. Los algoritmos propuestos utilizan una variante de conjuntos mágicos .

Alternativas y críticas

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 de cifrado se analizaron en modelos operativos (asumiendo una criptografía perfecta) utilizando comprobadores de modelos, y se encontraron numerosos errores en los protocolos que se "verificaron" con lógica BAN y formalismos relacionados. En algunos casos, el análisis de BAN consideró que un protocolo era seguro, pero de hecho era inseguro. Esto ha llevado al abandono de las lógicas de la familia BAN a favor de métodos de prueba basados ​​en el razonamiento de invariancia estándar.

Reglas básicas

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 ):

  • P cree que X : P actúa como si X fuera verdadero y puede afirmar X en otros mensajes.
  • P tiene jurisdicción sobre X : se debe confiar en las creencias de P sobre X.
  • P dijo X : En un tiempo, P transmite (y cree) Mensaje de X , aunque P ya no podría creer X .
  • P ve X : P recibe el mensaje X , y puede leer y repetición X .
  • { X } K : X es encriptada con la clave K .
  • fresh ( X ): X no se ha enviado previamente en ningún mensaje.
  • clave ( K , P ↔ Q ): P y Q pueden comunicarse con la clave compartida K

El significado de estas definiciones se captura en una serie de postulados:

  • Si P cree en la clave ( K , P ↔ Q ) y P ve { X } K , entonces P cree ( Q dijo X )
  • Si P cree ( Q dijo X ) y P cree fresco ( X ), entonces P cree ( Q cree X ).

P debe creer que X está fresco aquí. Si no se sabe que X sea ​​nuevo, entonces podría ser un mensaje obsoleto, reproducido por un atacante.

  • Si P cree ( Q tiene jurisdicción sobre X ) y P cree ( Q cree en X ), entonces P cree en X
  • Hay varios otros postulados técnicos relacionados con la composición de mensajes. Por ejemplo, si P cree que Q dijo < X , Y >, la concatenación de X y Y , entonces P también cree que Q dijo X , y P también cree que Q dijo Y .

Con esta notación, se pueden formalizar las suposiciones detrás de un protocolo de autenticación. Usando los postulados, se puede probar que ciertos agentes creen que pueden comunicarse usando ciertas claves. Si la prueba falla, el punto de falla generalmente sugiere un ataque que compromete el protocolo.

BAN análisis lógico del protocolo Wide Mouth Frog

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. Usando notación estándar, el protocolo se puede especificar de la siguiente manera:

Los agentes A y B están equipados con las claves K as y K bs , respectivamente, para comunicarse de forma segura con S. Así que tenemos suposiciones:

A cree clave ( K as , A ↔ S )
S cree clave ( K as , A ↔ S )
B cree clave ( K bs , B ↔ S )
S cree clave ( K bs , B ↔ S )

Agente A quiere iniciar una conversación segura con B . Por lo tanto, inventa una clave, K AB , que se utilizará para comunicarse con B . A cree que esta clave es segura, ya que compuso la clave en sí:

A cree clave ( K ab , A ↔ B )

B está dispuesto a aceptar esta clave, siempre que esté seguro de que proviene de A :

B cree ( A tiene jurisdicción sobre la clave ( K , A ↔ B ))

Además, B está dispuesto a confiar en S para transmitir con precisión las claves de A :

B cree ( S tiene jurisdicción sobre ( A cree clave ( K , A ↔ B )))

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 lo creerá también.

El objetivo es tener

B cree clave ( K ab , A ↔ B )

A lee el reloj, obtiene la hora actual t , y envía el siguiente mensaje:

1 A → S : { t , tecla ( K ab , A ↔ B )} K como

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 como .

Dado que S cree que la tecla ( K as , A ↔ S ), y S ve { t , key ( K ab , A ↔ B )} K como , entonces S concluye que A realmente dijo { t , key ( K ab , A ↔ B )}. (En particular, S cree que el mensaje no fue fabricado completamente por algún atacante).

Dado que los relojes están sincronizados, podemos asumir

S cree fresco ( t )

Dado que S cree en fresco ( t ) y S cree que A dijo { t , key ( K ab , A ↔ B )}, S cree que A realmente cree en esa clave ( 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 del pasado).

S luego reenvía la llave a B :

2 S → B : { t , A , A cree la clave ( K ab , A ↔ B )} K bs

Debido a que el mensaje 2 está encriptado con K bs , y B cree en la clave ( K bs , B ↔ S ), B ahora cree que S dijo { t , A , A cree en la clave ( K ab , A ↔ B )}. Debido a que los relojes están sincronizados, B cree fresco ( t ) y, por lo tanto, fresco ( A cree clave ( K ab , A ↔ B )). Dado que B cree que la declaración de S es reciente, B cree que S cree que ( A cree la clave ( K ab , A ↔ B )). Debido a que B cree que S tiene autoridad sobre lo que A cree, B cree que ( A cree key ( K ab , A ↔ B )). Debido a que B cree que A tiene autoridad sobre las claves de sesión entre A y B , B cree que la clave ( K ab , A ↔ B ). B ahora puede contactar a A directamente, usando K ab como clave de sesión secreta.

Ahora supongamos que abandonamos el supuesto de que los relojes están sincronizados. En ese caso, S obtiene el mensaje 1 de A con { t , key ( K ab , A ↔ B )}, pero ya no puede concluir que t es nuevo. Sabe que A envió este mensaje en algún momento del pasado (porque está encriptado con K como ) pero no que este sea un mensaje reciente, por lo que S no cree que A necesariamente quiera continuar usando la clave K ab . Esto apunta directamente a un ataque al protocolo: un atacante que puede capturar mensajes puede adivinar una de las claves de sesión antiguas K ab . (Esto puede llevar mucho tiempo.) El atacante reproduce la antigua { t , clave ( K AB , A ↔ B )} mensaje, enviarlo a S . Si los relojes no están sincronizados (tal vez como parte del mismo ataque), S podría creer este mensaje antiguo y solicitar que B use la clave antigua comprometida de nuevo.

El documento de Logic of Authentication original (vinculado a continuación) contiene este ejemplo y muchos otros, incluidos los análisis del protocolo de enlace de Kerberos y dos versiones del protocolo de enlace de Andrew Project RPC (una de las cuales es defectuosa).

Referencias

Otras lecturas