Burrows-Abadi-Needham-Logik

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]

Inhaltsverzeichnis

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:

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

Wikimedia Foundation.

Игры ⚽ Нужно решить контрольную?

Schlagen Sie auch in anderen Wörterbüchern nach:

  • BAN-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… …   Deutsch Wikipedia

  • Roger Needham — (links) mit David Wheeler (Mitte) und dem Kanzler der University of Cambridge, ca. 1979 Roger Michael Needham (CBE FREng FRS) (* 9. Februar 1935; † 1. März 2003 in Willingham, Cambridgeshire) war ein britischer …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”