SJP Signatures and Verification

This page describes the implementation at SekuraJS source revision 6dd5716a8f3bcf29d27ae9ca64800bb517601236.

Documentation version: 1.0

1. Two separate checks

verify-sjp checks both a cryptographic signature and the mathematical queries stored in the package. These checks answer different questions:

• Signature check: Does the SJP manifest verify under the Ed25519 public key embedded in its attestation, and is that public key exactly the one the caller supplied with --trusted-key?
• SMT replay: Do the SMT queries stored in the package reproduce their recorded results when run again through Z3, and optionally CVC5?

A valid signature does not by itself show that a proof query is mathematically valid. A successful SMT replay does not identify or authenticate the person who created the package. Replay checks the stored formulas; it does not regenerate them from source or prove that the source-to-formula translation was correct. See the SJP package format for the replay boundary.

2. Key generation

Generate an Ed25519 keypair with:

sekura-sjv keygen-ed25519 signing.secret signing.public

The current implementation uses libsodium and writes:

• signing.secret: the 64-byte binary Ed25519 secret key. The file is set to owner read/write permissions.
• signing.public: the 32-byte public key encoded as 64 hexadecimal characters followed by a newline.

The two paths must differ, and neither output file may already exist. The secret key is required by sign-sjp; the public key is required by verify-sjp. The CLI does not provide a key import/export or key-store command.

3. Create and sign an SJP

make-sjv writes an unsigned SJP v2 ZIP package. It does not sign the package. To make a package accepted by verify-sjp, generate a signed copy:

sekura-sjv make-sjv model.sjv program.sobj proof.sjp
sekura-sjv sign-sjp proof.sjp signing.secret proof.signed.sjp

For a SystemVerilog SJV source, the make-sjv form takes the SJV and output SJP path, with optional SV build options. For the SJS/SOBJ path, it takes the SJV, SOBJ, output SJP path, and optionally an environment JSON file.

sign-sjp accepts an unsigned SJP v2 ZIP and a 64-byte binary secret key. It refuses an already signed SJP and requires the output path to differ from the input path. It writes attestation.json into the copied package. The legacy line-oriented SJP v1 representation cannot be signed.

4. Attestation contents and signed bytes

The current attestation.json contains:

• attestation_version: 1;
• algorithm: Ed25519;
• context: Sekura SJP attestation v1;
• key_id: sha256: followed by the SHA-256 digest of the 32-byte public key;
• manifest_sha256: sha256: followed by the SHA-256 digest of the exact manifest.json bytes;
• public_key_hex: the 32-byte public key in hexadecimal;
• signature_hex: the detached Ed25519 signature in hexadecimal.

The signed message is the bytes of Sekura SJP attestation v1, followed by a NUL byte, followed by the exact bytes of manifest.json. The signature directly covers that message. The manifest contains hashes for each stored SMT payload and embedded dependency package, so replay checks those payload bytes against the manifest. The signature is not a signature over every byte of the outer ZIP file; ZIP CRC-32 is used to detect entry corruption, not as a cryptographic signature.

Changing the exact manifest bytes invalidates the signature. Changing a referenced SMT payload or embedded child package causes its manifest hash check to fail. Repacking an unchanged manifest and unchanged package members does not, by itself, change the signed message.

5. Verify the signature and replay the package

Use:

sekura-sjv verify-sjp proof.signed.sjp --trusted-key signing.public

The --trusted-key argument is required. The key file may contain either 32 raw bytes or 64 hexadecimal digits. verify-sjp performs these steps:

1. Reads the package and requires an SJP v2 ZIP containing manifest.json and attestation.json.
2. Checks attestation version, algorithm, context, public-key/signature sizes, key_id, and manifest_sha256.
3. Verifies the Ed25519 signature using the public key embedded in the attestation.
4. Compares that embedded public key with the key supplied by the caller. If they differ, verification fails.
5. Replays the stored SMT queries through Z3 and checks the replay results against the recorded results.

The command rejects unsigned packages and packages verified with a different supplied public key. It does not offer an “accept any mathematically valid signature” mode: omitting --trusted-key is an error.

SJP replay requires Z3. To request a second solver replay through CVC5 as well, run:

sekura-sjv verify-sjp proof.signed.sjp --trusted-key signing.public --cross-check-cvc5

This option requires the cvc5 executable on PATH. CVC5 cross-checking supplements the required Z3 replay; it does not replace the signature check.

6. Signature validity is not signer identity

sekura-sjv does not act as a public-key infrastructure (PKI), certificate authority, or organizational identity service. It does not issue certificates, maintain a trusted-key registry, map keys to people or organizations, revoke keys, or decide how a key was obtained.

A successful verify-sjp signature check establishes that:

• the attestation contains a valid Ed25519 signature for the exact manifest bytes; and
• the embedded public key matches the public key explicitly selected by the caller.

The caller or its organization must decide whether that supplied public key belongs to an authorized signer. The key_id is a SHA-256 fingerprint of the public key; it is not a certificate or an identity assertion.

For SJP files with embedded dependency packages, the verifier also checks child attestations cryptographically during replay. The root --trusted-key is not compared with child package keys. If an application requires signer identity checks for child packages, it must apply its own key-selection policy to those packages.

7. Command outcomes

For verify-sjp:

For keygen-ed25519 and sign-sjp, status 0 means the requested files were written; invalid paths, keys, packages, or I/O errors return status 1.

8. Notes on use

• Keep signing.secret private and make a protected backup according to your organization’s policy.
• Distribute signing.public through a channel your organization controls. Do not treat an SJP’s embedded public key alone as proof of who signed it.
• Re-run verify-sjp with the public key your organization selected for that package.
• Store and review the recorded verification scope and original inputs separately as needed; the signature only authenticates the manifest bytes, and replay only rechecks its included SMT queries.

9. Implementation references

Checked against the source revision identified above:

• src-sjv/cli/cli.cpp — key generation, attestation creation and parsing, public-key comparison, and command exit paths;
• src-sjv/core/sjp.cpp — signed-content loading, ZIP integrity checks, manifest/payload replay, and dependency replay;
• tests/sjv_cli_test.cpp — checks for unsigned SJP rejection, valid signing/replay, corrupted signature rejection, missing trusted key, and wrong-key rejection.

No tests or site build were run while preparing this reference.