RESUMEN
Recent progress in quantum computers severely endangers the security of widely used public-key cryptosystems and of all communication that relies on it. Thus, the US NIST is currently exploring new post-quantum cryptographic algorithms that are robust against quantum computers. Security is seen as one of the most critical issues of low-power IoT devices-even with pre-quantum public-key cryptography-since IoT devices have tight energy constraints, limited computational power and strict memory limitations. In this paper, we present, to the best of our knowledge, the first in-depth investigation of the application of potential post-quantum key encapsulation mechanisms (KEMs) and digital signature algorithms (DSAs) proposed in the related US NIST process to a state-of-the-art, TLS-based, low-power IoT infrastructure. We implemented these new KEMs and DSAs in such a representative infrastructure and measured their impact on energy consumption, latency and memory requirements during TLS handshakes on an IoT edge device. Based on our investigations, we gained the following new insights. First, we show that the main contributor to high TLS handshake latency is the higher bandwidth requirement of post-quantum primitives rather than the cryptographic computation itself. Second, we demonstrate that a smart combination of multiple DSAs yields the most energy-, latency- and memory-efficient public key infrastructures, in contrast to NIST's goal to standardize only one algorithm. Third, we show that code-based, isogeny-based and lattice-based algorithms can be implemented on a low-power IoT edge device based on an off-the-shelf Cortex M4 microcontroller while maintaining viable battery runtimes. This is contrary to much research that claims dedicated hardware accelerators are mandatory.
RESUMEN
Communication and information technologies shape the world's systems of today, and those systems shape our society. The security of those systems relies on mathematical problems that are hard to solve for classical computers, that is, the available current computers. Recent advances in quantum computing threaten the security of our systems and the communications we use. In order to face this threat, multiple solutions and protocols have been proposed in the Post-Quantum Cryptography project carried on by the National Institute of Standards and Technologies. The presented work focuses on defining a formal framework in Maude for the security analysis of different post-quantum key encapsulation mechanisms under assumptions given under the Dolev-Yao model. Through the use of our framework, we construct a symbolic model to represent the behaviour of each of the participants of the protocol in a network. We then conduct reachability analysis and find a man-in-the-middle attack in each of them and a design vulnerability in Bit Flipping Key Encapsulation. For both cases, we provide some insights on possible solutions. Then, we use the Maude Linear Temporal Logic model checker to extend the analysis of the symbolic system regarding security, liveness and fairness properties. Liveness and fairness properties hold while the security property does not due to the man-in-the-middle attack and the design vulnerability in Bit Flipping Key Encapsulation.