Abstractions Lab announces the first release of PQC-MAT (v0.1), now available on GitHub.
PQC-MAT introduces VECTOR — VErified Cryptography and Transition via Observable Registry — an open-source toolkit for inventorying cryptographic assets, assessing quantum risk exposure, and beginning a methodological migration to post-quantum cryptography (PQC).
What Is PQC-MAT?
PQC-MAT (Post-Quantum Cryptography Migration Assistance Theory and Tools) is a sub-project of CyFORT, carried out under the EU IPCEI-CIS initiative. It provides resources and tools for a secure migration from classical public-key cryptography to quantum-resistant alternatives in cyber-physical systems.
The urgency is real. “Harvest Now, Decrypt Later” (HNDL) adversaries are already collecting today’s encrypted traffic for future decryption once a Cryptographically Relevant Quantum Computer (CRQC) becomes available. Shor’s algorithm would break the asymmetric primitives underpinning modern infrastructure — RSA, ECDH, ECDSA, EdDSA — and NIST, BSI, and ANSSI all recommend starting migration now. In August 2024, NIST published the first finalized PQC standards (FIPS 203, 204, 205). Without a cryptographic inventory, organizations cannot assess their exposure or plan the transition. VECTOR closes that gap.
Key Highlights
TOR (Transition via Observable Registry) is the cryptographic inventory engine. It discovers assets across source code and network infrastructure, generating standardized Cryptographic Bills of Materials (CBOM) in CycloneDX 1.6 format via three tools operating under a unified vector CLI:
VECTOR-Code orchestrates cloc, CodeQL with cryptographic queries, and cryptobom-forge into a single command for Python, C, and C++ projects. One CBOM per detected language, plus SARIF findings and CodeQL databases.
VECTOR-Network fills a notable gap: no widely available tool converts testssl.sh or ZGrab2 output to CycloneDX CBOM. VECTOR-Network’s custom parsers decompose each TLS cipher suite into individual algorithm components (key exchange, authentication, encryption, MAC), detect standalone post-quantum KEMs (ML-KEM-512/768/1024), and split hybrid schemes such as X25519MLKEM768 and SecP256r1MLKEM768 into their constituent classical EC and PQC KEM parts.
VECTOR-Score reads any CycloneDX 1.6 CBOM and classifies each algorithm against a data-driven YAML catalog aligned with NIST FIPS 203/204/205, BSI TR-02102-1, and ANSSI. Seven classifications cover the full spectrum from quantum-vulnerable and classically-deprecated (immediate action) through quantum-weakened (review) to quantum-safe, post-quantum, and hybrid (no action needed). The annotated output CBOM carries rationale, migration recommendations, and normative references per component; a Markdown risk report summarizes the findings. The CBOM output of vector code or vector network feeds directly into vector score.
VEC (Verified Cryptography) demonstrates the use of F* for producing mathematically verified cryptographic implementations. The worked example covers the Extended Euclidean Algorithm — a foundational primitive in asymmetric cryptography — with explicit pre/post-conditions, SMT-assisted termination and correctness proofs, and automatic extraction of verified OCaml code.
PQC-MAT runs entirely inside a Docker Dev Container with all dependencies pre-installed. Opening the project in VS Code and selecting “Dev Containers: Reopen in Container” is all that is required to start.
Availability
PQC-MAT is available as a free and open-source release on GitHub:
https://github.com/AbstractionsLab/pqc-mat
Technical specifications and requirements traceability are available on the PQC-MAT traceability web page.
Community feedback and contributions are welcome.