Burrows-Abadi-Needham-Logik

Die Burrows-Abadi-Needham-Logik (auch bekannt unter BAN-Logik) ist eine 1989 von Michael Burrows, Martín Abadi, Roger Needham publizierte Modallogik, mit der kryptographische Protokolle zum Informationsaustausch definiert und auf Schwachstellen untersucht werden können. Eine Weiterentwicklung der BAN-Logik ist die GNY-Logik.

Wird ein Protokoll analysiert, wird die Beschreibung des Protokolls in BAN-Logik ausgedrückt. Danach werden Prämissen des Protokolls analysiert und anschließend in gültige Aussagen transformiert.

Dabei gibt es jedoch auch Schwachstellen. Auf der einen Seite können gewisse Protokollereignisse gar nicht in BAN-Logik ausgedrückt werden. Andererseits muss beim Übersetzen in BAN-Logik idealisiert werden, was schwierig ist. Sichere und unsichere Varianten eines Protokolls können, in BAN-Logik ausgedrückt, kaum mehr unterschieden werden.^[1]

Konstrukte

• $P \mid\!\equiv X$: P glaubt X
• $P \triangleleft X$: P hat eine Nachricht erhalten, die X enthält. P kann X nun lesen und wiederholen.
• $P \mid\!\sim X$: P hat X in der Vergangenheit bereits gesendet
• $\sharp(X)$: X ist noch nicht im Zuge des Protokollverlaufs gesendet worden
• $P \Rightarrow X$: P hat Autorität über X und ist uneingeschränkt glaubwürdig, wenn er X äußert
• $P \overset{K}{\longleftrightarrow} Q$: Der symmetrische Schlüssel K kann für vertrauliche Kommunikation zwischen P und Q verwendet werden
• $\overset{K}{\mapsto}P$: P verwendet K als öffentlichen Schlüssel
• $P \overset{X}{\rightleftharpoons} Q$: X ist ein nur P und Q bekanntes Geheimnis
• {X}_K: Die Nachricht X ist mit dem symmetrischen Schlüssel K verschlüsselt
• $\langle X \rangle_Y$: X mit der Formel Y kombiniert, hierbei ist Y ein Geheimnis, dessen Verwendung die Identität desjenigen beweist, der X äußert

Axiome

Die BAN-Logik verfügt über eine Schlußregel, die in allgemeiner Form wie folgt aussieht: $\frac{A_1,\ldots, A_n}{F}$. Hierbei sind $A_1, \ldots, A_n$ Prämissen und F ist die Folgerung. Die Axiome im Einzelnen:

Message-Meaning

Diese Axiome regeln die Interpretation von Nachrichten. Für verschiedene Verschlüsselungsvarianten lauten sie:

• $\frac{P\mid\!\equiv Q \overset{K}{\longleftrightarrow} P, \; P \triangleleft \{X\}_K}{P \mid\!\equiv Q \mid\!\sim X}$ für Symmetrische Verschlüsselung,
• $\frac{P\mid\!\equiv \overset{K}{\mapsto} Q, \; P \triangleleft \{X\}_{K^{-1}}}{P \mid\!\equiv Q \mid\!\sim X}$ für Asymmetrische Verschlüsselung und
• $\frac{P\mid\!\equiv Q \overset{Y}{\rightleftharpoons} P, \; P \triangleleft \langle X \rangle_Y}{P \mid\!\equiv Q \mid\!\sim X}$ für Shared Secrets.

Am Beispiel des ersten Schlusses erläutert bedeutet dies: Aus „P glaubt einen sicheren, symmetrischen Schlüssel K für eine Verbindung mit Q zu kennen“ und „P hat eine mit K verschlüsselte Nachricht erhalten“ wird „P glaubt Q habe X in der Vergangenheit gesendet“.

Hierbei wird implizit angenommen, dass P lokal verschlüsselte Nachrichten erkennen kann und dass {X}_K nicht von P stammt.^[2]

Nonce-Verification

Diese Regel ist die einzige, mit der von $\mid\!\sim$ auf $\mid\!\equiv$ geschlossen wird. Sie drückt aus, dass eine Nachricht „frisch“ ist, also nicht zuvor gesendet wurde, und der Sender noch immer daran glaubt. Dies stellt eine abstrakte Challenge-Response-Authentifizierung dar, die insbesondere Replay-Angriffe verhindern soll.

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

Wenn P glaubt, dass X „frisch“ ist und dass Q in der Vergangenheit X gesendet hat, dann glaubt P, dass Q noch immer an X glaubt. X ist hierbei nach Voraussetzung ein Klartext.

Jurisdiction

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

Falls Q nach Glauben von P eine Autorität für X ist und X glaubt, so glaubt auch P X.

Eigenschaften der Konstrukte

P glaubt eine Menge von Aussagen (X, Y) nur genau dann, wenn er jede der Teilaussagen glaubt.

$\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}$

Ähnlich zu den Eigenschaften für $\mid\!\equiv$ hat Q auch jede der Teilaussagen X und Y gesendet, wenn er (X,Y) gesendet hat. Die Umkehrung gilt hingegen nicht, da X und Y dann nicht notwendigerweise zusammengesendet wurden.

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

Literatur

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

Einzelnachweise

1. ↑ Colin Boyd, Wenbo Mao: “On a Limitation of BAN Logic”. In: Lecture Notes in Computer Science. 765/1994, Springer Berlin / Heidelberg, ISSN 1611-3349, S. 240–247 (http://www.springerlink.com/content/ym13ycjlt2j1/).
2. ↑ David Monniaux: “Analysis of Cryptographic Protocols using Logics of Belief: an Overview”. In: Journal of Telecommunications and Information Technology. 4, 2002, S. 57–67 (http://citeseer.ist.psu.edu/monniaux01analysis.html).