Burrows–Abadi–Needham logic

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

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

There are, however, weak points. On the one hand, certain log events can not be expressed in BAN logic. On the other hand, it must be idealized in translating in BAN logic, which is difficult. Safe and unsafe variants of a protocol can be expressed in BAN logic can hardly be more distinguished.

Constructs

  • : P believes X
  • : P has received a message containing X. P, X can now read and repeat.
  • : P X has already been sent in the past
  • X has not been sent as part of the log history
  • : P has authority over X and is fully credible if he expresses X
  • : The symmetric key K can be used for private communication between P and Q
  • : P K is used as a public key
  • : X is only P and Q -known secret
  • : The message X is encrypted with the symmetric key K
  • : X combined with the formula Y, where Y is a mystery, the use of the identity of the person proves that X is expressed

Axioms

BAN the logic circuit has a control, which looks in general terms as follows:. Here are the premises and the conclusion. The axioms are as follows:

Message Meaning

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

  • For symmetric ciphers,
  • For Asymmetric encryption and
  • For shared secrets.

Explained using the example of the first circuit means: From "P believes a secure symmetric key K for a compound with Q to know " and "P has received an encrypted message with K " is "P believes Q have sent X in the past".

Here, it is implicitly assumed that P may recognize locally encrypted messages, and that is not from P.

Nonce Verification

This rule is the only one that is closed with the of on. It expresses that a message "fresh" is, ie has not previously sent, and the sender still believes in it. This is an abstract challenge-response authentication is to prevent replay attacks, in particular.

If P believes that X is "fresh" and that Q has sent in the past X, then P believes that Q still believes in X. X here is by assumption a plain text.

Jurisdiction

If by faith of P, Q is an authority on X and X believes that P also believes X.

Characteristics of constructs

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

Similar to the properties of Q and each of the X and Y sub-statements sent if it has ( X, Y) sent. In contrast, the converse is not true, since X and Y were not necessarily coincide sent.

Communications protocol Public-key cryptography Challenge–response authentication Digital Object Identifier
102759
de