Lógica de Burroughs-Abadie-Needham

La lógica Burrows -Abadi-Needham o lógica BAN es un modelo lógico formal para el análisis de conocimiento y confianza , ampliamente utilizado en el análisis de protocolos de autenticación .

La idea principal de la lógica BAN es que al analizar dichos protocolos, en primer lugar, se debe prestar atención a cómo las partes involucradas en el proceso de autenticación perciben la información: lo que dan por sentado y lo que saben con certeza o pueden ser. deducen los lógicos a través de hechos que les son fiables. [una]

Normalmente, los protocolos de autenticación se describen mediante la enumeración secuencial de los mensajes transmitidos entre los participantes del protocolo. Cada paso describe el contenido del mensaje y especifica el remitente y el destinatario. La lógica BAN trata la autenticidad de un mensaje en función de su integridad y novedad, utilizando reglas lógicas para realizar un seguimiento del estado de estos atributos a lo largo del protocolo. [2]

Hay tres tipos de objetos en la lógica BAN: miembros, claves de cifrado y fórmulas que los vinculan. En el análisis formal del protocolo, cada mensaje se convierte en una fórmula lógica; entonces las fórmulas lógicas están unidas por sentencias . Por lo tanto, la lógica BAN es en muchos aspectos similar a la lógica de Hoare . [3] La única operación lógica utilizada en esta lógica es la conjunción. También se introducen varios predicados , por ejemplo, establecer relaciones entre participantes y declaraciones (relaciones de confianza, jurisdicción, etc.) o expresar algunas propiedades de las declaraciones (como la frescura , es decir, la declaración de que la declaración se recibió recientemente).

Como cualquier lógica formal, la lógica BAN está equipada con axiomas y reglas de inferencia. El análisis de protocolo formal consiste en probar un cierto conjunto de declaraciones, expresadas por fórmulas de lógica BAN, utilizando reglas de inferencia. Por ejemplo, el requisito mínimo para cualquier protocolo de autenticación es que ambas partes deben confiar en que han encontrado una clave secreta para poder intercambiar información entre sí.

Predicados básicos y sus designaciones

