======== Agenda ======== 1045h: Koustabh Gosh - Universal Hashing Based on Field Multiplication and (Near-)MDS Matrices 11:30h: coffee break 11:45h: Chengly Jin - Towards Remote Verifiable Computation without Digital Secrets 12:30h: Lunch 14:00h: Lisa Kohl - Oblivious Transfer with Constant Computational Overhead 14:45h: coffee break 15:00h: Matthias Meijers - Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+. Abstracts: Koustabh Gosh (RU) Title: Universal Hashing Based on Field Multiplication and (Near-)MDS Matrices Abstract: In our work, we propose a new construction for building universal hash functions, a specific instance called multi-265, and provide proofs for their universality. Our construction follows the key-then-hash parallel paradigm. In a first step it adds a variable length input message to a secret key and splits the result in blocks. Then it applies a fixed-length public function to each block and adds their results to form the output. The innovation presented in this work lies in the public function: we introduce the multiply-transform-multiply-construction that makes use of field multiplication and linear transformations. We prove upper bounds for the universality of key-then-hash parallel hash functions making use of a public function with our construction provided the linear transformation are maximum-distance-separable (MDS). We additionally propose a concrete instantiation of our construction, multi-265, where the underlying public function uses a near-MDS linear transformation and prove it similar level of universality. Chenglu Jin (CWI) Title: Towards Remote Verifiable Computation without Digital Secrets Abstract: The development of secure processor architecture technology has seen many challenges. It turns out difficult to implement efficient resource sharing and at the same time eliminate or protect against side channels as a result of shared caches and other buffers. For this reason, implemented hardware isolation cannot provide confidential computing (as of yet). Nevertheless, the hardware isolation for access control as implemented by micro code and added circuitry cannot be circumvented and this allows for verifiable computation. However, even though computations can be isolated in enclaves, how can we provide remote attestation of computed output? Remote attestation requires digital secrets which may leak due to side channels. We show two puzzle pieces which together can be used to implement remote attestation without secure digital computation or digital secrets: We use a strong PUF for masking ‘session signing keys’ and we use these in a new one-time signature primitive. In essence, computing a signature for an output boils down to directly reading out a signature from unmasked digital storage. Lisa Kohl (CWI) Title: Oblivious Transfer with Constant Computational Overhead Abstract: The computational overhead of a cryptographic task is the asymptotic ratio between the computational cost of securely realizing the task and that of realizing the task with no security at all. Ishai, Kushilevitz, Ostrovsky, and Sahai (STOC 2008) showed that secure two-party computation of Boolean circuits can be realized with constant computational overhead, independent of the desired level of security, assuming the existence of an oblivious transfer (OT) protocol and a local pseudorandom generator (PRG). However, this only applies to the case of semi-honest parties. A central open question in the area is the possibility of a similar result for malicious parties. This question is open even for the simpler task of securely realizing many instances of a constant-size function, such as OT of bits. We settle the question in the affirmative for the case of OT, assuming a standard OT protocol, a slightly stronger "correlation-robust" variant of a local PRG, and a standard sparse variant of the Learning Parity with Noise (LPN) assumption. We achieve this by constructing a constant-overhead pseudorandom correlation generator, which allows to generate a large number of pseudorandom instances of bit-OT by locally expanding short, correlated seeds. In this talk, I will give an overview of our result and discuss applications. This is joint work with Elette Boyle, Geoffroy Couteau, Niv Gilboa, Yuval Ishai, Nicolas Resch and Peter Scholl. Matthias Meijers (TU/e) Title: Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+. 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 Hülsing 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. 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 Hülsing 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+.