Eliseo Sarmiento

Modern instant messaging systems require end-to-end (E2E) security guarantees while operating over server-mediated infrastructures that cannot be fully trusted. At the same time, the impending transition to post-quantum cryptography raises nontrivial challenges for the design of secure messaging protocols that preserve these guarantees. In this work, we present the design of a post-quantum end-to-end secure protocol for instant messaging applications under an untrusted relay model. The proposed construction relies on lattice-based primitives standardized by NIST, namely ML-KEM for key establishment and ML-DSA for authentication, and follows a Double-KEM pattern combined with explicit context binding to derive an E2E session key known only to the communicating clients. The server acts solely as an authenticated relay and never gains access to plaintext messages or session keys. In addition to the protocol design, we complement the protocol description with an automated symbolic verification using ProVerif, establishing injective mutual authentication and session-key secrecy under a Dolev–Yao adversary model. Finally, we characterize the computational cost of different authentication and verification policies and evaluate the performance of the handshake on heterogeneous cloud-based architectures. The results provide practical insight into the feasibility of deploying post-quantum end-to-end secure protocols within existing instant messaging infrastructures.

Formal correctness proofs, analytical tail bounds, and empirical failure studies provide strong guarantees for the Module-Lattice-Based Key-Encapsulation Mechanism (ML–KEM). However, current methods fail to provide an operational, per-instance diagnostic of how close a fully compliant deployment operates to the decryption-failure boundary under standardized compression and thresholding. As a result, implementers, auditors, and operators lack direct visibility into operational safety margins, even when no failures are observed. This study introduces an empirical, fully reproducible diagnostic framework for the implementation assurance of the ML–KEM under the Federal Information Processing Standard 203 (FIPS 203). We define the headroom of each ciphertext as the gap between a compression-aware operative decision threshold and the observed decryption-residual magnitude, and we construct headroom curves by relating explicit threshold tightening to empirical failure probability. From these curves, we extracted the critical tightening budgets at empirically resolvable failure rates, yielding actionable safety margins grounded in the observed behavior. Across the three standardized ML–KEM parameter sets (512/768/1024), we observed a wide flat region followed by an abrupt transition with near overlap across security levels, indicating that operational reliability is governed primarily by compression-aware thresholding rather than by module dimensions. All artifacts (code, data, and figures) are released to ensure full reproducibility and support regression testing and compliance-oriented validation without modifying the standardized decision procedure.

A decreasing Cartesian code is defined by evaluating a monomial set closed under divisibility on a Cartesian set. Some well-known examples are the Reed-Solomon, Reed-Muller, and (some) toric codes. The affine permutations consist of the permutations of the code that depend on an affine transformation. In this work, we study the affine permutations of some decreasing Cartesian codes, including the case when the Cartesian set has copies of multiplicative or additive subgroups.

[ ]A hyperbolic code is an evaluation code that improves a Reed–Muller code because the dimension increases while the minimum distance is not penalized. We give necessary and sufficient conditions, based on the basic parameters of the Reed–Muller code, to determine whether a Reed–Muller code coincides with a hyperbolic code. Given a hyperbolic code [ ], we find the largest Reed–Muller code contained in [ ] and the smallest Reed–Muller code containing [ ]. We then prove that similar to Reed–Muller and affine Cartesian codes, the [ ]th generalized Hamming weight and the [ ]th footprint of the hyperbolic code coincide. Unlike for Reed–Muller and affine Cartesian codes, determining the [ ]th footprint of a hyperbolic code is still an open problem. We give upper and lower bounds for the [ ]th footprint of a hyperbolic code that, sometimes, are sharp.

Fix a square-free monomial m ∈ S = K [ x 1 , … , x n ] m \in S = \mathbb {K}[x_1,\ldots ,x_n] . The square-free principal Borel ideal generated by m m , denoted sfBorel ⁡ ( m ) \operatorname {sfBorel}(m) , is the ideal generated by all the square-free monomials that can be obtained via Borel moves from the monomial m m . We give upper and lower bounds for the Waldschmidt constant of sfBorel ⁡ ( m ) \operatorname {sfBorel}(m) in terms of the support of m m , and in some cases, exact values. For any rational a b ≥ 1 \frac {a}{b} \geq 1 , we show that there exists a square-free principal Borel ideal with Waldschmidt constant equal to a b \frac {a}{b} .