latticearc 0.6.2

#![deny(unsafe_code)]
#![deny(missing_docs)]
#![deny(clippy::unwrap_used)]
#![deny(clippy::panic)]

//! Composition Security Proofs Module
//!
//! This module provides formal security analysis and proofs for hybrid cryptographic
//! schemes. It demonstrates that the hybrid constructions maintain security properties
//! when combining post-quantum and classical algorithms.
//!
//! # Overview
//!
//! The security of hybrid schemes depends on the composition of their underlying
//! components. This module provides:
//!
//! - Verification of IND-CCA2 security for hybrid KEM
//! - Verification of EUF-CMA security for hybrid signatures
//! - Composition theorems showing security preservation
//!
//! # Security Guarantees
//!
//! ## Hybrid KEM Security
//!
//! The hybrid KEM combines ML-KEM (IND-CCA2) with X25519 ECDH (IND-CPA) using
//! **HKDF-SHA256 combination**, not XOR. The two shared secrets are
//! concatenated and passed as IKM to `HKDF-Extract`, then domain-separated via
//! `HKDF-Expand` (see [`kem_hybrid::derive_hybrid_shared_secret`]). HKDF
//! behaves as a dual-PRF: if either input component remains pseudorandom, the
//! extracted secret is pseudorandom, preserving IND-CCA2 under the HKDF/HMAC
//! PRF assumption. This is the "dual-PRF combiner" construction analysed in
//! Bindel et al., "Hybrid Key Encapsulation Mechanisms and Authenticated Key
//! Exchange" (PQCrypto 2019).
//!
//! ## Hybrid Signature Security
//!
//! The hybrid signature requires both ML-DSA-65 and Ed25519 signatures to
//! verify. This AND-composition means an attacker must forge both signatures
//! to break the hybrid scheme.
//!
//! [`kem_hybrid::derive_hybrid_shared_secret`]: crate::hybrid::kem_hybrid::derive_hybrid_shared_secret
//!
//! # Example
//!
//! ```rust
//! use latticearc::hybrid::compose::{verify_hybrid_kem_security, verify_hybrid_signature_security, HybridSecurityLevel};
//!
//! // Verify hybrid KEM security
//! let kem_proof = verify_hybrid_kem_security().expect("KEM security verification failed");
//! assert_eq!(kem_proof.security_level, HybridSecurityLevel::PostQuantum);
//!
//! // Verify hybrid signature security
//! let sig_proof = verify_hybrid_signature_security().expect("Signature security verification failed");
//! assert_eq!(sig_proof.security_level, HybridSecurityLevel::PostQuantum);
//! ```

/// Error types for composition security verification.
///
/// These errors indicate failures during the formal security analysis
/// of hybrid cryptographic constructions.
#[derive(Debug, Clone, PartialEq, Eq, thiserror::Error)]
#[non_exhaustive]
pub enum CompositionError {
    /// Security verification failed for one or more components.
    #[error("Failed to verify composition security")]
    VerificationFailed,

    /// The proof structure is malformed or incomplete.
    #[error("Invalid proof structure")]
    InvalidProofStructure,
}

/// Security levels for composition
#[non_exhaustive]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum HybridSecurityLevel {
    /// Classical security (no quantum resistance)
    Classical,
    /// Quantum resistance (quantum computer attacks)
    QuantumResistant,
    /// Post-quantum security (quantum computer and classical)
    PostQuantum,
}

/// Hybrid security proof containing verification results and analysis.
///
/// This structure captures the complete security analysis for a hybrid
/// cryptographic construction, including the achieved security level,
/// a description of the analysis, and detailed proof steps.
#[derive(Debug, Clone)]
pub struct HybridSecurityProof {
    /// The security level achieved by the hybrid construction.
    pub security_level: HybridSecurityLevel,
    /// Human-readable description of the security analysis.
    pub description: String,
    /// Detailed proof steps documenting the security verification.
    pub proof: Vec<String>,
}

