Burrows-Abadi-Needham logic

The Burrows-Abadi-Needham logic (also known as BAN logic ) is a modal logic published in 1989 by Michael Burrows, Martín Abadi and Roger Needham , with which cryptographic protocols for information exchange can be defined and examined for weak points. A further development of the BAN logic is the GNY logic .

If a protocol is analyzed, the description of the protocol is expressed in BAN logic. Then the premises of the protocol are analyzed and then transformed into valid statements.

However, there are also weak points. On the one hand, certain protocol events cannot be expressed in BAN logic at all. On the other hand, when translating into BAN logic, you have to idealize, which is difficult. In terms of BAN logic, it is hardly possible to differentiate between secure and insecure variants of a protocol.

Constructs

• ${\displaystyle P\mid \!\equiv X}$: P believes X
• ${\displaystyle P\triangleleft X}$: P received a message that contains X. P can now read and repeat X.
• ${\displaystyle P\mid \!\sim X}$: P has already sent X in the past
• ${\displaystyle \sharp (X)}$: X has not yet been sent in the course of the protocol process
• ${\displaystyle P\Rightarrow X}$: P has authority over X and is fully credible when he expresses X.
• ${\displaystyle P{\overset {K}{\longleftrightarrow }}Q}$: The symmetric key K can be used for confidential communication between P and Q.
• ${\displaystyle {\overset {K}{\mapsto }}P}$: P uses K as the public key
• ${\displaystyle P{\overset {X}{\rightleftharpoons }}Q}$: X is a secret known only to P and Q.
• ${\displaystyle \{X\}_{K}}$: The message X is encrypted with the symmetric key K.
• ${\displaystyle \langle X\rangle _{Y}}$: X combined with the formula Y, here Y is a secret, the use of which proves the identity of the person who utters X

Axioms

The BAN logic has a final rule that looks like in general terms follows: . Here are premises and is the inference. The axioms in detail: ${\displaystyle {\frac {A_{1},\ldots ,A_{n}}{F}}}$ ${\displaystyle A_{1},\ldots ,A_{n}}$ ${\displaystyle F}$

Message meaning

These axioms regulate the interpretation of messages. For different encryption variants they are:

• ${\displaystyle {\frac {P\mid \!\equiv Q{\overset {K}{\longleftrightarrow }}P,\;P\triangleleft \{X\}_{K}}{P\mid \!\equiv Q\mid \!\sim X}}}$for symmetric encryption ,
• ${\displaystyle {\frac {P\mid \!\equiv {\overset {K}{\mapsto }}Q,\;P\triangleleft \{X\}_{K^{-1}}}{P\mid \!\equiv Q\mid \!\sim X}}}$for asymmetric encryption and
• ${\displaystyle {\frac {P\mid \!\equiv Q{\overset {Y}{\rightleftharpoons }}P,\;P\triangleleft \langle X\rangle _{Y}}{P\mid \!\equiv Q\mid \!\sim X}}}$for shared secrets .

Using the example of the first conclusion, this means: From "P believes he knows a secure, symmetrical key K for a connection with Q" and "P has received a message encrypted with K" becomes "P believes Q sent X in the past" .

It is implicitly assumed here that P can recognize locally encrypted messages and that it does not originate from P. ${\displaystyle \{X\}_{K}}$

Nonce verification

This rule is the only one that closes from to . It expresses that a message is "fresh", that is, it was not sent before, and the sender still believes in it. This represents an abstract challenge-response authentication , which is particularly intended to prevent replay attacks. ${\displaystyle \mid \!\sim }$ ${\displaystyle \mid \!\equiv }$

${\displaystyle {\frac {P\mid \!\equiv \sharp (X),\;P\mid \!\equiv Q\mid \!\sim X}{P\mid \!\equiv Q\mid \!\equiv X}}}$

If P believes that X is "fresh" and that Q has sent X in the past, then P believes that Q still believes in X. According to the prerequisite, X is plain text.

Jurisdiction

${\displaystyle {\frac {P\mid \!\equiv Q\Rightarrow X,\;P\mid \!\equiv Q\mid \!\equiv X}{P\mid \!\equiv X}}}$

If, according to P's belief, Q is an authority for X and believes X, then P also believes X.

Properties of the constructs

P believes a set of statements (X, Y) only if and only if he believes each of the partial statements.

${\displaystyle {\frac {P\mid \!\equiv X,\;P\mid \!\equiv Y}{P\mid \!\equiv (X,Y)}},\quad {\frac {P\mid \!\equiv (X,Y)}{P\mid \!\equiv X}},\quad {\frac {P\mid \!\equiv Q\mid \!\equiv (X,Y)}{P\mid \!\equiv Q\mid \!\equiv X}}}$

Similar to the properties for , Q also sent each of the partial statements X and Y if it sent (X, Y). The reverse, however, does not apply, since X and Y were then not necessarily sent together. ${\displaystyle \mid \!\equiv }$

${\displaystyle {\frac {P\mid \!\equiv Q\mid \!\sim (X,Y)}{P\mid \!\equiv Q\mid \!\sim X}}}$

literature

• Michael Burrows, Martín Abadi, Roger Needham: “A Logic of Authentication” (revised version) . In: ACM Transactions on Computer Systems . tape 8 , no. 1 , February 1990, ISSN  0734-2071 , p. 18-36 , doi : 10.1145 / 77648.77649 .

Individual evidence

1. ↑ Colin Boyd, Wenbo Mao, “On a Limitation of BAN Logic” . In: Lecture Notes in Computer Science . tape 765/1994 . Springer Berlin / Heidelberg, ISSN  1611-3349 , p. 240-247 , doi : 10.1007 / 3-540-48285-7_20 .
2. ↑ David Monniaux: “Analysis of Cryptographic Protocols using Logics of Belief: an Overview” . In: Journal of Telecommunications and Information Technology . tape 4 , 2002, p. 57-67 ( psu, edu ).