In diesem Kapitel wird eine einfache eingebettete domänenspezifische Sprache für die Modellierung von Kryptoschemata entwickelt. Eine domänenspezifische Sprache ist eine Programmiersprache, die im Gegensatz zu einer General-purpose-Programmiersprache für einen eingeschränkten Einsatzbereich gedacht sind. Beispiele für domänenspezifische Sprachen sind CSS, VHDL, MATLAB und SQL. Bei einer eingebetteten domänenspezifischen Sprache wird keine komplett neue Sprache inklusive Compiler entwickelt, sondern es wird lediglich eine Bibliothek in einer Host-Sprache entwickelt, die aber von Domänenexpert*innen verwendet werden soll. Daher nutzen solche Bibliotheken häufig Nomenklatur und Symbole, die Domänenexpert*innen bekannt sind. Bekannte Beispiele von eingebetteten domänenspezifischen Sprachen sind JUnit, React und LINQ.

Der Code in diesem Abschnitt ist an die Implementierung aus der Publikation The foundational cryptography framework angelehnt. Der Quellcode dieser Bibliothek ist unter https://github.com/adampetcher/fcf zu finden.

Wahrscheinlichkeitsverteilungen

In diesem Abschnitt diskutieren wir, wie wir Wahrscheinlichkeitsverteilungen in Coq modellieren. Eine Wahrscheinlichkeitsverteilung (Distribution) wird durch den folgenden Datentyp modelliert.

Definition Dist (A : Type) := A -> rat.

Das heißt, eine Wahrscheinlichkeitsverteilung von booleschen Werten wird durch eine Funktion von bool nach rat modelliert. Das heißt, wir können in die Funktion einen Wert vom Typ bool stecken und erhalten dann die Wahrscheinlichkeit, die dieser Wert in der Verteilung hat.

Wir können zum Beispiel wie folgt eine Wahrscheinlichkeitsverteilung für boolesche Werte definieren, die dem Ereignis true die Wahrscheinlichkeit 1/4 zuordnet und dem Ereignis false die Wahrscheinlichkeit 3/4. Im Folgenden gehen wir immer davon aus, dass die Wahrscheinlichkeiten einer Verteilung in der Summe 1 ergeben.

Definition unfairCoin : Dist bool :=
  fun b => if b then 1/4 else 3/4.

Außerdem können wir wie folgt eine Wahrscheinlichkeitsverteilung für eine faire Münze definieren.

Definition fairCoin : Dist bool :=
  fun _ => 1/2.

Wir definieren außerdem eine Funktion, um zu prüfen, ob zwei Wahrscheinlichkeitsverteilungen gleich sind. Dazu prüfen wir, ob die Wahrscheinlichkeiten für alle möglichen Ereignisse identisch sind.

Definition eq_dist {A : Type} (d1 d2 : Dist A) : Prop :=
  forall e : A, d1 e = d2 e.

Wahrscheinlichkeitsbasierte Berechnungen

Unser eigentliches Ziel ist die Beschreibung von Kryptoschemata. Ein Kryptoschema beschreibt dabei, wie ein Schlüssel generiert, wie eine Nachricht verschlüsselt und wie eine Nachricht entschlüsselt wird. Ein Kryptoschema wird dabei durch eine Art Berechnung beschrieben. Die Berechnungen sind dabei wahrscheinlichkeitsbasiert, das heißt, es gibt Primitive um einen zufälligen Wert zu generieren. In unserem Kontext wird es möglich sein, einen zufälligen Bit-Vektor einer bestimmten Länge zu erzeugen. Dabei haben alle Bit-Vektoren der angegebenen Länge die gleiche Wahrscheinlichkeit, dass sie gezogen werden, das heißt, sie sind gleichverteilt.