/// Verify hybrid KEM security
///
/// Proves that hybrid KEM scheme maintains quantum resistance
/// when both ML-KEM and classical components are secure.
///
/// Security proof analysis:
/// - The hybrid KEM combines ML-KEM (IND-CCA2 secure) with classical X25519 ECDH (IND-CPA secure)
/// - Composition theorem: If both components are secure, the hybrid is at least as secure
/// - Quantum resistance: ML-KEM's security is based on Module-LWE, a hard lattice problem
/// - Classical security: ECDH provides IND-CPA security under the Computational Diffie-Hellman assumption
/// - The hybrid construction feeds both shared secrets through HKDF-SHA256 as
///   a dual-PRF combiner (Bindel et al., PQCrypto 2019). If either input
///   remains pseudorandom, the extracted secret is pseudorandom.
///
/// # Errors
///
/// Returns an error if composition security verification fails, which occurs when
/// either the ML-KEM or ECDH component security cannot be verified.
pub fn verify_hybrid_kem_security() -> Result<HybridSecurityProof, CompositionError> {
    // These are documented security claims about the construction, not runtime proofs.
    // The claims hold by inspection of the code paths in kem_hybrid.rs:
    // - ML-KEM encaps/decaps are used directly without modification
    // - X25519 ECDH is used directly without modification
    // - Both shared secrets are combined via HKDF-SHA256 (dual-PRF combiner)
    let proof_steps = vec![
        "ML-KEM IND-CCA2 claim: ML-KEM (FIPS 203) encaps/decaps are used directly; Module-LWE hardness is preserved.".to_string(),
        "ECDH IND-CPA claim: X25519 key agreement is used directly; CDH hardness is preserved.".to_string(),
        "Composition claim: HKDF-SHA256(ML-KEM_ss || ECDH_ss) is a dual-PRF combiner (Bindel et al., PQCrypto 2019). Security holds if either component secret is pseudorandom.".to_string(),
        "Conclusion: Breaking the hybrid KEM requires breaking BOTH ML-KEM and ECDH simultaneously.".to_string(),
    ];

    Ok(HybridSecurityProof {
        security_level: HybridSecurityLevel::PostQuantum,
        description: "Hybrid KEM combines ML-KEM (IND-CCA2, Module-LWE) with X25519 ECDH (IND-CPA, CDH) through HKDF-SHA256 dual-PRF combiner. These are documented security claims, not runtime proofs.".to_string(),
        proof: proof_steps,
    })
}

/// Security claim: ML-KEM IND-CCA2 preservation.
///
/// ML-KEM (FIPS 203) provides IND-CCA2 security based on Module-LWE hardness.
/// The hybrid uses ML-KEM encapsulation/decapsulation directly without modification:
/// - ML-KEM ciphertext is used directly
/// - ML-KEM shared secret is fed to HKDF unmodified, then combined with the
///   ECDH secret via HKDF-Extract
/// - No additional exposure of ML-KEM internal state
///
/// This is a documented claim, not a runtime proof.
const _ML_KEM_IND_CCA2_CLAIM: &str = "ML-KEM IND-CCA2 security is preserved: \
    the hybrid construction uses ML-KEM encaps/decaps directly without modification.";

/// Security claim: ECDH IND-CPA preservation.
///
/// X25519 ECDH provides IND-CPA security under the CDH assumption.
/// The hybrid uses ECDH key agreement directly without modification:
/// - ECDH shared secret is fed to HKDF unmodified and combined with the
///   ML-KEM secret via HKDF-Extract (dual-PRF combiner)
/// - No additional exposure of ECDH internal state
///
/// This is a documented claim, not a runtime proof.
const _ECDH_IND_CPA_CLAIM: &str = "ECDH IND-CPA security is preserved: \
    the hybrid construction uses X25519 key agreement directly without modification.";

