We present an effective methodology for the formal verification of practical cryptographic protocol implementations written in Rust. Within a single proof framework, we show how to develop machine-checked proofs of diverse properties like runtime safety, parsing correctness, and cryptographic protocol security. All analysis tasks are driven by the software developer who writes annotations in the Rust source code and chooses a backend prover for each task, ranging from a generic proof assistant like F* to dedicated crypto-oriented provers like ProVerif and SSProve Our main contribution is a demonstration of this methodology on Bert13, a portable, post-quantum implementation of TLS 1.3 written in Rust and verified both for security and functional correctness. To our knowledge, this is the first security verification result for a protocol implementation written in Rust, and the first verified post-quantum TLS 1.3 library.

WebAuthn, forming part of FIDO2, is a W3C standard for strong authentication, which employs digital signatures to authenticate web users whilst preserving their privacy. Owned by users, WebAuthn authenticators generate attested and unlinkable public-key credentials for each web service to authenticate users. Since the loss of authenticators prevents users from accessing web services, usable recovery solutions preserving the original WebAuthn design choices and security objectives are urgently needed. We examine Yubico's recent proposal for recovering from the loss of a WebAuthn authenticator by using a secondary backup authenticator. We analyse the cryptographic core of their proposal by modelling a new primitive, called Asynchronous Remote Key Generation (ARKG), which allows some primary authenticator to generate unlinkable public keys for which the backup authenticator may later recover corresponding private keys. Both processes occur asynchronously without the need for authenticators to export or share secrets, adhering to WebAuthn's attestation requirements. We prove that Yubico's proposal achieves our ARKG security properties under the discrete logarithm and PRF-ODH assumptions in the random oracle model. To prove that recovered private keys can be used securely by other cryptographic schemes, such as digital signatures or encryption schemes, we model compositional security of ARKG using composable games by Brzuska et al. (ACM CCS 2011), extended to the case of arbitrary public-key protocols. As well as being more general, our results show that private keys generated by ARKG may be used securely to produce unforgeable signatures for challenge-response protocols, as used in WebAuthn. We conclude our analysis by discussing concrete instantiations behind Yubico's ARKG protocol, its integration with the WebAuthn standard, performance, and usability aspects.

We develop a three-level hierarchy of privacy notions for (unforgeable) digital signature schemes. We first prove mutual independence of existing notions of anonymity and confidentiality, and then show that these are implied by higher privacy goals. The top notion in our hierarchy is pseudorandomness: signatures with this property hide the entire information about the signing process and cannot be recognized as signatures when transmitted over a public network. This implies very strong unlinkability guarantees across different signers and even different signing algorithms, and gives rise to new forms of private public-key authentication.

Many future electronic identity cards will be equipped with a contact-less interface. Analysts expect that a significant proportion of future mobile phones support Near Field Communication (NFC) technology. Thus, it is a reasonable approach to use the cell phone as mobile smart card terminal, which in particular supports the Password Authenticated Connection Establishment (PACE) protocol to ensure user consent and to protect the wireless interface between the mobile phone and the smart card. While there are efficient PACE implementations for smart cards, there does not seem to be an efficient and platform independent solution for mobile terminals. Therefore we provide a new implementation using the Java Micro Edition (Java ME), which is supported by almost all modern mobile phones. However, the benchmarks of our first, straightforward PACE implementation on an NFC-enabled mobile phone have shown that improvement is needed. In order to reach a user friendly performance we implemented an optimized version, which, as of now, is restricted to optimizations which can be realized using features of existing Java ME libraries.