Analysis and verification of code-based key encapsulation mechanism BIKE in Maude

Information technologies are everywhere. From mobile devices to the simplest components, all of them share information over the network. This network might prove to be insecure in the near future with the introduction of quantum cryptography. This concern is addressed by the National Institute for Standards and Technologies with the Post Quantum Cryptography project. In this paper, we select from round 4 of this project the code-based Key Encapsulation Mechanism BIKE and analyze it in Maude. We use a previously defined framework on which we can specify the symbolic model and perform two kinds of formal verification. The reachability analysis shows that a Man-In-The-Middle attack is present. Also, a design vulnerability in one cryptography primitive makes the scheme insecure. For both cases, we provide solutions.