diff --git a/Cargo.lock b/Cargo.lock index f1b5c3267..650c92551 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -109,6 +109,12 @@ dependencies = [ "serde", ] +[[package]] +name = "bumpalo" +version = "3.14.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7f30e7476521f6f8af1a1c4c0b8cc94f0bee37d91763d0ca2665f299b6cd8aec" + [[package]] name = "camino" version = "1.1.6" @@ -167,6 +173,16 @@ dependencies = [ "thiserror", ] +[[package]] +name = "cc" +version = "1.0.83" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f1174fb0b6ec23863f8b971027804a42614e347eafb0a95bf0b12cdae21fc4d0" +dependencies = [ + "jobserver", + "libc", +] + [[package]] name = "cfg-if" version = "1.0.0" @@ -401,8 +417,10 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "be4136b2a15dd319360be1c07d9933517ccf0be8f16bf62a3bee4f0d618df427" dependencies = [ "cfg-if", + "js-sys", "libc", "wasi", + "wasm-bindgen", ] [[package]] @@ -556,6 +574,9 @@ dependencies = [ [[package]] name = "hax-lib-protocol" version = "0.1.0-pre.1" +dependencies = [ + "libcrux", +] [[package]] name = "hax-lib-protocol-macros" @@ -696,6 +717,24 @@ version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38" +[[package]] +name = "jobserver" +version = "0.1.27" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8c37f63953c4c63420ed5fd3d6d398c719489b9f872b9fa683262f8edd363c7d" +dependencies = [ + "libc", +] + +[[package]] +name = "js-sys" +version = "0.3.67" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a1d36f1235bc969acba30b7f5990b864423a6068a10f7c90ae8f0112e3a59d1" +dependencies = [ + "wasm-bindgen", +] + [[package]] name = "lazy_static" version = "1.4.0" @@ -708,6 +747,48 @@ version = "0.2.152" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "13e3bf6590cbc649f4d1a3eefc9d5d6eb746f5200ffb04e5e142700b8faa56e7" +[[package]] +name = "libcrux" +version = "0.0.2-pre.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "31d9dcd435758db03438089760c55a45e6bcab7e4e299ee261f75225ab29d482" +dependencies = [ + "getrandom", + "libcrux-hacl", + "libcrux-platform", + "libjade-sys", + "rand", +] + +[[package]] +name = "libcrux-hacl" +version = "0.0.2-pre.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "52b2581ce493c5c22700077b5552b47be69b67b8176716572b02856218db0b68" +dependencies = [ + "cc", + "libcrux-platform", +] + +[[package]] +name = "libcrux-platform" +version = "0.0.2-pre.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "647e39666194b11df17c19451d1154b9be79df98b9821532560c2ecad0cf3410" +dependencies = [ + "libc", +] + +[[package]] +name = "libjade-sys" +version = "0.0.2-pre.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ec4d22bba476bf8f5aebe36ccfd0e56dba8707e0c3b5c76996576028f48ffb8e" +dependencies = [ + "cc", + "libcrux-platform", +] + [[package]] name = "libtest-mimic" version = "0.6.1" @@ -856,6 +937,12 @@ version = "0.2.13" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8afb450f006bf6385ca15ef45d71d2288452bc3683ce2e2cacc0d18e4be60b58" +[[package]] +name = "ppv-lite86" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5b40af805b3121feab8a3c29f04d8ad262fa8e0561883e7653e024ae4479e6de" + [[package]] name = "predicates" version = "3.0.4" @@ -926,6 +1013,36 @@ dependencies = [ "proc-macro2", ] +[[package]] +name = "rand" +version = "0.8.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404" +dependencies = [ + "libc", + "rand_chacha", + "rand_core", +] + +[[package]] +name = "rand_chacha" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88" +dependencies = [ + "ppv-lite86", + "rand_core", +] + +[[package]] +name = "rand_core" +version = "0.6.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" +dependencies = [ + "getrandom", +] + [[package]] name = "redox_syscall" version = "0.4.1" @@ -1437,6 +1554,60 @@ version = "0.11.0+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" +[[package]] +name = "wasm-bindgen" +version = "0.2.90" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b1223296a201415c7fad14792dbefaace9bd52b62d33453ade1c5b5f07555406" +dependencies = [ + "cfg-if", + "wasm-bindgen-macro", +] + +[[package]] +name = "wasm-bindgen-backend" +version = "0.2.90" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fcdc935b63408d58a32f8cc9738a0bffd8f05cc7c002086c6ef20b7312ad9dcd" +dependencies = [ + "bumpalo", + "log", + "once_cell", + "proc-macro2", + "quote", + "syn 2.0.38", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-macro" +version = "0.2.90" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3e4c238561b2d428924c49815533a8b9121c664599558a5d9ec51f8a1740a999" +dependencies = [ + "quote", + "wasm-bindgen-macro-support", +] + +[[package]] +name = "wasm-bindgen-macro-support" +version = "0.2.90" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bae1abb6806dc1ad9e560ed242107c0f6c84335f1749dd4e8ddb012ebd5e25a7" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.38", + "wasm-bindgen-backend", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-shared" +version = "0.2.90" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4d91413b1c31d7539ba5ef2451af3f0b833a005eb27a631cec32bc0635a8602b" + [[package]] name = "which" version = "4.4.2" diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index 534aad389..e8e702346 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/engine/backends/proverif/proverif_backend.ml @@ -10,6 +10,7 @@ include include On.Macro include On.Question_mark include On.Early_exit + include On.Slice end) (struct let backend = Diagnostics.Backend.ProVerif @@ -30,6 +31,7 @@ module SubtypeToInputLanguage (* and type slice = Features.Off.slice *) (* and type raw_pointer = Features.Off.raw_pointer *) with type early_exit = Features.On.early_exit + and type slice = Features.On.slice and type question_mark = Features.On.question_mark and type macro = Features.On.macro (* and type as_pattern = Features.Off.as_pattern *) @@ -61,7 +63,6 @@ struct let mutable_reference = reject let mutable_pointer = reject let reference = reject - let slice = reject let raw_pointer = reject let as_pattern = reject let nontrivial_lhs = reject @@ -286,17 +287,6 @@ module Print = struct | TApp _ -> super#ty ctx ty | _ -> string "bitstring" - method! expr_app : expr -> expr list -> generic_value list fn = - fun f args _generic_args -> - let args = - separate_map - (comma ^^ break 1) - (print#expr_at Expr_App_arg >> group) - args - in - let f = print#expr_at Expr_App_f f |> group in - f ^^ iblock parens args - method! literal : Generic_printer_base.literal_ctx -> literal fn = fun _ctx -> function | Int { value; negative; _ } -> diff --git a/hax-lib-protocol/Cargo.toml b/hax-lib-protocol/Cargo.toml index 8f5c11cda..073e1fbba 100644 --- a/hax-lib-protocol/Cargo.toml +++ b/hax-lib-protocol/Cargo.toml @@ -11,3 +11,4 @@ readme.workspace = true # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] +libcrux = "0.0.2-pre.2" diff --git a/hax-lib-protocol/README.md b/hax-lib-protocol/README.md new file mode 100644 index 000000000..f867250b7 --- /dev/null +++ b/hax-lib-protocol/README.md @@ -0,0 +1,19 @@ +# Hax Protocol Library +This crate provides tools for protocol developers to write protcol +specifications for hax. + +## Protocol Traits +To hax, a protocol is a collection of communicating state +machines. This module provides traits that describe parts of a state +machine's behaviour, specifically it provides traits for creating an +initial state, and for state transition behaviour when reading or +writing a message. + +## Cryptographic Abstractions +Beside message passing and state transitions, a protocol of course +includes operations on the sent and received messages. For +cryptographic protocols, these will be of a fairly restricted set of +cryptoraphic primitive operations, which are provided in these +cryptographic abstractions. This allows protocol authors to specify +protocol party internal operations in a way that is easily accessible +to hax. diff --git a/hax-lib-protocol/src/crypto.rs b/hax-lib-protocol/src/crypto.rs new file mode 100644 index 000000000..47ad118e6 --- /dev/null +++ b/hax-lib-protocol/src/crypto.rs @@ -0,0 +1,194 @@ +//! This module defines a cryptographic abstraction layer for use in +//! hax protocol specifications. + +use crate::ProtocolError; + +/// An abstract Diffie-Hellman scalar. +#[derive(Clone)] +pub struct DHScalar(Vec); + +impl DHScalar { + /// Wrap bytes into a Diffie-Hellman scalar. Does *not* perform + /// input validation. + pub fn from_bytes(bytes: &[u8]) -> Self { + DHScalar(bytes.to_vec()) + } +} + +/// An abstract Diffie-Hellman group element. +pub struct DHElement(Vec); + +impl DHElement { + /// Wrap bytes into a Diffie-Hellman group element. Does *not* perform + /// input validation. + pub fn from_bytes(bytes: &[u8]) -> Self { + DHElement(bytes.to_vec()) + } +} + +/// Choice of Diffie-Hellman groups. +pub enum DHGroup { + X25519, + X448, + P256, + P384, + P521, +} + +impl From for libcrux::ecdh::Algorithm { + /// Converter to `libcrux` type. + fn from(value: DHGroup) -> Self { + match value { + DHGroup::X25519 => libcrux::ecdh::Algorithm::X25519, + DHGroup::X448 => libcrux::ecdh::Algorithm::X448, + DHGroup::P256 => libcrux::ecdh::Algorithm::P256, + DHGroup::P384 => libcrux::ecdh::Algorithm::P384, + DHGroup::P521 => libcrux::ecdh::Algorithm::P521, + } + } +} + +/// Scalar multiplication of `scalar` and `element`. +pub fn dh_scalar_multiply(group: DHGroup, scalar: DHScalar, element: DHElement) -> Vec { + libcrux::ecdh::derive(group.into(), element.0, scalar.0).unwrap() +} + +/// Scalar multiplication of a fixed generator and `scalar`. +pub fn dh_scalar_multiply_base(group: DHGroup, scalar: DHScalar) -> Vec { + libcrux::ecdh::secret_to_public(group.into(), scalar.0).unwrap() +} + +/// An abstract AEAD key. +pub struct AEADKey(libcrux::aead::Key); + +/// Choice of AEAD algorithms. +pub enum AEADAlgorithm { + Aes128Gcm, + Aes256Gcm, + Chacha20Poly1305, +} + +impl From for libcrux::aead::Algorithm { + /// Converter to `libcrux` type. + fn from(value: AEADAlgorithm) -> Self { + match value { + AEADAlgorithm::Aes128Gcm => libcrux::aead::Algorithm::Aes128Gcm, + AEADAlgorithm::Aes256Gcm => libcrux::aead::Algorithm::Aes256Gcm, + AEADAlgorithm::Chacha20Poly1305 => libcrux::aead::Algorithm::Chacha20Poly1305, + } + } +} + +impl AEADKey { + /// Attempt deserialization of `bytes` into an AEAD key for + /// `algorithm`. Panics on failure. + pub fn from_bytes(algorithm: AEADAlgorithm, bytes: &[u8]) -> Self { + AEADKey(libcrux::aead::Key::from_bytes(algorithm.into(), bytes.to_vec()).unwrap()) + } +} + +/// An abstract AEAD initialization vector. +pub struct AEADIV(libcrux::aead::Iv); + +impl AEADIV { + /// Attempt construction of an AEAD IV from `bytes`. Panics if + /// number of `bytes` is insufficient. + pub fn from_bytes(bytes: &[u8]) -> Self { + AEADIV(libcrux::aead::Iv::new(bytes).unwrap()) + } +} + +/// An abstract AEAD authentication tag. +pub struct AEADTag(libcrux::aead::Tag); +impl AEADTag { + /// Attempt deserialization of an AEAD tag from `bytes`. Panics if + /// number of `bytes` is insufficient. + pub fn from_bytes(bytes: &[u8]) -> Self { + let bytes: [u8; 16] = bytes.try_into().unwrap(); + AEADTag(libcrux::aead::Tag::from(bytes)) + } +} + +/// Abstract AEAD encryption using `algorithm`. Returns a pair of byte +/// vectors `(ciphertext, tag)`. +pub fn aead_encrypt(key: AEADKey, iv: AEADIV, aad: &[u8], plain: &[u8]) -> (Vec, Vec) { + let (tag, cip) = libcrux::aead::encrypt_detached(&key.0, plain, iv.0, aad).unwrap(); + (cip, tag.as_ref().to_vec()) +} + +/// Abstract AEAD decryption using `algorithm`. On success returns the +/// decrypted plaintext, otherwise a `CryptoError`. +pub fn aead_decrypt( + key: AEADKey, + iv: AEADIV, + aad: &[u8], + cip: &[u8], + tag: AEADTag, +) -> Result, ProtocolError> { + libcrux::aead::decrypt_detached(&key.0, cip, iv.0, aad, &tag.0) + .map_err(|_| ProtocolError::CryptoError) +} + +/// Choice of hashing algorithms. +pub enum HashAlgorithm { + Sha1, + Sha224, + Sha256, + Sha384, + Sha512, + Blake2s, + Blake2b, + Sha3_224, + Sha3_256, + Sha3_384, + Sha3_512, +} + +impl From for libcrux::digest::Algorithm { + /// Converter to `libcrux` type. + fn from(value: HashAlgorithm) -> Self { + match value { + HashAlgorithm::Sha1 => libcrux::digest::Algorithm::Sha1, + HashAlgorithm::Sha224 => libcrux::digest::Algorithm::Sha224, + HashAlgorithm::Sha256 => libcrux::digest::Algorithm::Sha256, + HashAlgorithm::Sha384 => libcrux::digest::Algorithm::Sha384, + HashAlgorithm::Sha512 => libcrux::digest::Algorithm::Sha512, + HashAlgorithm::Blake2s => libcrux::digest::Algorithm::Blake2s, + HashAlgorithm::Blake2b => libcrux::digest::Algorithm::Blake2b, + HashAlgorithm::Sha3_224 => libcrux::digest::Algorithm::Sha3_224, + HashAlgorithm::Sha3_256 => libcrux::digest::Algorithm::Sha3_256, + HashAlgorithm::Sha3_384 => libcrux::digest::Algorithm::Sha3_384, + HashAlgorithm::Sha3_512 => libcrux::digest::Algorithm::Sha3_512, + } + } +} + +/// Abstract hashing using `algorithm`. +pub fn hash(algorithm: HashAlgorithm, input: &[u8]) -> Vec { + libcrux::digest::hash(algorithm.into(), input) +} + +/// Choice of algorithms for instantiation of HMAC. +pub enum HMACAlgorithm { + Sha1, + Sha256, + Sha384, + Sha512, +} + +impl From for libcrux::hmac::Algorithm { + /// Converter to `libcrux` type. + fn from(value: HMACAlgorithm) -> Self { + match value { + HMACAlgorithm::Sha1 => libcrux::hmac::Algorithm::Sha1, + HMACAlgorithm::Sha256 => libcrux::hmac::Algorithm::Sha256, + HMACAlgorithm::Sha384 => libcrux::hmac::Algorithm::Sha384, + HMACAlgorithm::Sha512 => libcrux::hmac::Algorithm::Sha512, + } + } +} + +/// Abstract HMAC using `algorithm` as the hash function. +pub fn hmac(algorithm: HMACAlgorithm, key: &[u8], input: &[u8]) -> Vec { + libcrux::hmac::hmac(algorithm.into(), key, input, None) +} diff --git a/hax-lib-protocol/src/lib.rs b/hax-lib-protocol/src/lib.rs index d58a6ed58..d425a909e 100644 --- a/hax-lib-protocol/src/lib.rs +++ b/hax-lib-protocol/src/lib.rs @@ -1,14 +1,18 @@ -//! This crate provides types and traits for implementing a protocol state -//! machine. +//! This crate provides tools for protocol authors to write protocol +//! specifications for hax. //! -//! A protocol party is conceived of as having a set of possible states, one of -//! which is the initial state. Transitioning to a different state is possible -//! either through receiving and processing a message or through writing a -//! message. +//! It contains a collection traits describing state machine behaviour, as +//! well as a library of abstract primitive cryptographic operations for +//! use in protocol specifications. + +pub mod crypto; +pub mod state_machine; /// A protocol error type. #[derive(Debug)] pub enum ProtocolError { + /// An error in the crypto abstraction layer + CryptoError, /// On receiving an unexpected message, i.e. one that does not allow a state /// transition from the current state. InvalidMessage, @@ -17,41 +21,3 @@ pub enum ProtocolError { } pub type ProtocolResult = Result; - -/// A trait for protocol initial states. -pub trait InitialState { - /// Initializes the state given initialization data in `prologue`. - /// - /// Errors on invalid initialization data. - fn init(prologue: Option>) -> ProtocolResult - where - Self: Sized; -} - -/// A state where a message must be written before transitioning to the next state. -/// -/// `WriteState` can only be implemented once by every state type, implying that -/// in any protocol party state, if a message is to be written, that message and -/// the state the party is in after writing the message are uniquely determined. -pub trait WriteState { - /// The uniquely determined state that is transitioned to after writing the message. - type NextState; - /// The type of the message that is being written. - type Message; - /// Produce the message to be written when transitioning to the next state. - fn write(self) -> ProtocolResult<(Self::NextState, Self::Message)>; -} - -/// A state where a message must be read before transitioning to the next state. -/// -/// A state type may implement `ReadState` multiple times, for different -/// instances of `NextState`, allowing the following state to depend on the -/// message that was received. -pub trait ReadState { - /// The type of message to be read. - type Message; - - /// Generate the next state based on the current state and the received - /// message. - fn read(self, msg: Self::Message) -> ProtocolResult; -} diff --git a/hax-lib-protocol/src/state_machine.rs b/hax-lib-protocol/src/state_machine.rs new file mode 100644 index 000000000..b9ea158e4 --- /dev/null +++ b/hax-lib-protocol/src/state_machine.rs @@ -0,0 +1,47 @@ +//! This module provides types and traits for implementing a protocol state +//! machine. +//! +//! A protocol party is conceived of as having a set of possible states, one of +//! which is the initial state. Transitioning to a different state is possible +//! either through receiving and processing a message or through writing a +//! message. + +use crate::ProtocolResult; + +/// A trait for protocol initial states. +pub trait InitialState { + /// Initializes the state given initialization data in `prologue`. + /// + /// Errors on invalid initialization data. + fn init(prologue: Option>) -> ProtocolResult + where + Self: Sized; +} + +/// A state where a message must be written before transitioning to the next state. +/// +/// `WriteState` can only be implemented once by every state type, implying that +/// in any protocol party state, if a message is to be written, that message and +/// the state the party is in after writing the message are uniquely determined. +pub trait WriteState { + /// The uniquely determined state that is transitioned to after writing the message. + type NextState; + /// The type of the message that is being written. + type Message; + /// Produce the message to be written when transitioning to the next state. + fn write(self) -> ProtocolResult<(Self::NextState, Self::Message)>; +} + +/// A state where a message must be read before transitioning to the next state. +/// +/// A state type may implement `ReadState` multiple times, for different +/// instances of `NextState`, allowing the following state to depend on the +/// message that was received. +pub trait ReadState { + /// The type of message to be read. + type Message; + + /// Generate the next state based on the current state and the received + /// message. + fn read(self, msg: Self::Message) -> ProtocolResult; +} diff --git a/tests/Cargo.lock b/tests/Cargo.lock index ac5da0078..d6beb80a2 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -52,6 +52,10 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa" +[[package]] +name = "basic-structs" +version = "0.1.0" + [[package]] name = "bitflags" version = "1.3.2" @@ -71,8 +75,14 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "37b2a672a2cb129a2e41c10b1224bb368f9f37a2b16b612598138befd7b37eb5" [[package]] -name = "basic-structs" -version = "0.1.0" +name = "cc" +version = "1.0.83" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f1174fb0b6ec23863f8b971027804a42614e347eafb0a95bf0b12cdae21fc4d0" +dependencies = [ + "jobserver", + "libc", +] [[package]] name = "cfg-if" @@ -238,45 +248,10 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "be4136b2a15dd319360be1c07d9933517ccf0be8f16bf62a3bee4f0d618df427" dependencies = [ "cfg-if", + "js-sys", "libc", "wasi", -] - -[[package]] -name = "hacspec-chacha20" -version = "0.1.0" -source = "git+https://github.com/hacspec/specs#3efdf5e1245783a68d2fb3d83e0f90bd15ad4982" -dependencies = [ - "hacspec-lib", -] - -[[package]] -name = "hacspec-chacha20poly1305" -version = "0.1.0" -source = "git+https://github.com/hacspec/specs#3efdf5e1245783a68d2fb3d83e0f90bd15ad4982" -dependencies = [ - "hacspec-chacha20", - "hacspec-lib", - "hacspec-poly1305", -] - -[[package]] -name = "hacspec-curve25519" -version = "0.1.0" -source = "git+https://github.com/hacspec/specs#3efdf5e1245783a68d2fb3d83e0f90bd15ad4982" -dependencies = [ - "hacspec-lib", -] - -[[package]] -name = "hacspec-derive" -version = "0.1.0" -source = "git+https://github.com/hacspec/hacspec.git#bb5b411dced2dfe5c7601674153de4545c783c10" -dependencies = [ - "hacspec-lib", - "proc-macro2", - "quote", - "syn 1.0.109", + "wasm-bindgen", ] [[package]] @@ -291,25 +266,6 @@ dependencies = [ "serde_json", ] -[[package]] -name = "hacspec-hkdf" -version = "0.1.0" -source = "git+https://github.com/hacspec/specs#3efdf5e1245783a68d2fb3d83e0f90bd15ad4982" -dependencies = [ - "hacspec-hmac", - "hacspec-lib", - "hacspec-sha256", -] - -[[package]] -name = "hacspec-hmac" -version = "0.1.0" -source = "git+https://github.com/hacspec/specs#3efdf5e1245783a68d2fb3d83e0f90bd15ad4982" -dependencies = [ - "hacspec-lib", - "hacspec-sha256", -] - [[package]] name = "hacspec-lib" version = "0.1.0-beta.1" @@ -320,25 +276,6 @@ dependencies = [ "secret_integers", ] -[[package]] -name = "hacspec-poly1305" -version = "0.1.0" -source = "git+https://github.com/hacspec/specs#3efdf5e1245783a68d2fb3d83e0f90bd15ad4982" -dependencies = [ - "hacspec-lib", -] - -[[package]] -name = "hacspec-sha256" -version = "0.1.0" -source = "git+https://github.com/hacspec/specs#3efdf5e1245783a68d2fb3d83e0f90bd15ad4982" -dependencies = [ - "abstract_integers", - "hacspec-derive", - "hacspec-lib", - "secret_integers", -] - [[package]] name = "half" version = "1.8.2" @@ -381,6 +318,9 @@ dependencies = [ [[package]] name = "hax-lib-protocol" version = "0.1.0-pre.1" +dependencies = [ + "libcrux", +] [[package]] name = "hax-lib-protocol-macros" @@ -430,6 +370,15 @@ version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38" +[[package]] +name = "jobserver" +version = "0.1.27" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8c37f63953c4c63420ed5fd3d6d398c719489b9f872b9fa683262f8edd363c7d" +dependencies = [ + "libc", +] + [[package]] name = "js-sys" version = "0.3.66" @@ -451,6 +400,48 @@ version = "0.2.147" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b4668fb0ea861c1df094127ac5f1da3409a82116a4ba74fca2e58ef927159bb3" +[[package]] +name = "libcrux" +version = "0.0.2-pre.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "31d9dcd435758db03438089760c55a45e6bcab7e4e299ee261f75225ab29d482" +dependencies = [ + "getrandom", + "libcrux-hacl", + "libcrux-platform", + "libjade-sys", + "rand", +] + +[[package]] +name = "libcrux-hacl" +version = "0.0.2-pre.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "52b2581ce493c5c22700077b5552b47be69b67b8176716572b02856218db0b68" +dependencies = [ + "cc", + "libcrux-platform", +] + +[[package]] +name = "libcrux-platform" +version = "0.0.2-pre.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "647e39666194b11df17c19451d1154b9be79df98b9821532560c2ecad0cf3410" +dependencies = [ + "libc", +] + +[[package]] +name = "libjade-sys" +version = "0.0.2-pre.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ec4d22bba476bf8f5aebe36ccfd0e56dba8707e0c3b5c76996576028f48ffb8e" +dependencies = [ + "cc", + "libcrux-platform", +] + [[package]] name = "literals" version = "0.1.0" @@ -500,15 +491,10 @@ name = "noise-kkpsk0" version = "0.1.0" dependencies = [ "criterion", - "hacspec-chacha20", - "hacspec-chacha20poly1305", - "hacspec-curve25519", "hacspec-dev", - "hacspec-hkdf", - "hacspec-hmac", - "hacspec-lib", - "hacspec-poly1305", - "hacspec-sha256", + "hax-lib-macros", + "hax-lib-protocol", + "hax-lib-protocol-macros", "rand", "rayon", "serde", diff --git a/tests/proverif-noise/Cargo.toml b/tests/proverif-noise/Cargo.toml index 7f64550f6..ab65750ba 100644 --- a/tests/proverif-noise/Cargo.toml +++ b/tests/proverif-noise/Cargo.toml @@ -8,14 +8,6 @@ description = "hacspec chacha20 poly1305 authenticated encryption" readme = "README.md" [dependencies] -hacspec-lib = { git = "https://github.com/hacspec/hacspec.git" } -hacspec-chacha20 = { git = "https://github.com/hacspec/specs", version = "0.1.0" } -hacspec-poly1305 = { git = "https://github.com/hacspec/specs", version = "0.1.0" } -hacspec-chacha20poly1305 = { git = "https://github.com/hacspec/specs", version = "0.1.0" } -hacspec-curve25519 = { git = "https://github.com/hacspec/specs", version = "0.1.0" } -hacspec-sha256 = { git = "https://github.com/hacspec/specs", version = "0.1.0" } -hacspec-hmac = { git = "https://github.com/hacspec/specs", version = "0.1.0" } -hacspec-hkdf = { git = "https://github.com/hacspec/specs", version = "0.1.0" } hax-lib-protocol = { path = "../../hax-lib-protocol" } hax-lib-protocol-macros = { path = "../../hax-lib-protocol-macros" } hax-lib-macros = { path = "../../hax-lib-macros" } @@ -28,3 +20,6 @@ rayon = "1.3.0" criterion = "0.4" rand = "0.8" hacspec-dev = { git = "https://github.com/hacspec/hacspec.git" } + +[package.metadata.hax-tests] +into."pro-verif" = { broken = false, snapshot = "none" } diff --git a/tests/proverif-noise/src/lib.rs b/tests/proverif-noise/src/lib.rs index 735225745..2fa4119d3 100644 --- a/tests/proverif-noise/src/lib.rs +++ b/tests/proverif-noise/src/lib.rs @@ -1,8 +1,3 @@ -#![feature(proc_macro_hygiene)] -#[hax_lib_macros::exclude] pub mod noise_crypto; pub mod noise_kkpsk0; -#[hax_lib_macros::exclude] pub mod noise_lib; -use hacspec_lib::*; -bytes!(ProtocolName, 36); diff --git a/tests/proverif-noise/src/noise_crypto.rs b/tests/proverif-noise/src/noise_crypto.rs index 6572aae01..93b5c0287 100644 --- a/tests/proverif-noise/src/noise_crypto.rs +++ b/tests/proverif-noise/src/noise_crypto.rs @@ -1,13 +1,5 @@ // Import hacspec and all needed definitions. -use hacspec_lib::*; - -use hacspec_chacha20::*; -use hacspec_chacha20poly1305::*; -use hacspec_curve25519::*; -use hacspec_hmac::*; -use hacspec_poly1305::*; -use hacspec_sha256::*; -//use hacspec_hkdf::*; +use hax_lib_protocol::crypto::{DHGroup, *}; /// This file formalizes the Crypto Functions from the Noise Specification /// Section 4: Crypto Functions @@ -19,62 +11,60 @@ pub enum Error { /// Section 4.1 and 12.1: Diffie-Hellman Functions for Curve25519 pub struct KeyPair { - private_key: X25519SerializedScalar, - pub public_key: Seq, + private_key: DHScalar, + pub public_key: Vec, } pub const DHLEN: usize = 32; -pub fn generate_keypair(sk: &Seq) -> KeyPair { - let sk = X25519SerializedScalar::from_seq(sk); - let pk = Seq::from_seq(&x25519_secret_to_public(sk)); +pub fn generate_keypair(sk: &[u8]) -> KeyPair { + let sk = DHScalar::from_bytes(sk); + let pk = dh_scalar_multiply_base(DHGroup::X25519, sk.clone()); KeyPair { private_key: sk, public_key: pk, } } -pub fn dh(sk: &KeyPair, pk: &Seq) -> Seq { - let pk = X25519SerializedPoint::from_seq(pk); - let secret = x25519_scalarmult(sk.private_key, pk); - Seq::from_seq(&secret) +pub fn dh(sk: &KeyPair, pk: &[u8]) -> Vec { + let pk = DHElement::from_bytes(pk); + + dh_scalar_multiply(DHGroup::X25519, sk.private_key.clone(), pk) } /// Section 4.2 and 12.3: Cipher functions for ChaCha20-Poly1305 -pub fn encrypt(key: &Seq, counter: u64, aad: &Seq, plain: &Seq) -> Seq { - let chacha_iv = Seq::::new(4).concat(&U64_to_le_bytes(U64(counter))); - let (cipher, tag) = chacha20_poly1305_encrypt( - ChaChaKey::from_seq(key), - ChaChaIV::from_seq(&chacha_iv), +pub fn encrypt(key: &[u8], counter: u64, aad: &[u8], plain: &[u8]) -> Vec { + let mut chacha_iv = vec![0u8; 4]; + chacha_iv.extend_from_slice(&counter.to_le_bytes()); + let (mut cipher, tag) = aead_encrypt( + AEADKey::from_bytes(AEADAlgorithm::Chacha20Poly1305, key), + AEADIV::from_bytes(&chacha_iv), aad, plain, ); - cipher.concat(&tag) + cipher.extend_from_slice(&tag); + cipher } -pub fn decrypt( - key: &Seq, - counter: u64, - aad: &Seq, - cipher: &Seq, -) -> Result, Error> { - let chacha_iv = Seq::::new(4).concat(&U64_to_le_bytes(U64(counter))); +pub fn decrypt(key: &[u8], counter: u64, aad: &[u8], cipher: &[u8]) -> Result, Error> { + let mut chacha_iv = vec![0u8; 4]; + chacha_iv.extend_from_slice(&counter.to_le_bytes()); let cipher_len = cipher.len() - 16; - let cip = cipher.slice(0, cipher_len); - let tag = cipher.slice(cipher_len, 16); - chacha20_poly1305_decrypt( - ChaChaKey::from_seq(key), - ChaChaIV::from_seq(&chacha_iv), + let cip = &cipher[0..cipher_len]; + let tag = &cipher[cipher_len..cipher.len()]; + aead_decrypt( + AEADKey::from_bytes(AEADAlgorithm::Chacha20Poly1305, key), + AEADIV::from_bytes(&chacha_iv), aad, - &cip, - Poly1305Tag::from_seq(&tag), + cip, + AEADTag::from_bytes(tag), ) .map_err(|_| Error::CryptoError) } -pub fn rekey(key: &Seq) -> Seq { - encrypt(key, 0xffffffffffffffffu64, &Seq::new(0), &Seq::new(32)) +pub fn rekey(key: &[u8]) -> Vec { + encrypt(key, 0xffffffffffffffffu64, &Vec::new(), &[0u8; 32]) } /// Section 4.3 and 12.5: Hash functions for SHA-256 @@ -82,38 +72,36 @@ pub fn rekey(key: &Seq) -> Seq { pub const HASHLEN: usize = 32; pub const BLOCKLEN: usize = 64; -pub fn hash(input: &Seq) -> Seq { - Seq::from_seq(&sha256(input)) +pub fn hash(input: &[u8]) -> Vec { + hax_lib_protocol::crypto::hash(HashAlgorithm::Sha256, input) } -pub fn hmac_hash(key: &Seq, input: &Seq) -> Seq { - Seq::from_seq(&hmac(key, input)) +pub fn hmac_hash(key: &[u8], input: &[u8]) -> Vec { + hmac(HMACAlgorithm::Sha256, key, input) } /// HKDF spec as per Noise /// Alternative would be to directly use HKDF -pub fn kdf_next(secret: &Seq, prev: &Seq, counter: u8) -> Seq { - let mut ctr = Seq::new(1); - ctr[0] = U8(counter); - hmac_hash(secret, &prev.concat(&ctr)) +pub fn kdf_next(secret: &[u8], prev: &[u8], counter: u8) -> Vec { + hmac_hash(secret, &[prev, &[counter]].concat()) } -pub fn hkdf1(key: &Seq, ikm: &Seq) -> Seq { +pub fn hkdf1(key: &[u8], ikm: &[u8]) -> Vec { let secret = hmac_hash(key, ikm); - kdf_next(&secret, &Seq::new(0), 1) + kdf_next(&secret, &Vec::new(), 1) } -pub fn hkdf2(key: &Seq, ikm: &Seq) -> (Seq, Seq) { +pub fn hkdf2(key: &[u8], ikm: &[u8]) -> (Vec, Vec) { let secret = hmac_hash(key, ikm); - let k1 = kdf_next(&secret, &Seq::new(0), 1); + let k1 = kdf_next(&secret, &Vec::new(), 1); let k2 = kdf_next(&secret, &k1, 2); (k1, k2) } -pub fn hkdf3(key: &Seq, ikm: &Seq) -> (Seq, Seq, Seq) { +pub fn hkdf3(key: &[u8], ikm: &[u8]) -> (Vec, Vec, Vec) { let secret = hmac_hash(key, ikm); - let k1 = kdf_next(&secret, &Seq::new(0), 1); + let k1 = kdf_next(&secret, &Vec::new(), 1); let k2 = kdf_next(&secret, &k1, 2); let k3 = kdf_next(&secret, &k1, 3); (k1, k2, k3) diff --git a/tests/proverif-noise/src/noise_kkpsk0.rs b/tests/proverif-noise/src/noise_kkpsk0.rs index 6047a4a90..1f4ab9496 100644 --- a/tests/proverif-noise/src/noise_kkpsk0.rs +++ b/tests/proverif-noise/src/noise_kkpsk0.rs @@ -1,16 +1,14 @@ // Import hacspec and all needed definitions. -use hacspec_lib::*; - use crate::*; use noise_crypto::*; use noise_lib::*; pub struct HandshakeStateI0 { st: SymmetricState, - psk: Seq, + psk: Vec, s: KeyPair, e: KeyPair, - rs: Seq, + rs: Vec, } pub struct HandshakeStateI1 { @@ -21,73 +19,74 @@ pub struct HandshakeStateI1 { pub struct HandshakeStateR0 { st: SymmetricState, - psk: Seq, + psk: Vec, s: KeyPair, e: KeyPair, - rs: Seq, + rs: Vec, } pub struct HandshakeStateR1 { st: SymmetricState, e: KeyPair, - rs: Seq, - re: Seq, + rs: Vec, + re: Vec, } pub struct Transport { send: CipherState, recv: CipherState, - handshake_hash: Seq, + handshake_hash: Vec, } +struct ProtocolName([u8; 36]); #[allow(non_upper_case_globals)] -const Noise_KKpsk0_25519_ChaChaPoly_SHA256: ProtocolName = ProtocolName(secret_bytes!([ +const Noise_KKpsk0_25519_ChaChaPoly_SHA256: ProtocolName = ProtocolName([ 78u8, 111u8, 105u8, 115u8, 101u8, 95u8, 75u8, 75u8, 112u8, 115u8, 107u8, 48u8, 95u8, 50u8, 53u8, 53u8, 49u8, 57u8, 95u8, 67u8, 104u8, 97u8, 67u8, 104u8, 97u8, 80u8, 111u8, 108u8, 121u8, - 95u8, 83u8, 72u8, 65u8, 50u8, 53u8, 54u8 -])); + 95u8, 83u8, 72u8, 65u8, 50u8, 53u8, 54u8, +]); /// KKpsk0: /// -> s /// <- s /// ... pub fn initialize_initiator( - prologue: &Seq, - psk: Seq, + prologue: &[u8], + psk: Vec, s: KeyPair, e: KeyPair, - rs: &Seq, + rs: &[u8], ) -> HandshakeStateI0 { - let st = initialize_symmetric(&Seq::from_seq(&Noise_KKpsk0_25519_ChaChaPoly_SHA256)); + let st = initialize_symmetric(&Noise_KKpsk0_25519_ChaChaPoly_SHA256.0); let st = mix_hash(st, prologue); - let st = mix_hash(st, &Seq::from_seq(&s.public_key)); + let st = mix_hash(st, &s.public_key); let st = mix_hash(st, rs); HandshakeStateI0 { psk, st, s, e, - rs: rs.clone(), + rs: rs.to_vec(), } } pub fn initialize_responder( - prologue: &Seq, - psk: Seq, + prologue: &[u8], + psk: Vec, s: KeyPair, e: KeyPair, - rs: &Seq, + rs: &[u8], ) -> HandshakeStateR0 { - let st = initialize_symmetric(&Seq::from_seq(&Noise_KKpsk0_25519_ChaChaPoly_SHA256)); + let st = initialize_symmetric(&Noise_KKpsk0_25519_ChaChaPoly_SHA256.0); let st = mix_hash(st, prologue); let st = mix_hash(st, rs); - let st = mix_hash(st, &Seq::from_seq(&s.public_key)); + let st = mix_hash(st, &s.public_key); HandshakeStateR0 { st, psk, s, e, - rs: rs.clone(), + rs: rs.to_vec(), } } @@ -96,8 +95,8 @@ pub fn initialize_responder( /// -> psk, e, es, ss pub fn write_message1( hs: HandshakeStateI0, - payload: &Seq, -) -> Result<(HandshakeStateI1, Seq), Error> { + payload: &[u8], +) -> Result<(HandshakeStateI1, Vec), Error> { let HandshakeStateI0 { st, psk, s, e, rs } = hs; let st = mix_key_and_hash(st, &psk); let st = mix_hash(st, &e.public_key); @@ -113,30 +112,32 @@ pub fn write_message1( pub fn read_message1( hs: HandshakeStateR0, - ciphertext: &Seq, -) -> Result<(HandshakeStateR1, Seq), Error> { + ciphertext: &[u8], +) -> Result<(HandshakeStateR1, Vec), Error> { let HandshakeStateR0 { st, psk, s, e, rs } = hs; - let re = ciphertext.slice(0, DHLEN); - let ciphertext = ciphertext.slice(DHLEN, ciphertext.len() - DHLEN); + let re = &ciphertext[0..DHLEN]; + let ciphertext = &ciphertext[DHLEN..ciphertext.len()]; let st = mix_key_and_hash(st, &psk); - let st = mix_hash(st, &re); - let st = mix_key(st, &re); - let es = dh(&s, &re); + let st = mix_hash(st, re); + let st = mix_key(st, re); + let es = dh(&s, re); let st = mix_key(st, &es); let ss = dh(&s, &rs); let st = mix_key(st, &ss); - let (st, plaintext) = decrypt_and_hash(st, &ciphertext)?; - let hs = HandshakeStateR1 { st, e, rs, re }; + let (st, plaintext) = decrypt_and_hash(st, ciphertext)?; + let hs = HandshakeStateR1 { + st, + e, + rs, + re: re.to_vec(), + }; Ok((hs, plaintext)) } /// KKpsk0: /// ... /// <- e, ee, se -pub fn write_message2( - hs: HandshakeStateR1, - payload: &Seq, -) -> Result<(Transport, Seq), Error> { +pub fn write_message2(hs: HandshakeStateR1, payload: &[u8]) -> Result<(Transport, Vec), Error> { let HandshakeStateR1 { st, e, rs, re } = hs; let st = mix_hash(st, &e.public_key); let st = mix_key(st, &e.public_key); @@ -156,18 +157,18 @@ pub fn write_message2( pub fn read_message2( hs: HandshakeStateI1, - ciphertext: &Seq, -) -> Result<(Transport, Seq), Error> { + ciphertext: &[u8], +) -> Result<(Transport, Vec), Error> { let HandshakeStateI1 { st, s, e } = hs; - let re = ciphertext.slice(0, DHLEN); - let ciphertext = ciphertext.slice(DHLEN, ciphertext.len() - DHLEN); - let st = mix_hash(st, &re); - let st = mix_key(st, &re); - let ee = dh(&e, &re); + let re = &ciphertext[0..DHLEN]; + let ciphertext = &ciphertext[DHLEN..ciphertext.len()]; + let st = mix_hash(st, re); + let st = mix_key(st, re); + let ee = dh(&e, re); let st = mix_key(st, &ee); - let se = dh(&s, &re); + let se = dh(&s, re); let st = mix_key(st, &se); - let (st, plaintext) = decrypt_and_hash(st, &ciphertext)?; + let (st, plaintext) = decrypt_and_hash(st, ciphertext)?; let (c1, c2, h) = split(st); let tx = Transport { send: c1, @@ -182,9 +183,9 @@ pub fn read_message2( /// <- pub fn write_transport( tx: Transport, - ad: &Seq, - payload: &Seq, -) -> Result<(Transport, Seq), Error> { + ad: &[u8], + payload: &[u8], +) -> Result<(Transport, Vec), Error> { let Transport { send, recv, @@ -201,9 +202,9 @@ pub fn write_transport( pub fn read_transport( tx: Transport, - ad: &Seq, - ciphertext: &Seq, -) -> Result<(Transport, Seq), Error> { + ad: &[u8], + ciphertext: &[u8], +) -> Result<(Transport, Vec), Error> { let Transport { send, recv, diff --git a/tests/proverif-noise/src/noise_lib.rs b/tests/proverif-noise/src/noise_lib.rs index a6fe4d856..e801e2d4b 100644 --- a/tests/proverif-noise/src/noise_lib.rs +++ b/tests/proverif-noise/src/noise_lib.rs @@ -1,5 +1,4 @@ // Import hacspec and all needed definitions. -use hacspec_lib::*; use crate::*; use noise_crypto::*; @@ -8,24 +7,24 @@ use noise_crypto::*; /// Section 5: https://noiseprotocol.org/noise.html#processing-rules pub struct CipherState { - k: Option>, + k: Option>, n: u64, } pub struct SymmetricState { cs: CipherState, - ck: Seq, - h: Seq, + ck: Vec, + h: Vec, } /// 5.1: The CipherState Object -pub fn initialize_key(key: Option>) -> CipherState { +pub fn initialize_key(key: Option>) -> CipherState { CipherState { k: key, n: 0u64 } } pub fn has_key(cs: &CipherState) -> bool { - cs.k != None + cs.k.is_some() } pub fn set_nonce(cs: CipherState, n: u64) -> CipherState { @@ -35,9 +34,9 @@ pub fn set_nonce(cs: CipherState, n: u64) -> CipherState { pub fn encrypt_with_ad( cs: CipherState, - ad: &Seq, - plaintext: &Seq, -) -> Result<(CipherState, Seq), Error> { + ad: &[u8], + plaintext: &[u8], +) -> Result<(CipherState, Vec), Error> { let CipherState { k, n } = cs; if n == 0xffffffffffffffffu64 { Err(Error::CryptoError) @@ -53,16 +52,16 @@ pub fn encrypt_with_ad( cip, )) } - None => Ok((CipherState { k, n }, plaintext.clone())), + None => Ok((CipherState { k, n }, plaintext.to_vec())), } } } pub fn decrypt_with_ad( cs: CipherState, - ad: &Seq, - ciphertext: &Seq, -) -> Result<(CipherState, Seq), Error> { + ad: &[u8], + ciphertext: &[u8], +) -> Result<(CipherState, Vec), Error> { let CipherState { k, n } = cs; if n == 0xffffffffffffffffu64 { Err(Error::CryptoError) @@ -78,7 +77,7 @@ pub fn decrypt_with_ad( plain, )) } - None => Ok((CipherState { k, n }, ciphertext.clone())), + None => Ok((CipherState { k, n }, ciphertext.to_vec())), } } } @@ -96,14 +95,13 @@ pub fn rekey(cs: CipherState) -> Result { /// 5.2: The SymmetricState Object -pub fn initialize_symmetric(protocol_name: &Seq) -> SymmetricState { +pub fn initialize_symmetric(protocol_name: &[u8]) -> SymmetricState { let pnlen = protocol_name.len(); - let mut hv: Seq = Seq::new(0); - if pnlen < HASHLEN { - hv = protocol_name.concat(&Seq::new(32 - pnlen)); + let hv: Vec = if pnlen < HASHLEN { + [protocol_name, &vec![0u8; 32 - pnlen]].concat() } else { - hv = hash(protocol_name); - } + hash(protocol_name) + }; let ck = hv.clone(); SymmetricState { cs: initialize_key(None), @@ -112,11 +110,11 @@ pub fn initialize_symmetric(protocol_name: &Seq) -> SymmetricState { } } -pub fn mix_key(st: SymmetricState, input_key_material: &Seq) -> SymmetricState { +pub fn mix_key(st: SymmetricState, input_key_material: &[u8]) -> SymmetricState { let SymmetricState { cs: _, ck, h } = st; let (ck, mut temp_k) = hkdf2(&ck, input_key_material); if HASHLEN == 64 { - temp_k = temp_k.slice(0, 32); + temp_k.truncate(32); } SymmetricState { cs: initialize_key(Some(temp_k)), @@ -125,21 +123,23 @@ pub fn mix_key(st: SymmetricState, input_key_material: &Seq) -> SymmetricSta } } -pub fn mix_hash(st: SymmetricState, data: &Seq) -> SymmetricState { +pub fn mix_hash(st: SymmetricState, data: &[u8]) -> SymmetricState { let SymmetricState { cs, ck, h } = st; SymmetricState { cs, ck, - h: hash(&h.concat(data)), + h: hash(&[&h, data].concat()), } } -pub fn mix_key_and_hash(st: SymmetricState, input_key_material: &Seq) -> SymmetricState { +pub fn mix_key_and_hash(st: SymmetricState, input_key_material: &[u8]) -> SymmetricState { let SymmetricState { cs: _, ck, h } = st; let (ck, temp_h, mut temp_k) = hkdf3(&ck, input_key_material); - let new_h = hash(&h.concat(&temp_h)); + let mut new_h = h; + new_h.extend_from_slice(&temp_h); + let new_h = hash(&new_h); if HASHLEN == 64 { - temp_k = temp_k.slice(0, 32); + temp_k.truncate(32); } SymmetricState { cs: initialize_key(Some(temp_k)), @@ -149,7 +149,7 @@ pub fn mix_key_and_hash(st: SymmetricState, input_key_material: &Seq) -> Sym } /// Unclear if we need a special function for psk or we can reuse mix_key_and_hash above -//pub fn mix_psk(st:SymmetricState,psk:&Seq) -> (Seq,Seq,Seq) { +//pub fn mix_psk(st:SymmetricState,psk:&[u8]) -> (Vec,Vec,Vec) { // let (ck,temp_hash,cs_k) = kdf3(key,psk); // let next_hash = mix_hash(prev_hash,&temp_hash); // (ck,cs_k,next_hash) @@ -157,10 +157,12 @@ pub fn mix_key_and_hash(st: SymmetricState, input_key_material: &Seq) -> Sym pub fn encrypt_and_hash( st: SymmetricState, - plaintext: &Seq, -) -> Result<(SymmetricState, Seq), Error> { + plaintext: &[u8], +) -> Result<(SymmetricState, Vec), Error> { let (new_cs, ciphertext) = encrypt_with_ad(st.cs, &st.h, plaintext)?; - let new_h = hash(&st.h.concat(&ciphertext)); + let mut new_h = st.h.clone(); + new_h.extend_from_slice(&ciphertext); + let new_h = hash(&new_h); Ok(( SymmetricState { cs: new_cs, @@ -173,10 +175,12 @@ pub fn encrypt_and_hash( pub fn decrypt_and_hash( st: SymmetricState, - ciphertext: &Seq, -) -> Result<(SymmetricState, Seq), Error> { + ciphertext: &[u8], +) -> Result<(SymmetricState, Vec), Error> { let (new_cs, plaintext) = decrypt_with_ad(st.cs, &st.h, ciphertext)?; - let new_h = hash(&st.h.concat(ciphertext)); + let mut new_h = st.h.clone(); + new_h.extend_from_slice(ciphertext); + let new_h = hash(&new_h); Ok(( SymmetricState { cs: new_cs, @@ -187,11 +191,11 @@ pub fn decrypt_and_hash( )) } -pub fn split(st: SymmetricState) -> (CipherState, CipherState, Seq) { - let (mut temp_k1, mut temp_k2) = hkdf2(&st.ck, &Seq::new(0)); +pub fn split(st: SymmetricState) -> (CipherState, CipherState, Vec) { + let (mut temp_k1, mut temp_k2) = hkdf2(&st.ck, &Vec::new()); if HASHLEN == 64 { - temp_k1 = temp_k1.slice(0, 32); - temp_k2 = temp_k2.slice(0, 32); + temp_k1.truncate(32); + temp_k2.truncate(32); } ( initialize_key(Some(temp_k1)), diff --git a/tests/proverif-ping-pong/src/a.rs b/tests/proverif-ping-pong/src/a.rs index 0f72e5f24..79616f4d2 100644 --- a/tests/proverif-ping-pong/src/a.rs +++ b/tests/proverif-ping-pong/src/a.rs @@ -1,4 +1,4 @@ -use hax_lib_protocol::*; +use hax_lib_protocol::state_machine::*; use crate::Message; diff --git a/tests/proverif-ping-pong/src/b.rs b/tests/proverif-ping-pong/src/b.rs index edd234679..5d950d638 100644 --- a/tests/proverif-ping-pong/src/b.rs +++ b/tests/proverif-ping-pong/src/b.rs @@ -1,4 +1,4 @@ -use hax_lib_protocol::*; +use hax_lib_protocol::state_machine::*; use crate::Message; diff --git a/tests/proverif-ping-pong/src/lib.rs b/tests/proverif-ping-pong/src/lib.rs index f72bfd4da..e6570e81c 100644 --- a/tests/proverif-ping-pong/src/lib.rs +++ b/tests/proverif-ping-pong/src/lib.rs @@ -11,7 +11,7 @@ pub enum Message { fn run() { use a::A0; use b::{B0, B1}; - use hax_lib_protocol::{InitialState, ReadState, WriteState}; + use hax_lib_protocol::state_machine::{InitialState, ReadState, WriteState}; let a = A0::init(Some(vec![1])).unwrap(); let b = B0::init(None).unwrap();