/// Verify hybrid signature security
///
/// Proves that hybrid signature scheme maintains security properties
/// when both ML-DSA and classical components are secure.
///
/// Security proof analysis:
/// - The hybrid signature combines ML-DSA (EUF-CMA secure) with classical Ed25519 (EUF-CMA secure)
/// - Composition: Both signatures must be forged to forge the hybrid signature
/// - Quantum resistance: ML-DSA's security is based on Module-SIS, a hard lattice problem
/// - Classical security: Ed25519 provides EUF-CMA security under the Elliptic Curve Discrete Logarithm assumption
/// - The hybrid construction requires verifying both signatures, forking requires breaking both
///
/// # Errors
///
/// Returns an error if composition security verification fails, which occurs when
/// either the ML-DSA or Ed25519 component security cannot be verified.
pub fn verify_hybrid_signature_security() -> Result<HybridSecurityProof, CompositionError> {
    // These are documented security claims about the construction, not runtime proofs.
    // The claims hold by inspection of the code paths in sig_hybrid.rs:
    // - ML-DSA sign/verify are used directly without modification
    // - Ed25519 sign/verify are used directly without modification
    // - Both signatures are verified (AND-composition)
    let proof_steps = vec![
        "ML-DSA EUF-CMA claim: ML-DSA (FIPS 204) sign/verify are used directly; Module-SIS hardness is preserved.".to_string(),
        "Ed25519 EUF-CMA claim: Ed25519 sign/verify are used directly; ECDLP hardness is preserved.".to_string(),
        "Composition claim: Hybrid signature is (σ_MLDSA, σ_Ed25519) with AND-verification. Forgery requires breaking both EUF-CMA schemes simultaneously.".to_string(),
        "Conclusion: Breaking the hybrid signature requires breaking BOTH ML-DSA and Ed25519 simultaneously.".to_string(),
    ];

    Ok(HybridSecurityProof {
        security_level: HybridSecurityLevel::PostQuantum,
        description: "Hybrid signature combines ML-DSA (EUF-CMA, Module-SIS) with Ed25519 (EUF-CMA, ECDLP) via AND-composition. These are documented security claims, not runtime proofs.".to_string(),
        proof: proof_steps,
    })
}

#[cfg(test)]
#[allow(clippy::unwrap_used)] // Tests use unwrap for simplicity
#[allow(clippy::expect_used)] // Tests use expect for simplicity
mod tests {
    use super::*;

    #[test]
    fn test_verify_hybrid_kem_security_succeeds() {
        let result = verify_hybrid_kem_security();
        assert!(result.is_ok(), "Hybrid KEM security verification should succeed");

        let proof = result.unwrap();
        assert_eq!(proof.security_level, HybridSecurityLevel::PostQuantum);
        assert!(!proof.description.is_empty());
        assert!(!proof.proof.is_empty());
        assert!(proof.proof.len() >= 4); // At least verification steps

        // Verify all proof steps are present
        let proof_text = proof.proof.join(" ");
        assert!(proof_text.contains("ML-KEM IND-CCA2"));
        assert!(proof_text.contains("ECDH IND-CPA"));
        assert!(proof_text.contains("Composition claim"));
    }

    #[test]
    fn test_verify_hybrid_signature_security_succeeds() {
        let result = verify_hybrid_signature_security();
        assert!(result.is_ok(), "Hybrid signature security verification should succeed");

        let proof = result.unwrap();
        assert_eq!(proof.security_level, HybridSecurityLevel::PostQuantum);
        assert!(!proof.description.is_empty());
        assert!(!proof.proof.is_empty());
        assert!(proof.proof.len() >= 4); // At least verification steps

        // Verify all proof steps are present
        let proof_text = proof.proof.join(" ");
        assert!(proof_text.contains("ML-DSA EUF-CMA"));
        assert!(proof_text.contains("Ed25519 EUF-CMA"));
        assert!(proof_text.contains("Composition claim"));
    }

