ProvenCrypto.jl

Formally verified cryptographic protocols and post-quantum primitives for Julia.

Table of Contents

• Features
  • Post-Quantum Cryptography
  • Protocol Implementations
  • Zero-Knowledge Proofs
  • Threshold Cryptography
  • Hardware Acceleration
  • Formal Verification
• Installation
  • System Dependencies
• Usage
  • Post-Quantum Key Exchange (Kyber)
  • Post-Quantum Signatures (Dilithium)
  • Authenticated Encryption (libsodium FFI)
  • Hardware-Accelerated Operations
• Security Warnings
• Containerized Execution
• Formal Verification
• Architecture
• Development
• References
• License

Features

Post-Quantum Cryptography

• Kyber — KEM (Key Encapsulation Mechanism), NIST PQC winner

• Dilithium — Digital signatures, NIST PQC winner

• SPHINCS+ — Hash-based signatures (conservative security)

Protocol Implementations

• Noise Protocol Framework — Modern secure channel (WireGuard, Lightning)

• Signal Protocol — Double Ratchet for messaging

• TLS 1.3 — Reference implementation (educational)

Zero-Knowledge Proofs

• zk-SNARKs — Groth16, PLONK, Halo2

• zk-STARKs — Transparent, post-quantum secure

Threshold Cryptography

• Shamir Secret Sharing — M-of-N key recovery

• Distributed Key Generation — Multi-party computation

Hardware Acceleration

• GPU — CUDA (NVIDIA), ROCm (AMD), Metal (Apple)

• NPU/TPU — Intel oneAPI, Google TPU, Apple Neural Engine

• Crypto Instructions — AES-NI, SHA extensions, Intel QAT

• Secure Enclaves — Intel SGX, AMD SEV, ARM TrustZone

• Multi-platform — x86, ARM, RISC-V, Apple Silicon

Formal Verification

• SMT Integration — Z3, CVC5, Yices, MathSAT

• Proof Assistants — Idris 2, Lean 4, Coq, Isabelle/HOL

• Property Verification — Correctness, security properties

• Proof Export — Long-term formalization

Installation

using Pkg
Pkg.add(url="https://github.com/hyperpolymath/ProvenCrypto.jl")

System Dependencies

libsodium is required for primitives:

# macOS
brew install libsodium

# Ubuntu/Debian
sudo apt install libsodium-dev

# Fedora
sudo dnf install libsodium-devel

# Arch
sudo pacman -S libsodium

Usage

Post-Quantum Key Exchange (Kyber)

using ProvenCrypto

# Generate keypair
(pk, sk) = kyber_keygen(768)  # AES-192 equivalent security

# Sender: Encapsulate shared secret
(ciphertext, shared_secret_sender) = kyber_encapsulate(pk)

# Receiver: Decapsulate
shared_secret_receiver = kyber_decapsulate(sk, ciphertext)

@assert shared_secret_sender == shared_secret_receiver

Post-Quantum Signatures (Dilithium)

using ProvenCrypto

# Generate signing keypair
(pk, sk) = dilithium_keygen(3)  # AES-192 equivalent security

# Sign message
message = b"Hello, post-quantum world!"
signature = dilithium_sign(sk, message)

# Verify
is_valid = dilithium_verify(pk, message, signature)
@assert is_valid

Authenticated Encryption (libsodium FFI)

using ProvenCrypto

# Generate key and nonce
key = rand(UInt8, 32)
nonce = rand(UInt8, 12)  # Must be unique per message!

# Encrypt
plaintext = b"Secret message"
ciphertext = aead_encrypt(key, nonce, plaintext)

# Decrypt
recovered = aead_decrypt(key, nonce, ciphertext)
@assert recovered == plaintext

Hardware-Accelerated Operations

using ProvenCrypto

# Detect available hardware
backend = detect_hardware()
println(backend)
# Output: MetalBackend(M3 + Neural Engine)
#     or: CUDABackend(device=0, CC=8.9)
#     or: CPUBackend(avx512, 16 threads)

# Operations automatically use best backend
features = detect_hardware_features()
print_hardware_report(features)

Security Warnings

Warning

Production Use — This library is for research and educational purposes. For production systems, use libsodium (symmetric crypto), OpenSSL FIPS module (classical asymmetric), or Argon2 C library (memory-hard KDFs) via FFI wrappers provided in this library.

Note	Not FIPS-Certified — Pure Julia implementations are NOT FIPS 140-2/3 certified. For compliance-critical systems, use FIPS-certified libraries via FFI.

What is safe to use:

• FFI wrappers to proven libraries (libsodium, BoringSSL)

• Post-quantum reference implementations (research, interoperability)

• Protocol verification and formal analysis

• Standards compliance testing

Containerized Execution

For maximum security isolation, run cryptographic operations in the verified container:

# Build container
cd verified-container-spec/examples/proven-crypto-runner
podman build -t proven-crypto-runner -f Containerfile

# Run with svalinn/vordr security policy
svalinn run --policy svalinn-policy.json \
    -v ./ProvenCrypto.jl:/crypto/provencrypto:ro \
    proven-crypto-runner keygen

# Interactive REPL
podman run -it -v ./ProvenCrypto.jl:/crypto/provencrypto:ro \
    proven-crypto-runner repl

Security features: process isolation (PID/network/mount/IPC/UTS/user namespaces), seccomp filters, resource limits (1 CPU, 2GB RAM, 512 processes), no capabilities, reproducible builds (Guix + Nix fallback).

Formal Verification

Export verification certificates to proof assistants:

using ProvenCrypto

cert = ProofCertificate(
    property="Kyber decapsulation correctness",
    specification="∀pk,sk,c,ss. decapsulate(sk, fst(encapsulate(pk))) = snd(encapsulate(pk))",
    verified=true,
    verifier="SMT-Z3",
    timestamp=now(),
    metadata=Dict()
)

export_idris(cert, "proofs/kyber_correctness.idr")
export_lean(cert, "proofs/kyber_correctness.lean")
export_coq(cert, "proofs/kyber_correctness.v")

Architecture

Layer	Components
Layer 1: Verified Primitives (FFI)	libsodium, BoringSSL, Argon2
Layer 2: Protocols (Pure Julia)	Noise, Signal, TLS 1.3 (uses Layer 1)
Layer 3: Post-Quantum (Pure Julia + Verification)	Kyber, Dilithium, SPHINCS+; GPU/TPU/NPU-accelerated NTT

Development

# Tests
julia --project -e 'using Pkg; Pkg.test("ProvenCrypto")'

# Benchmarks
julia --project benchmark/benchmarks.jl

# Documentation
julia --project docs/make.jl

References

• NIST Post-Quantum Cryptography

• Kyber Specification

• Dilithium Specification

• SPHINCS+ Specification

• Noise Protocol Framework

• Signal Protocol

• libsodium

• Idris 2

Wondering how this works? See EXPLAINME.adoc.

License

SPDX-License-Identifier: MPL-2.0
See LICENSE.