Neben dem Generieren eines zufälligen Bit-Vektors soll es auch möglich sein, auf diesen Bit-Vektor eine Operation anzuwenden. Um eine solche Berechnung zu modellieren, nutzen wir eine monadische Modellierung. Die genauen Hintergründe, was eine Monade ist, sollen hier keine Rolle spielen. Mithilfe einer Monade kann man aber verschiedene Formen von “Hintereinanderausführungen” beschreiben. Ein Beispiel für eine solche “Hintereinanderausführung” ist die Modellierung von Berechnungen, die mit Wahrscheinlichkeiten arbeiten.

Wir definieren erst einmal den folgenden Datentyp und werden im Anschluss diskutieren, welche Bedeutung die einzelnen Konstruktoren haben.

Inductive Comp : Type -> Type :=
  | Rnd (n : nat) : Comp (Bvector n)
  | Ret (A : Type) (eqb : A -> A -> bool) (value : A) : Comp A
  | Bind (A B : Type) (c : Comp B) (f : B -> Comp A) : Comp A.

Arguments Ret {A}.
Arguments Bind {A} {B}.

Der Datentyp Comp beschreibt Berechnungen, die mit Wahrscheinlichkeiten arbeiten. Wir nutzen für die Definition von Comp einen Ansatz der sehr stark and die induktiv definierten Propositionen erinnert. Man nennt diese Form eines Datentyps auch einen GADT (Generalized Algebraic Data Type). Wie der Name schon andeutet, handelt es sich hierbei um eine Verallgemeinerung von algebraischen Datentypen, wie wir sie bisher verwendet haben. Bei der Modellierung von induktiv definierten Propositionen nutzt man ebenfalls dieses Sprach-Feature. Auch die Programmiersprache Haskell stellt GADTs als Sprach-Feature zur Verfügung.

Mit dem Datentyp Comp können wir wahrscheinlichkeitsbasierte Berechnungen modellieren. Wir werden später eine Funktion definieren, die in der Lage ist, für eine Berechnung vom Typ Comp eine Wahrscheinlichkeitsverteilung zu berechnen. Das heißt, wir können Berechnungen schreiben und für diese Berechnungen berechnen, wie wahrscheinlich es ist, dass die Berechnung ein bestimmtes Ergebnis liefern.

Das One-Time Pad

Um den Datentyp Prop zu illustrieren betrachten wir ein One-Time Pad. Ein One-Time Pad ist eine ganz einfache Variante eines Kryptoschemas. Abbildung 1 zeigt die Definition des One-Time Pads aus dem Buch Introduction to Modern Cryptography.

Abbildung 1: Das Kryptoschema des _One-Time Pads_

In Coq setzen wir diese Definition wie folgt um.

Section OneTimePad.
  Variable l : nat.

  Definition Plaintext : Type := {0,1}^l.
  Definition Key : Type := {0,1}^l.
  Definition Ciphertext : Type := {0,1}^l.

  Definition Gen : Comp Key :=
    {0,1}^l.

  Definition Enc (k : Key) (m : Plaintext) : Comp Ciphertext :=
    ret (k ⊕ m).

  Definition Dec (k : Key) (c : Ciphertext) : Comp Plaintext :=
    ret (k ⊕ c).

End OneTimePad.

Wir werden die Definition des One-Time Pad jetzt Stück für Stück erklären.

In Coq kann man innerhalb einer Section eine Variable definieren. Diese Variable kann dann in allen folgenden Definitionen innerhalb der Section verwendet werden. Wenn wir eine Definition, die diese Variable nutzt, von außerhalb der Section verwenden, müssen wir den Wert der Variable als weiteres Argument an die Definition übergeben. Das heißt, Wenn wir Gen von außerhalb der Section verwenden wollen, erhält Gen ein Argument vom Typ nat. Durch die Verwendung einer Variable kann man Definitionen angeben, wie sie in

Die Konstanten Plaintext, Key und Ciphertext definieren die Typen, aus denen Klartext, Schlüssel und Geheimtext kommen. Im Fall des One-Time Pads handelt es sich hierbei jeweils um Bit-Vektoren. Die folgende Notation führt eine in der Kryptografie übliche Schreibweise für Bit-Vektoren ein.

Notation "{ 0 , 1 } ^ n" := (Bvector n) (at level 50) : type_scope.