$P|\equiv X$ significa que él cree en la afirmación . Esto significa que actuará como si fuera información verdadera. $PAGS$ $X$ $PAGS$ $X$
$P\vartriangleleft X$ implica que ve , es decir, recibió un mensaje que contiene . Es decir, puede leer y reproducir (quizás después del procedimiento de descifrado) el mensaje . $PAGS$ $X$ $PAGS$ $X$ $PAGS$ $X$
$P|\sim X$ significa que alguna vez expresó , es decir, en algún momento envió un mensaje que contenía . $PAGS$ $X$ $PAGS$ $X$
${\ estilo de visualización P | \ flecha derecha X}$ significa que tiene jurisdicción sobre (o tiene jurisdicción sobre ), es decir, tiene autoridad sobre un asunto relacionado con . $X$ $PAGS$ $PAGS$ $X$ $PAGS$ $X$
${\ estilo de visualización \ # X}$ significa que el estado de cuenta se recibió recientemente. Es decir, el mensaje no se envió en algún momento del pasado (antes de que se iniciara el protocolo). $X$ $X$
$P{\stackrel {k}{\longleftrightarrow}}Q$ significa eso y usar una clave compartida para la comunicación . $PAGS$ $q$ $k$
$\lbrace X\rbrace _{k}$ implica que los datos están encriptados con una clave . $X$ $k$

Otras denominaciones

La operación de conjunción se indica con una coma y la consecuencia lógica se indica con una barra horizontal. Por lo tanto, la regla lógica en la notación de la lógica BAN se escribe como ${\ estilo de visualización A \ cuña B \ flecha derecha C}$ ${\dfrac{A,B}{C))$

Axiomas de la lógica BAN

El tiempo se divide en dos eras: pasado y presente . El presente comienza desde el momento en que se lanza el protocolo.
El participante que habla cree en la verdad . $PAGS$ $X$ $X$
El cifrado se considera absolutamente seguro: un mensaje cifrado no puede ser descifrado por un participante que no conozca la clave.

Reglas de salida

Regla del significado del mensaje :

{\dfrac {A|\equiv A{\stackrel {K}{\longleftrightarrow}}B,A\vartriangleleft \lbrace X\rbrace _{K}}{A|\equiv B|\sim X}}

Formulación verbal equivalente: de los supuestos que cree en compartir la clave con , y ve el mensaje encriptado con la clave , se deduce que cree que en algún momento dijo . $A$ $k$ $B$ $A$ $X$ $k$ $A$ $B$ $X$

Tenga en cuenta que aquí se supone implícitamente que él mismo nunca expresó . $A$ $X$

Regla para verificar la unicidad de las inserciones numéricas :

{\dfrac {A|\equiv \#X,A|\equiv B|\sim X}{A|\equiv B|\equiv X))

es decir, si cree en la novedad y en lo que alguna vez expresó , entonces cree que todavía confía . $A$ $X$ $B$ $X$ $A$ $B$ $X$

Regla de jurisdicción :

{\dfrac {A|\equiv B|\Rightarrow X,A|\equiv B|\equiv X}{A|\equiv X))

afirma que si cree en poderes sobre , y cree en lo que cree , entonces debe creer en . $A$ $B$ $X$ $A$ $B$ $X$ $A$ $X$

Otras reglas

El operador de confianza y la conjunción obedecen a las siguientes relaciones:

{\dfrac {A|\equiv X,A|\equiv Y}{A|\equiv (X,Y)))

{\dfrac {A|\equiv (X,Y)}{A|\equiv X))

{\dfrac {A|\equiv B|\equiv (X,Y)}{A|\equiv B|\equiv X))

De hecho, estas reglas establecen el siguiente requisito: confiar en algún conjunto de declaraciones si y solo si confía en cada declaración por separado. $A$ $A$

Existe una regla similar para el operador : ${\ estilo de visualización | \ sim}$

{\dfrac {A|\equiv B|\sim (X,Y)}{A|\equiv B|\sim X))

Finalmente, si una parte de la declaración se recibió recientemente, entonces se puede decir lo mismo sobre la declaración completa:

{\dfrac {A|\equiv \#X}{A|\equiv \#(X,Y)))

Un enfoque formal para el análisis de los protocolos de autenticación

Desde un punto de vista práctico, el análisis del protocolo se realiza de la siguiente manera: [4] [5]

El protocolo original se convierte en uno idealizado (es decir, escrito en términos de lógica BAN).
Se añaden supuestos sobre el estado inicial del protocolo.
Cada declaración está asociada con una fórmula lógica, es decir, una declaración lógica sobre el estado del protocolo después de cada declaración.
Las reglas de inferencia y los axiomas se aplican a los supuestos y afirmaciones del protocolo para determinar el estado de confianza de las partes al concluir el protocolo.

Expliquemos el significado de este procedimiento. El primer paso se llama idealización y consiste en lo siguiente: cada paso del protocolo, escrito como , se transforma en un conjunto de declaraciones lógicas relativas a las partes transmisora y receptora. Deje, por ejemplo, que uno de los pasos del protocolo se vea así: $P\longrightarrow Q:mensaje$

A\longrightarrow B:\lbrace A,K_{ab}\rbrace_{K_{bs}}

Este mensaje le dice a la parte (que tiene la clave ) que la clave debe usarse para comunicarse con . La fórmula lógica correspondiente para este mensaje es: $B$ ${\ Displaystyle K_ {bs}}$ ${\ Displaystyle K_ {ab}}$ $A$

A\longrightarrow B:\lbrace A{\stackrel {K_{ab}}{\longleftrightarrow }}B\rbrace_{K_{bs}}

Cuando se entrega el mensaje dado , la declaración es verdadera: $B$

B\vartriangleleft \lbrace A{\stackrel {K_{ab}}{\longleftrightarrow }}B\rbrace_{K_{bs}}

es decir, ve este mensaje y seguirá actuando de acuerdo con él. $B$

Después de la idealización, el protocolo parece una secuencia de declaraciones y declaraciones que conectan estas declaraciones. La declaración inicial consta de los supuestos iniciales del protocolo, la declaración final es el resultado del protocolo:

[suposiciones]S_{1}[afirmación1]\cdots [afirmación(n-1)]S_{n}[conclusiones]

Un protocolo se considera correcto si el conjunto de declaraciones finales incluye el conjunto de objetivos de protocolo (formalizados).

Propósitos de los protocolos de autenticación

Escribamos los objetivos del protocolo de autenticación en términos de lógica BAN (es decir, qué afirmaciones lógicas deben derivarse de las suposiciones del protocolo, dada la secuencia de pasos (afirmaciones) realizadas en este protocolo): [6] [7]

A|\equiv A{\stackrel {K}{\longleftrightarrow}}B

B|\equiv A{\stackrel {K}{\longleftrightarrow}}B

es decir, ambas partes deben confiar en que están utilizando la misma clave secreta para intercambiar mensajes. Sin embargo, puedes pedir más, por ejemplo:

A|\equiv B|\equiv A{\stackrel {K}{\longleftrightarrow}}B

B|\equiv A|\equiv A{\stackrel {K}{\longleftrightarrow}}B

es decir, acuse de recibo de la clave . [6]

Analizando el protocolo de la rana de boca ancha usando la lógica BAN

Considere un protocolo de autenticación simple , el protocolo de rana de boca ancha , que permite que dos partes, y , establezcan una conexión segura utilizando un servidor en el que ambos confían y relojes sincronizados. [8] En notación estándar, el protocolo se escribe de la siguiente manera: $A$ $B$ $S$

A\rightarrow S:A,\{T_{A},K_{ab},B\}_{K_{as))

S\rightarrow B:\{T_{S},K_{ab},A\}_{K_{bs}}

Después de la idealización, los pasos del protocolo toman la forma:

A\rightarrow S:\{T_{A},A{\stackrel {K_{ab}}{\longleftrightarrow }}B\}_{K_{as}}

S\rightarrow B:\{T_{S},A|\equiv A{\stackrel {K_{ab}}{\longleftrightarrow }}B\}_{K_{bs}}

Escribamos los supuestos iniciales del protocolo. Las partes y tienen claves y , respectivamente, para la comunicación segura con el servidor , que en el lenguaje de la lógica BAN se puede expresar como: $A$ $B$ ${\ Displaystyle K_ {como}}$ ${\ Displaystyle K_ {bs}}$ $S$

A|\equiv A{\stackrel {K_{as}}{\longleftrightarrow }}S

S|\equiv A{\stackrel {K_{as}}{\longleftrightarrow }}S

B|\equiv B{\stackrel {K_{bs}}{\longleftrightarrow }}S

S|\equiv B{\stackrel {K_{bs}}{\longleftrightarrow }}S

También hay suposiciones sobre las inserciones temporales:

S|\equiv\#T_{A}

B|\equiv\#T_{S}

Más allá de eso, hay algunas suposiciones sobre la clave de cifrado:

$B$ depende en la elección de una buena clave: $A$

B|\equiv A|\Rightarrow (A{\stackrel {K_{ab)){\longleftrightarrow }}B)

$B$ confía en pasar la clave de : $S$ $A$

B|\equiv S|\Rightarrow (A|\equiv A{\stackrel {K_{ab)){\longleftrightarrow }}B)

$A$ confía en que la clave de sesión es aceptada:

A|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)

Pasemos al análisis del protocolo.

$S$ recibe el primer mensaje, del cual se pueden extraer las siguientes conclusiones:

$S$ , al ver un mensaje encriptado con la clave , concluye que fue enviado (la regla sobre el significado del mensaje). ${\ Displaystyle K_ {como}}$ $A$
La presencia de una nueva inserción temporal nos permite concluir que todo el mensaje fue escrito recientemente (la regla para el operador ). $EJÉRCITO DE RESERVA}$ ${\ estilo de visualización \ #}$
De la frescura de todo el mensaje , puede concluir que creía en lo que envió (la regla para verificar la unicidad de las inserciones numéricas). $S$ $A$

Por lo tanto, . $S|\equiv A|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)$

$B$ recibe el segundo mensaje de protocolo, lo que da como resultado:

Al ver un mensaje cifrado con la clave , el cliente entiende que ha sido enviado . ${\ Displaystyle K_ {bs}}$ $B$ $S$
La inserción temporal demuestra que el mensaje completo se envió recientemente. $T_{S}$ $B$
Ante la frescura del mensaje, concluye que confía en todo lo enviado. $B$ $S$
En particular, cree que confía en la segunda parte del mensaje. $B$ $S$
Pero también cree que está en la competencia averiguar si su socio conoce la clave secreta y, por lo tanto, le confía la autoridad para generar la clave. $B$ $S$ $A$ $B$ $A$

De estas consideraciones se pueden extraer las siguientes conclusiones:

B|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)

B|\equiv A|\equiv (A{\stackrel {K_{ab)){\longleftrightarrow }}B)

Teniendo en cuenta el supuesto inicial de , obtenemos que el protocolo analizado está justificado. Lo único que no se puede decir es: $A|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)$

A|\equiv B|\equiv (A{\stackrel {K_{ab}}{\longleftrightarrow }}B)

es decir, no logró confirmar que recibió la clave deseada. $A$ $B$

Crítica

El proceso de idealización es el más criticado, ya que el protocolo idealizado puede no reflejar correctamente su contraparte real. [9] Esto se debe a que la descripción de los protocolos no se da de manera formal, lo que en ocasiones pone en duda la posibilidad misma de una correcta idealización. [10] Además, varios críticos intentan demostrar que la lógica BAN también puede obtener características obviamente incorrectas de los protocolos. [10] Además, el resultado del análisis del protocolo utilizando la lógica BAN no puede considerarse una prueba de su seguridad, ya que esta lógica formal se ocupa exclusivamente de cuestiones de confianza. [once]

Notas

↑ N. Smart, Criptografía, pág. 175.
↑ B. Schneier, "Criptografía aplicada", p. 66.
↑ M. Burrows, M. Abadi, R. Needham, "Una lógica de autenticación", pág. 3.
↑ M. Burrows, M. Abadi, R. Needham, "Una lógica de autenticación", pág. once.
↑ B. Schneier, "Criptografía aplicada", p. 67.
↑ 1 2 N. Smart, "Criptografía", pág. 177.
↑ M. Burrows, M. Abadi, R. Needham, "Una lógica de autenticación", pág. 13
↑ N. Smart, Criptografía, pág. 169-170.
↑ DM Nessett, "Una crítica de la lógica de Burrows, Abadi y Needham", págs. 35-38.
↑ 1 2 Boyd, C. y Mao, W. "Sobre una limitación de la lógica BAN"
↑ PF Syverson, "El uso de la lógica en el análisis de protocolos criptográficos"

Literatura

M. Burrows, M. Abadi, R. Needham. Una lógica de autenticación (neopr.) // Centro de investigación de sistemas de Digital Equipment Corporation en Palo Alto. - 1989. - Diciembre ( vol. 426 ). - S. 44-54 .

Monniaux, D. Procedimientos de decisión para el análisis de protocolos criptográficos por lógica de creencia // Taller de fundamentos de seguridad informática, 1999. Actas del 12º IEEE: revista. - 1999. - Págs. 44-54 .

Boyd, Colin; Mao, Wenbo. Sobre una limitación de la lógica BAN // Avances en criptología - EUROCRYPT '93 (neopr.) / Helleseth, Tor. - Springer Berlín/Heidelberg, 1994. - S. 240-247. - ISBN 978-3-540-57600-6 .

N inteligente. Criptografía . - Moscú: Technosfera, 2005. - S. 162 -179. — 528 pág. - ISBN 5-94836-043-1 .

B. Schneier. Criptografía aplicada (neopr.) . - John Wiley & Sons , 1995. - S. 66-69. — 662 pág. - ISBN 0-47111-709-9 . Archivado el 3 de septiembre de 2012 en Wayback Machine .

A. Alferov, A. Kuzmin, A. Zubov, A. Cheremushkin. Fundamentos de Criptografía . - Moscú: Helios ARV, 2002. - S. 378-385 , 404-406. — 480 s. — ISBN 5-85438-025-0 .

Enlaces

Material del curso UT Austin CS sobre lógica BAN (PDF) Archivado el 26 de enero de 2020 en Wayback Machine .
Authentication Logic ( Mirror ), fuente original de Michael Burrows , Martín Abadi y Roger Needham .
Fuente: La lógica de Burrows-Abadi-Needham
Lógica de BAN en contexto, de UT Austin CS (PDF) Archivado el 26 de enero de 2020 en Wayback Machine .