Skip to main content

Crate kopis

Crate kopis 

Source
Expand description

§kopis-rs

This crate is a pure-Rust, no-std implementation of the Kopis key encapsulation mechanism (KEM). Kopis is a lattice-based KEM that is designed to be secure against classical and quantum adversaries. It comes in three variants:

  • Kopis-512, which is designed to have security roughly equivalent to AES-128
  • Kopis-768, which is designed to have security roughly equivalent to AES-192
  • Kopis-1024, which is designed to have security roughly equivalent to AES-256

§Example code

The following code can be found in examples/simple.rs.

use kopis::{
    kopis512::{Kopis512Ciphertext, Kopis512PublicKey, Kopis512SecretKey, KOPIS512_CIPHERTEXT_LEN},
    SharedSecret
};

let mut rng = rand::rng();

// Generate a keypair
let sk = Kopis512SecretKey::generate(&mut rng);
let pk = sk.public_key();

// Serialize the secret key, maybe to save on disk
let sk_seed: &[u8; 32] = sk.seed();

// Deserialize the secret key
let sk = Kopis512SecretKey::expand_from_seed(sk_seed);

// Also serialize and deserialize the public key
let mut pk_bytes = [0u8; Kopis512PublicKey::SERIALIZED_LEN];
pk.serialize(&mut pk_bytes);
let slice_containing_pk = pk_bytes.as_slice();
assert_eq!(
    slice_containing_pk.len(),
    Kopis512PublicKey::SERIALIZED_LEN
);
let pk_arr = slice_containing_pk.try_into().unwrap();
// The API only accepts fixed-len slices, so we have to cast it first
let pk = Kopis512PublicKey::from_bytes(pk_arr);

// Encapsulate a shared secret, ss1, to pk
let (ct, ss1): (Kopis512Ciphertext, SharedSecret) = pk.encapsulate(&mut rng);
// Note ct is just a [u8; KOPIS512_CIPHERTEXT_LEN]

// Deserializing is also straightforward
let slice_containing_ct = ct.as_slice();
let receiver_ct: &Kopis512Ciphertext = slice_containing_ct.try_into().unwrap();

// Use the secret key to decapsulate the ciphertext
let ss2 = sk.decapsulate(receiver_ct);

// Check the shared secrets are equal. NOTE is not a constant-time check (ie not secure). We
// only do this for testing purposes.
assert_eq!(ss1.as_bytes(), ss2.as_bytes());

println!("KEM ran successfully");

§Benchmarks

We have implemented benchmarks for key generation, encapsulation, and decapsulation for all variants. Simply run cargo bench.

§Formal Verification

We use aeneas to extract our Rust implementation to Lean. After making changes to the Rust, run extract_rust_to_lean.sh, which regenerates lean/ExtractedRust.lean.

That extracted code is then proved to match an audited Lean specification of Kopis. The proofs live in lean/; see lean/README.md for the layout. To check them:

cd lean
make prove-kopis      # build + kernel-verify the correspondence proofs
make test-kopis-spec  # run the audited spec against the Kopis test vectors

§License

Licensed under either of

at your option.

Modules§

kopis512
Kopis-512 is designed to have security close to that of AES-128
kopis768
Kopis-768 is designed to have security close to that of AES-192
kopis1024
Kopis-1024 is designed to have security close to that of AES-256

Structs§

SharedSecret
A shared secret of a KEM execution. This is just a [u8; 32] that zeroes itself from memory when it goes out of scope.