qssh 0.4.2

Post-quantum secure shell with NIST PQC algorithms (Falcon, SPHINCS+, ML-KEM), configurable security tiers, and quantum-resistant protocol design
Documentation

qssh

Post-Quantum SSH. Drop-in replacement. Formally verified.

qssh is a pure Rust implementation of SSH with post-quantum cryptography. It replaces OpenSSH's classical key exchange and authentication with quantum-resistant algorithms while maintaining full protocol compatibility.


Security notice (2026-09-13)

Every release before 0.4.2 defaults to a key exchange that provides no confidentiality. The FalconSignedShares exchange authenticates the peers, but derives the session key from values sent in cleartext, so a passive observer can reconstruct it. An ML-KEM exchange existed in the code, but the client hardcoded the default algorithm and never selected it. Found 2026-07-15, fixed on main 2026-07-16 (PR #5), released as 0.4.2 on 2026-09-13: ML-KEM-1024 is the default and the configured algorithm is honoured. Earlier crates.io versions are yanked; the v0.4.1 release, the Homebrew formula and the APT package built from the June tag are superseded. Upgrade, and treat any session made under an earlier default configuration as having had no confidentiality against a passive attacker. Details in CHANGELOG.md and SECURITY.md.

What It Does

Capability Detail
Key exchange ML-KEM-1024 (NIST FIPS 203)
Authentication Falcon-1024, SPHINCS+-256s
Encryption AES-256-GCM, ChaCha20-Poly1305
Tests 132 automated tests
Formal proofs 67 Lean 4 theorems, zero sorries, Mathlib v4.27.0
Patents None. Patent-free by design.
Dependencies Pure Rust. No OpenSSH fork, no C bindings.
3-tier verification Kani (panic-free), Verus (functional correctness), Lean 4 (mathematical foundations)

The Problem qssh Solves

Every SSH connection today uses RSA or ECDSA — both broken by Shor's algorithm on a sufficiently powerful quantum computer. The NIST deadline for PQC migration is 2035, but "harvest now, decrypt later" attacks mean data captured today can be decrypted retroactively.

qssh provides quantum-resistant SSH today. Not a patch on OpenSSH — a ground-up implementation with formal proofs that the cryptographic properties hold.

Formal Verification

Three levels of verification — no other SSH implementation offers this:

Level Tool What It Proves
Panic-free Kani (AWS) No execution path causes a crash
Functional correctness Verus (Microsoft Research) Code does exactly what it claims
Mathematical foundations Lean 4 + Mathlib Cryptographic properties are proven

Published on Zenodo: DOI 10.5281/zenodo.18663125

Related Work

qssh is part of the Paraxiom post-quantum infrastructure stack:

Project Description Theorems
qssl PQ TLS — 12 cipher suites 100
PQTG PQ Transport Gateway for QKD control channels 99
Drista PQ encrypted chat (ML-KEM-1024, STARK, Nostr+IPFS) 100
QuantumHarmony PQ L1 blockchain, live on 3 validators 76
Coherence Shield AI trust proxy with toroidal logit bias 115

Total: 909+ theorems across 10 systems. All Lean 4, all zero sorries.

Install

macOS / Linux (Homebrew)

brew tap paraxiom/tap
brew trust paraxiom/tap     # one-time: clears Homebrew's third-party-tap check
brew install qssh

Builds from source (Homebrew pulls in the Rust toolchain automatically). Works on macOS and on Linux via Homebrew — including ARM, where the .deb below is not yet published.

Debian / Ubuntu (APT)

curl -fsSL https://paraxiom.github.io/apt/paraxiom.gpg | sudo tee /usr/share/keyrings/paraxiom.gpg >/dev/null
echo "deb [signed-by=/usr/share/keyrings/paraxiom.gpg] https://paraxiom.github.io/apt stable main" \
  | sudo tee /etc/apt/sources.list.d/paraxiom.list
sudo apt-get update
sudo apt-get install qssh

This installs the qssh client, the qsshd daemon and the supporting tools, plus a systemd service for qsshd:

sudoedit /etc/qssh/qsshd.env     # set listen address / port
sudo systemctl start qsshd       # generates a Falcon-512 host key on first start

Standalone .deb

Download the .deb from Releases and:

sudo apt install ./qssh_*.deb

Building the package yourself and the APT-repo setup are documented in docs/PACKAGING.md and docs/APT-REPO.md.

Releases

Pre-built binaries are available under Releases.

Licence

Two regimes, at the recipient's choice: GPL-3.0-only (the default, reciprocal) or a Paraxiom commercial licence for products that cannot carry the GPL. See LICENSE.md.

We choose collaboration over extraction. If you're working on post-quantum infrastructure — whether in research, government, defence, or industry — write to sylvain@paraxiom.org with a brief description of your work. That door opens when you knock.

Citation

@misc{cormier2025qssh,
  author    = {Cormier, Sylvain},
  title     = {qssh: Post-Quantum SSH with 3-Tier Formal Verification},
  year      = {2025},
  publisher = {Paraxiom Technologies Inc.},
  url       = {https://github.com/Paraxiom/qssh}
}

Contact

Sylvain Cormier Paraxiom Technologies Inc. — Montreal sylvain@paraxiom.org | paraxiom.org