Was gebaut ist
Ein Nachweis ist das festgehaltene Ergebnis einer Prüfung von KALKÜL: Eine Handlung wurde gegen Regeln in einem Zustand gerechnet, und das Ergebnis liegt als Datensatz vor, der sich prüfen lässt, ohne dem System zu vertrauen.
Was er belegt
Begriff · Herkunft
Die Angabe zu einem Wert, aus welcher Quelle, welchem Objekt der Quelle und welchem Lauf er stammt. Herkunft belegt nicht, dass der Wert stimmt.
Er belegt, dass eine bestimmte Handlung in einem bestimmten Zustand unter bestimmten Annahmen die genannten Regeln in ihrer Version hält. Er belegt nicht, dass die Regeln die Vorschrift richtig wiedergeben, und nicht, dass der Zustand stimmt. Beides steht als Herkunft und Fundstelle im Datensatz, damit man es prüfen kann.
Drei Ergebnisse
Das Ergebnis ist bewiesen, widerlegt oder unentschieden. Bewiesen heißt, dass es keinen zulässigen Zustand gibt, in dem die Regel bricht. Widerlegt heißt, dass ein Gegenbeispiel vorliegt, und es gehört zum Nachweis. Unentschieden heißt, dass die Rechnung im Rahmen ihres Budgets nicht zum Ende kam, und es gibt keine Freigabe.
Woraus er besteht
Der Datensatz enthält die Handlung, den Zustand mit Herkunft, die Regeln mit Version, das Rechenmodell, die Einstellungen des Lösers, das Ergebnis und die Voraussetzungen. Er wird in eine kanonische Form gebracht, mit SHA-256 zu einem Prüfwert gerechnet, mit Ed25519 signiert und mit einem Zeitstempel nach RFC 3161 belegt.
Wer ihn prüft
Jeder, der den Datensatz, den öffentlichen Schlüssel und das Zeitstempeltoken hat. Er rechnet Prüfwert und Signatur nach und kann die Rechnung selbst wiederholen. Zugang zu KALKÜL braucht er dafür nicht.
Wovon er sich unterscheidet
Ein Nachweis ist kein Protokolleintrag: Ein Eintrag hält fest, dass etwas geschah, ein Nachweis, dass etwas vor der Handlung geprüft wurde. Er ist kein Zertifikat einer Stelle und keine Zusicherung des Betreibers. Und er ist kein Beweis im Sinn der Mathematik für die Wirklichkeit, sondern für die formalisierten Regeln.
Grenze
- Grenze
- Gebaut ist ein Demonstrator, der im Browser eine Bahn mit ihrer Unsicherheit gegen drei Regeln rechnet und einen SHA-256-Prüfwert über einen Beispieldatensatz bildet. Kanonische Form, Signatur, Zeitstempel und der Löser im Betrieb sind Bauweise.
Fragen
- Gibt es auch einen Nachweis für ein Nein?
- Ja. Ein Nein kommt mit der Belegung, die die Regel bricht, und sie ist Teil des Nachweises.
- Wie lange gilt ein Nachweis?
- Solange der Stand innerhalb seiner Voraussetzungen liegt. Verlässt er sie, gilt der Nachweis für die Ausführung nicht mehr.
Quellen
- RFC 8785: JSON Canonicalization SchemeIETF. Eindeutige Schreibweise für Prüfwerte und Signaturen.
- RFC 3161: Time-Stamp ProtocolIETF. Zeitstempel durch eine unabhängige Stelle.