Nachweis: signiert und ohne SnapSite prüfbar

Was gebaut ist

Ein Nachweis hält das Ergebnis einer Prüfung so fest, dass es jemand ohne Zugang zu KALKÜL und ohne Vertrauen in das System nachrechnen kann. Dieser geplante Vertrag legt fest, was in den Datensatz gehört, wie er geschrieben wird und womit er geprüft wird.

Ein geplanter Vertrag, kein erreichbarer Endpunkt

Begriff · Nachweis

Der signierte Datensatz einer Prüfung: Handlung, Zustand, Regeln, Ergebnis und Voraussetzungen, mit Prüfwert, Signatur und Zeitstempel. Er lässt sich ohne Zugang zum System nachrechnen.

Nachweis im Zusammenhang

Die Felder beschreiben die vorgesehene Form eines Nachweises. Der Demonstrator von KALKÜL rechnet einen SHA-256-Prüfwert über einen Beispieldatensatz, den ein Test unabhängig nachrechnet. Kanonische Form, Signatur und Zeitstempel sind Bauweise und noch nicht gebaut.

Was in den Datensatz gehört

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.

Herkunft im Zusammenhang

Der Datensatz enthält alles, was zum Nachrechnen nötig ist: die Handlung mit ihren Parametern, den Zustand mit Herkunft und Erfassungszeit, die Regeln in ihrer Version, das Rechenmodell mit Version, die Einstellungen der Rechnung und das Ergebnis. Das Ergebnis ist ein Nachweis, ein Gegenbeispiel oder unentschieden, und bei einem Gegenbeispiel ist die Belegung Teil des Datensatzes. Dazu kommen die Voraussetzungen, unter denen der Nachweis gilt, also die Intervalle der Annahmen.

Kanonisch, Prüfwert, Signatur

Der Datensatz wird nach dem JSON Canonicalization Scheme (RFC 8785) in eine eindeutige Form gebracht. Über sie wird SHA-256 gerechnet (FIPS 180-4), der Prüfwert wird mit Ed25519 signiert (RFC 8032). Die Signatur hat 64 Byte, der öffentliche Schlüssel 32 Byte, und der Schlüssel trägt einen Gültigkeitszeitraum, damit auch ältere Nachweise prüfbar bleiben.

Zeitstempel

Ein Zeitstempel nach RFC 3161 bestätigt, dass der Prüfwert der Signatur zu einem Zeitpunkt vorlag. Er wird von einem unabhängigen Dienst ausgestellt und hängt als Token am Nachweis. Ein qualifizierter Zeitstempel nach der eIDAS-Verordnung kommt von einem qualifizierten Vertrauensdiensteanbieter; welcher, entscheidet der Betreiber.

Prüfen durch Dritte

Wer prüft, bildet die kanonische Form, rechnet SHA-256, prüft die Signatur mit dem öffentlichen Schlüssel und das Token des Zeitstempels. Danach prüft sie, ob der aktuelle Stand noch innerhalb der Voraussetzungen liegt, falls der Nachweis zur Ausführung dient. Keiner dieser Schritte braucht Zugang zu KALKÜL. Das Ergebnis selbst lässt sich nachrechnen: ein Gegenbeispiel durch Einsetzen, ein Nachweis mit einem eigenen Löser.

Schema

{
  "id": "<nachweis-kennung>",
  "kind": "proof",
  "action": { "actionType": "<objekttyp>.<operation>.v1", "input": { } },
  "state": { "ref": "<zustand>", "digest": "sha256:<wert>" },
  "rules": [{ "id": "<regel>", "version": <nummer> }],
  "computation": { "name": "<rechenmodell>", "version": "<nummer>" },
  "solver": { "name": "<loeser>", "version": "<nummer>", "budget": "<dauer>", "seed": <startwert> },
  "assumptions": [{ "name": "<annahme>", "interval": [<von>, <bis>] }],
  "canonicalization": "JCS-RFC8785",
  "digest": "sha256:<wert>",
  "signature": { "alg": "Ed25519", "keyId": "<schluessel>", "value": "<base64url>" },
  "timestamp": { "type": "RFC3161", "token": "<base64url>" }
}

Schema 1JSON · Schema mit Platzhaltern

Felder

Feld	Typ	Pflicht	Bedeutung
`id`	`string`	ja	Kennung des Nachweises.
`kind`	`string`	ja	proof, counterexample oder undecided. Ein Nein ohne Belegung gibt es nicht.
`action`	`object`	ja	Die geprüfte Handlung mit Typ und Parametern.
`state`	`object`	ja	Verweis auf den Zustand mit Herkunft und Erfassungszeit, dazu sein Prüfwert.
`rules`	`object[]`	ja	Regeln mit Version, gegen die gerechnet wurde.
`computation`	`object`	ja	Rechenmodell mit Name und Version.
`solver`	`object`	ja	Löser mit Version, Rechenbudget und Startwert. Dieselben Eingaben führen bei gleicher Einstellung zum selben Ergebnis.
`counterexample`	`object`	nein	Belegung oder Kasten, der die Regel bricht. Nur bei counterexample.
`assumptions`	`object[]`	nein	Voraussetzungen als Intervalle. Der Nachweis gilt nur innerhalb.
`canonicalization`	`string`	ja	Verfahren der kanonischen Form, hier JCS nach RFC 8785.
`digest`	`string`	ja	SHA-256 über die kanonische Form.
`signature`	`object`	ja	Verfahren, Kennung des öffentlichen Schlüssels und Wert, Ed25519 nach RFC 8032.
`timestamp`	`object`	nein	Token nach RFC 3161 über den Prüfwert der Signatur.

Fehlerfälle

Kennung	Bedeutung
`PROOF_DIGEST_MISMATCH`	Der Prüfwert der kanonischen Form stimmt nicht mit dem im Nachweis überein.
`PROOF_SIGNATURE_INVALID`	Die Signatur passt nicht zum Prüfwert und zum öffentlichen Schlüssel.
`PROOF_TIMESTAMP_INVALID`	Das Token passt nicht zur Signatur oder ist nicht gültig signiert.
`PROOF_ASSUMPTION_VIOLATED`	Der aktuelle Stand liegt außerhalb der Voraussetzungen; der Nachweis gilt nicht für die Ausführung.
`PROOF_RULE_UNKNOWN`	Die genannte Version einer Regel liegt dem Prüfer nicht vor.

Grenze

Grenze: Dieser Schnittstellenvertrag ist geplant. Er belegt weder eine veröffentlichte Schnittstelle noch eine Signatur mit einem Schlüssel im Hardware-Sicherheitsmodul oder einen Zeitstempeldienst. Ein Nachweis zeigt, dass eine Rechnung mit diesen Regeln und diesem Zustand so ausgegangen ist; dass die Regeln die Vorschrift richtig wiedergeben, zeigt er nicht.

Quellen

RFC 8785: JSON Canonicalization SchemeIETF. Eindeutige Schreibweise von JSON für Prüfwerte und Signaturen.
RFC 8032: Edwards-Curve Digital Signature AlgorithmIETF. Ed25519.
RFC 3161: Time-Stamp ProtocolIETF. Zeitstempel durch eine unabhängige Stelle.
FIPS 180-4: Secure Hash StandardNIST. SHA-256.

Ein Nachweis ist signiert und ohne SnapSite prüfbar.