Die Definition Gen in OneTimePad gibt an, wie bei einem One-Time Pad der Schlüssel erzeugt wird. Dazu wird zufällig ein Bit-Vektor der Länge l erzeugt. Die Definition Gen nutzt die folgende Notation.

Notation "{ 0 , 1 } ^ n" := (Rnd n) (at level 50).

Der Konstruktor Rnd modelliert das gleichverteilte Auswählen eines Bit-Vektors. Der Konstruktor erhält dazu die natürliche Zahl, die angibt, wie lang der Bit-Vektor ist.

Die Definition Enc beschreibt, wie eine Nachricht bei einem One-Time Pad verschlüsselt wird. Dazu erhält Enc den Schlüssel k und die Nachricht m, beides Bit-Vektoren der Länge l. Bei einem One-Time Pad werden Schlüssel und Nachricht mit einem punktweisen Xor miteinander verknüpf. Das Ergebnis ist die verschlüsselte Nachricht. Die Definition Enc liefert als Ergebnis eine Berechnung, die einen Bit-Vektor der Länge l liefert. Daher ist der Ergebnistyp der Funktion Enc vom Typ Comp (Bvector l). Um aus einem Wert den Ergebniswert einer Berechnung zu machen, nutzen wir den Konstruktor Ret. Der Konstruktor Ret speichert den Wert, den die Berechnung als Ergebnis liefern soll. Außerdem speichert die Konstruktor noch eine Funktion, um den Wert mit einem anderen Wert zu vergleichen. Wir werden später sehen, wofür diese Funktion genutzt wird.

Notation "'ret' v" := (Ret (BVeq _ _) v) (at level 60).

Neben der Funktion Enc stellt ein Kryptoschema noch eine Funktion Dec zum Entschlüsseln einer Nachricht zur Verfügung. Diese Funktion erhält ebenfalls den Schlüssel k und eine verschlüsselte Nachricht c. Das Ergebnis der Funktion ist die entschlüsselte Nachricht. Hier wird wiederum der Konstruktor Ret genutzt, um die entschlüsselte Nachricht in ein Comp umzuwandeln.

Korrektheit

Um den Konstruktor Bind zu motivieren, betrachten wir eine grundlegende Eigenschaft eines Kryptoschemas. Bei einem Kryptoschema wie dem One-Time Pad sollte das Entschlüsseln einer verschlüsselten Nachricht wieder die Originalnachricht liefern. Da die Funktionen Enc und Dec wahrscheinlichkeitsbasiert sind, erhalten wir nicht direkt die Ausgangsnachricht m, sondern eine Wahrscheinlichkeitsverteilung, die mit Wahrscheinlichkeit 1 den Wert m liefert.

Theorem otp_correct :
  forall (k : Key) (m : Plaintext), eq_comp (c <- Enc k m; Dec k c) (ret m).

Die Funktion eq_comp ist wie folgt definiert und gibt an, dass zwei wahrscheinlichkeitsbasierte Berechnungen die gleiche Verteilung erzeugen.

Definition eq_comp {A : Type} (c1 c2 : Comp A) : Prop :=
  eq_dist (dist c1) (dist c2).

Die Funktion dist berechnet die Wahrscheinlichkeitsverteilung einer wahrscheinlichkeitsbasierten Berechnung. Wir werden die Definition dieser Funktion später diskutieren.

Um das Lemma otp_correct genauer zu verstehen, müssen wir noch einige Notationen einführen, die dort verwendet werden. Zuerst einmal müssen wir in der Lage sein, eine Berechnung zu beschreiben, die eine Nachricht verschlüsselt und anschließend entschlüsselt. Die Funktion Enc hat den Ergebnistyp Comp (Bvector l), die Funktion Dec erhält aber ein Argument vom Typ Bvector l und keine Berechnung. Daher müssen wir in der Lage sein, diese beiden Komponenten zu kombinieren. Zu diesem Zweck nutzen wir den Konstruktor Bind. Dieser Konstruktor nimmt ein Comp B und eine Funktion B -> Comp A und konstruiert daraus ein Comp A. Wir führen wiederum Notation ein, um eine Syntax nutzen zu können, wie sie im Bereich der Kryptographie für diese Art von wahrscheinlichkeitsbasierten Berechnungen üblich ist.

