Abstract
As a compact representation of joint probability distributions over a dependence graph of random variables, and a tool for modelling and reasoning in the presence of uncertainty, Bayesian networks are of great importance for artificial intelligence to combine domain knowledge, capture causal relationships, or learn from incomplete datasets. Known as a NP-hard problem in a classical setting, Bayesian inference pops up as a class of algorithms worth to explore in a quantum framework. This paper explores such a research direction and improves on previous proposals by a judicious use of the utility function in an entangled configuration. It proposes a completely quantum mechanical decision-making process with a proven computational advantage. A prototype implementation in Qiskit (a Python-based program development kit for the IBM Q machine) is discussed as a proof-of-concept.

Abstract
FIDO2 is becoming a defacto standard for passwordless authentication. Using FIDO2 and WebAuthn, web applications can enable users to associate cryptographic credentials to their profiles, and then rely on an external authenticator (e.g., a hardware token plugged into the USB port) to perform strong signature-based authentication when accessing their accounts. The security of FIDO2 has been theoretically validated, but these analyses follow the threat model adopted in the FIDO2 design and explicitly exclude some attack vectors as being out of scope. In this paper we show that two of these attacks, which appear to be folklore in the community, are actually straightforward to launch in practice (user PIN extraction, impersonation and rogue key registration). We demonstrate a deployment over vanilla Linux distributions and commercial FIDO2 authenticators. We discuss the potential impact of our results, which we believe will contribute to the improvement of future versions of the protocol.

Abstract

Abstract

Abstract
This work presents a novel machine-checked tight security proof for XMSS-a stateful hash-based signature scheme that is (1) standardized in RFC 8391 and NIST SP 800-208, and (2) employed as a primary building block of SPHINCS+, one of the signature schemes recently selected for standardization as a result of NIST's post-quantum competition. In 2020, Kudinov, Kiktenko, and Fedoro pointed out a flaw affecting the tight security proofs of SPHINCS+ and XMSS. For the case of SPHINCS+, this flaw was fixed in a subsequent tight security proof by Hulsing and Kudinov. Unfortunately, employing the fix from this proof to construct an analogous tight security proof for XMSS would merely demonstrate security with respect to an insufficient notion. At the cost of modeling the message-hashing function as a random oracle, we complete the tight security proof for XMSS and formally verify it using the EasyCrypt proof assistant. (Note that this merely extends the use of the random oracle model, as this model is already required in other parts of the security analysis to justify the currently standardized parameter values). As part of this endeavor, we formally verify the crucial step common to the security proofs of SPHINCS+ and XMSS that was found to be flawed before, thereby confirming that the core of the aforementioned security proof by Hulsing and Kudinov is correct. As this is the first work to formally verify proofs for hash-based signature schemes in EasyCrypt, we develop several novel libraries for the fundamental cryptographic concepts underlying such schemes-e.g., hash functions and digital signature schemes-establishing a common starting point for future formal verification efforts. These libraries will be particularly helpful in formally verifying proofs of other hash-based signature schemes such as LMS or SPHINCS+.

Abstract
We extend and consolidate the security justification for the Dilithium signature scheme. In particular, we identify a subtle but crucial gap that appears in several ROM and QROM security proofs for signature schemes that are based on the Fiat-Shamir with aborts paradigm, including Dilithium. The gap lies in the CMA-to-NMA reduction and was uncovered when trying to formalize a variant of the QROM security proof by Kiltz, Lyubashevsky, and Schaffner (Eurocrypt 2018). The gap was confirmed by the authors, and there seems to be no simple patch for it. We provide new, fixed proofs for the affected CMA-to-NMA reduction, both for the ROM and the QROM, and we perform a concrete security analysis for the case of Dilithium to show that the claimed security level is still valid after addressing the gap. Furthermore, we offer a fully mechanized ROM proof for the CMA-security of Dilithium in the EasyCrypt proof assistant. Our formalization includes several new tools and techniques of independent interest for future formal verification results.