imported>Aka: /* Axiome */ Tippfehler entfernt

2021-07-22T19:29:06Z

Neue Seite

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

Wird ein Protokoll analysiert, wird die Beschreibung des Protokolls in BAN-Logik ausgedrückt. Danach werden [[Prämisse]]n 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.<ref name="boyd1994">{{Literatur |Autor=Colin Boyd, Wenbo Mao |Titel=“On a Limitation of BAN Logic” |Sammelwerk=Lecture Notes in Computer Science |Band=765/1994 |Verlag=Springer Berlin / Heidelberg |Datum=2001-07 |ISSN=1611-3349 |Seiten=240–247 |DOI=10.1007/3-540-48285-7_20}}</ref>

== Konstrukte ==
* <math> P \mid\!\equiv X</math>: P glaubt X
* <math> P \triangleleft X</math>: P hat eine Nachricht erhalten, die X enthält. P kann X nun lesen und wiederholen.
* <math> P \mid\!\sim X</math>: P hat X in der Vergangenheit bereits gesendet
* <math>\sharp(X)</math>: X ist noch nicht im Zuge des Protokollverlaufs gesendet worden
* <math>P \Rightarrow X</math>: P hat Autorität über X und ist uneingeschränkt glaubwürdig, wenn er X äußert
* <math>P \overset{K}{\longleftrightarrow} Q</math>: Der symmetrische Schlüssel K kann für vertrauliche Kommunikation zwischen P und Q verwendet werden
* <math>\overset{K}{\mapsto}P</math>: P verwendet K als öffentlichen Schlüssel
* <math>P \overset{X}{\rightleftharpoons} Q</math>: X ist ein nur P und Q bekanntes Geheimnis
* <math>\{X\}_K</math>: Die Nachricht X ist mit dem symmetrischen Schlüssel K verschlüsselt
* <math>\langle X \rangle_Y</math>: 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 Schlussregel, die in allgemeiner Form wie folgt aussieht: <math>\frac{A_1,\ldots, A_n}{F}</math>. Hierbei sind <math>A_1, \ldots, A_n</math> Prämissen und <math>F</math> ist die Folgerung. Die Axiome im Einzelnen:

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

* <math>\frac{P\mid\!\equiv Q \overset{K}{\longleftrightarrow} P, \; P \triangleleft \{X\}_K}{P \mid\!\equiv Q \mid\!\sim X}</math> für [[Symmetrisches Kryptosystem|Symmetrische Verschlüsselung]],
* <math>\frac{P\mid\!\equiv \overset{K}{\mapsto} Q, \; P \triangleleft \{X\}_{K^{-1}}}{P \mid\!\equiv Q \mid\!\sim X}</math> für [[Asymmetrisches Kryptosystem|Asymmetrische Verschlüsselung]] und
* <math>\frac{P\mid\!\equiv Q \overset{Y}{\rightleftharpoons} P, \; P \triangleleft \langle X \rangle_Y}{P \mid\!\equiv Q \mid\!\sim X}</math> für [[Shared Secret]]s.

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 <math>\{X\}_K</math> nicht von P stammt.<ref name="monniaux2001">{{Literatur |Autor=David Monniaux |Titel=“Analysis of Cryptographic Protocols using Logics of Belief: an Overview” |Sammelwerk=Journal of Telecommunications and Information Technology |Band=4 |Datum=2002 |Seiten=57–67 |Online=http://citeseer.ist.psu.edu/monniaux01analysis.html}}</ref>

=== Nonce-Verification ===
Diese Regel ist die einzige, mit der von <math>\mid\!\sim</math> auf <math>\mid\!\equiv</math> 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.
:<math>\frac{P \mid\!\equiv \sharp(X),\; P \mid\!\equiv Q \mid\!\sim X}{P \mid\!\equiv Q \mid\!\equiv X}</math>

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 ===
:<math>\frac{P\mid\!\equiv Q \Rightarrow X, \; P \mid\!\equiv Q \mid\!\equiv X}{P \mid\!\equiv X}</math>

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.
:<math>\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}</math>

Ähnlich zu den Eigenschaften für <math>\mid\!\equiv</math> 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.
:<math>\frac{P \mid\!\equiv Q \mid\!\sim (X,Y)}{P \mid\!\equiv Q \mid\!\sim X}</math>

== Literatur ==
* {{Literatur
|Autor=Michael Burrows, Martín Abadi, Roger Needham
|Titel=“A Logic of Authentication” (revised version)
|Sammelwerk=ACM Transactions on Computer Systems
|Band=8
|Nummer=1
|Datum=1990-02
|ISSN=0734-2071
|Seiten=18–36
|DOI=10.1145/77648.77649}}

== Einzelnachweise ==
<references />

[[Kategorie:Kryptologie]]
[[Kategorie:Digitale Kommunikation]]
[[Kategorie:Nichtklassische Logik]]

Burrows-Abadi-Needham-Logik - Versionsgeschichte

imported>Aka: /* Axiome */ Tippfehler entfernt