Notation "x <- c1 ; c2" := (Bind c1 (fun x => c2)) (right associativity, at level 65, c1 at next level).

Zu guter Letzt fehlt noch die Definition der Funktion dist. Diese Funktion berechnet die Wahrscheinlichkeitsverteilung, die ein Programm vom Typ Prog erzeugt.

Fixpoint dist {A: Type} (comp: Comp A) : Dist A :=
  match comp with
  | Rnd n => fun _ => 1 / Pos.of_nat (2^n)
  | Ret eqb a => fun b => if eqb a b then 1 else 0
  | Bind c f => fun e1 => sum (List.map (fun e2 => dist c e2 * dist (f e2) e1) (support p))
  end.

Der Fall für den Konstruktor Rnd erzeugt eine Gleichverteilung. Die Wahrscheinlichkeit jedes einzelnen Vektors ergibt sich als 1 durch die Anzahl der Vektoren, die es gibt. Der Konstruktor Ret beschreibt eine Wahrscheinlichkeitsverteilung, bei der ein Ereignis die Wahrscheinlichkeit 1 und alle anderen Ereignisse die Wahrscheinlichkeit 0 haben. Zur Definition dieser Wahrscheinlichkeitsverteilung nutzen wir die Funktion eqb, die im Konstruktor Ret enthalten ist.

Der komplizierteste Fall bei der Berechnung der Wahrscheinlichkeitsverteilung ist der Konstruktor Bind. Die Variable e1 enthält das Ereignis für das wir die Wahrscheinlichkeit berechnen wollen. Dazu berechnen wir erst einmal den Support der Wahrscheinlichkeitsverteilung c. Der Support ist die Menge der Ereignisse, die eine Wahrscheinlichkeit besitzen, die ungleich 0 ist. Für jedes Ereignis e2, dessen Wahrscheinlichkeit ungleich 0 ist, berechnen wir die konkrete Wahrscheinlichkeit, durch eval p e2. Außerdem wird die Funktion f auf das Ereignis e2 angewendet und für das Ergebnis vom Typ Comp eine Wahrscheinlichkeitsverteilung berechnet. Für diese berechnen wir dann die Wahrscheinlichkeit für Ereignis e1. Am Ende summieren wir alle Wahrscheinlichkeiten für die Ereignisse aus dem Support auf.

Als nächstes definieren wir eine Funktion support, die für ein Programm berechnet, welche Werte eine Wahrscheinlichkeit ungleich 0 haben.

Fixpoint support {A : Type} (comp : Comp A) : list A :=
  match comp with
  | Rnd n => all_bvectors n
  | Ret _ a => [a]
  | Bind c f => distinct (eqb_comp (f (value c))) (List.flat_map (fun e => support (f e)) (support c))
  end.

Die ersten beiden Fälle sind wiederum recht einfach. Im Fall des Konstruktors Rnd haben alle Vektoren eine Wahrscheinlichkeit, die ungleich null ist, da die Vektoren gleichverteilt generiert werden. Im Fall des Konstruktors Ret gibt es nur einen einzigen Wert, der eine Wahrscheinlichkeit hat, die ungleich null ist. Im Fall des Konstruktors Bind ist die Berechnung wiederum etwas komplizierter. Zuerst berechnen wir den Support für c. Für alle Werte, die nicht im Support von c sind, ergibt die Multiplikation in der Definition von eval ebenfalls null. Daher sind diese Werte auch nicht im Support von Bind c f.