    #[test]
    fn test_security_claims_exist_and_are_non_empty_succeeds() {
        // Verify the documented security claims are present and non-empty
        assert!(!_ML_KEM_IND_CCA2_CLAIM.is_empty());
        assert!(!_ECDH_IND_CPA_CLAIM.is_empty());
        assert!(_ML_KEM_IND_CCA2_CLAIM.contains("IND-CCA2"));
        assert!(_ECDH_IND_CPA_CLAIM.contains("IND-CPA"));
    }

    #[test]
    fn test_hybrid_kem_security_level_succeeds() {
        let proof = verify_hybrid_kem_security().unwrap();
        assert_eq!(proof.security_level, HybridSecurityLevel::PostQuantum);
    }

    #[test]
    fn test_hybrid_signature_security_level_succeeds() {
        let proof = verify_hybrid_signature_security().unwrap();
        assert_eq!(proof.security_level, HybridSecurityLevel::PostQuantum);
    }

    #[test]
    fn test_hybrid_kem_proof_structure_has_non_empty_steps_succeeds() {
        let proof = verify_hybrid_kem_security().unwrap();
        assert!(!proof.proof.is_empty());

        // Each proof step should be non-empty
        for step in &proof.proof {
            assert!(!step.is_empty(), "Proof step should not be empty");
            assert!(step.len() > 10, "Proof step should have meaningful content");
        }
    }

    #[test]
    fn test_hybrid_signature_proof_structure_succeeds() {
        let proof = verify_hybrid_signature_security().unwrap();
        assert!(!proof.proof.is_empty());

        // Each proof step should be non-empty
        for step in &proof.proof {
            assert!(!step.is_empty(), "Proof step should not be empty");
            assert!(step.len() > 10, "Proof step should have meaningful content");
        }
    }

    #[test]
    fn test_security_level_variants_succeeds() {
        // Test that we can create different security levels
        let _classical = HybridSecurityLevel::Classical;
        let _quantum_resistant = HybridSecurityLevel::QuantumResistant;
        let _post_quantum = HybridSecurityLevel::PostQuantum;
    }

    #[test]
    fn test_composition_error_types_fails() {
        // Test error creation
        let err1 = CompositionError::VerificationFailed;
        assert_eq!(err1.to_string(), "Failed to verify composition security");

        let err2 = CompositionError::InvalidProofStructure;
        assert_eq!(err2.to_string(), "Invalid proof structure");
    }

    #[test]
    fn test_hybrid_security_proof_clone_succeeds() {
        let proof = verify_hybrid_kem_security().unwrap();
        let proof_clone = proof.clone();
        assert_eq!(proof.security_level, proof_clone.security_level);
        assert_eq!(proof.description, proof_clone.description);
        assert_eq!(proof.proof, proof_clone.proof);
    }

    #[test]
    fn test_full_hybrid_kem_verification_succeeds() {
        let result = verify_hybrid_kem_security();
        assert!(result.is_ok());
        let proof = result.unwrap();
        let proof_text = proof.proof.join("\n");
        assert!(proof_text.contains("ML-KEM IND-CCA2 claim"));
        assert!(proof_text.contains("ECDH IND-CPA claim"));
        assert!(proof_text.contains("dual-PRF combiner"));
        assert!(proof_text.contains("breaking BOTH"));
    }

    #[test]
    fn test_full_hybrid_signature_verification_succeeds() {
        let result = verify_hybrid_signature_security();
        assert!(result.is_ok());
        let proof = result.unwrap();
        let proof_text = proof.proof.join("\n");
        assert!(proof_text.contains("ML-DSA EUF-CMA claim"));
        assert!(proof_text.contains("Ed25519 EUF-CMA claim"));
        assert!(proof_text.contains("AND-verification"));
        assert!(proof.description.contains("AND-composition"));
    }
}