<jats:title>Abstract</jats:title><jats:p>We consider the<jats:italic>theoretically sound</jats:italic>selection of cryptographic parameters, such as the size of algebraic groups or RSA keys, for TLS 1.3 in practice. While prior works gave security proofs for TLS 1.3, their security loss is<jats:italic>quadratic</jats:italic>in the total number of sessions across all users, which due to the pervasive use of TLS is huge. Therefore, in order to deploy TLS 1.3 in a theoretically sound way, it would be necessary to compensate this loss with unreasonably large parameters that would be infeasible for practical use at large scale. Hence, while these previous works show that in principle the design of TLS 1.3 is secure in an asymptotic sense, they do not yet provide any useful<jats:italic>concrete</jats:italic>security guarantees for real-world parameters used in practice. In this work, we provide a new security proof for the cryptographic core of TLS 1.3 in the random oracle model, which reduces the security of TLS 1.3<jats:italic>tightly</jats:italic>(that is, with constant security loss) to the (multi-user) security of its building blocks. For some building blocks, such as the symmetric record layer encryption scheme, we can then rely on prior work to establish tight security. For others, such as the RSA-PSS digital signature scheme currently used in TLS 1.3, we obtain at least a<jats:italic>linear</jats:italic>loss in the number of users, independent of the number of sessions, which is much easier to compensate with reasonable parameters. Our work also shows that by replacing the RSA-PSS scheme with a tightly secure scheme (e.g., in a future TLS version), one can obtain the first fully tightly secure TLS protocol. Our results enable a theoretically sound selection of parameters for TLS 1.3, even in large-scale settings with many users and sessions per user.</jats:p>