Im Support für den Konstruktor Bind können Duplikate vorkommen. Diese müssen entfernt werden, da sie zu falschen Ergebnissen führen würden. Zu diesem Zweck nutzen wir die Funktion distinct, die Duplikate aus einer Liste entfernt. Um Duplikate entfernen zu können, benötigen wir eine Funktion, um die Elemente der Liste vergleichen zu können. In der Prog-Struktur sind Vergleichsfunktionen, wie wir sie benötigen, vorhanden, wir müssen sie aber erst aus der Prog-Struktur extrahieren. Für diesen Zweck ist die folgende Funktion.

Fixpoint eqb_comp {A : Type} (comp : Comp A) : A -> A -> bool :=
  match comp with
  | Rnd n => BVeq n n
  | Ret eqb _ => eqb
  | Bind c f => eqb_prog (f (value c))
  end.

Im Fall des Konstruktors Rnd nutzen wir einfach eine vordefinierte Funktion zum Vergleich von Bit-Vektoren. Im Fall des Konstruktors Ret liefern wir die Funktion zurück, die im Konstruktor abgelegt wurde. Die Implementierung für den Konstruktor Bind stellt allerdings ein Problem dar. In der zweiten Komponente des Konstruktors steckt eine Funktion, aus der wir gern die Vergleichsfunktion extrahieren würden. Um dies zu erreichen müssen wir die Funktion allerdings anwenden. Zu diesem Zweck definieren wir die folgende Funktion. Diese Funktion liefert uns zu einem Wert vom Typ Comp A einen Wert vom Typ A. Es ist dabei unerheblich, welchen konkreten Wert wir zurückerhalten. Wir nutzen diesen Wert nur, um an ein Blatt der Comp-Struktur heranzukommen. In allen Blättern stecken die gleichen Vergleichsfunktionen, daher ist es irrelevant, welche Blatt wir aus der Struktur raussuchen.

Fixpoint value {A : Type} (comp : Comp A) : A :=
  match comp with
  | Rnd n => Bvect_false n
  | Ret _ a => a
  | Bind c f => value (f (value c))
  end.

Die Funktion Bvect_false liefert einen Bit-Vektor einer bestimmten Länge, der nur false als Einträge enthält. Im Fall des Konstruktors Ret haben wir einen konkreten Wert vom Typ A direkt zur Verfügung. Im Fall des Konstruktors Bind müssen wir wiederum auf die gleich Art und Weise einen Wert aus der Struktur extrahieren.

Perfect Secrecy

Das eigentliche Ziel einer Bibliothek zur Formulierung von Kryptoschemata ist nicht nur der Beweis der Korrektheit, sondern der Beweis von kryptografischen Eigenschaften. Wir betrachten hier als Beispiel eine sehr grundlegende Eigenschaft von Kryptoschemata, die als Perfect Secrecy bezeichnet wird. Wir geben wieder zuerst die Definition an und diskutieren anschließend seine Bedeutung.

Section Security.
  Variable Plaintext Key Ciphertext : Type.

  Variable Gen : Comp Key.
  Variable Enc : Key -> Plaintext -> Comp Ciphertext.

  Definition perfectly_secret : Prop :=
    forall (m m' : Plaintext), eq_comp (k <- Gen; Enc k m) (k <- Gen; Enc k m').
End Security.

Die Proposition perfectly_secret gibt an, wann ein Kryptoschema als perfectly secret bezeichnet wird. Die Definition verwendet nur einen Schlüssel-Generator Gen und eine Funktion zur Verschlüsselung Enc. Ein Kryptoschema wird als perfectly secret bezeichnet, wenn es die folgende Bedingung erfüllt. Wir generieren uns zweimal einen Schlüssel. Im einen Fall verschlüsseln wir eine Nachricht m mit diesem Schlüssel. Im anderen Fall verschlüsseln wir eine Nachricht m' mit dem Schlüssel. Das Kryptoschema als gilt als perfectly secret, falls die Wahrscheinlichkeitsverteilungen, dass ein bestimmter Geheimtext c entsteht in beiden Varianten identisch ist.

Zu guter Letzt wollen wir ein Theorem angeben, das besagt, dass das One-Time Pad perfectly secret ist.

Theorem otp_perfectly_secret :
    perfectly_secret Key Plaintext Ciphertext Gen Enc.