========
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+.