Computer-verified proofs for FrodoKEM​ ​

​

• Collaboration with Manuel Barbosa (Max Planck Institute for Security and Privacy), and Peter Schwabe (Max Planck Institute for Security and Privacy)

• Description: FrodoKEM is a lattice-based key-encapsulation mechanism under standardization by the International Organization for Standardization (ISO) and being recommended by the German Federal Office for Information Security (BSI). FordoKEM is considered more conservative than ML-KEM in terms of security, but requires significantly larger public keys and ciphertexts. We are collaborating with international researchers to produce high-assurance implementations that come with computer-verified proofs proving both the correctness of the implementation as well as the security of the scheme.

​​​

​​

​​​​

​

Formally-verified assembly implementation of UOV​​

​

• Collaboration with Bow-Yaw Wang (Academia Sinica) and Bo-Yin Yang (Academia Sinica)

• Description: Unbalance-Oil-and-Vinegar (UOV) is a candidate for standardization of the US National Institute of Standards and Technology (NIST) and features some of the smallest signatures among all post-quantum signature schemes. We are collaborating with researchers from Academia Sinica on applying the CryptoLine formal verification tool to verify the correctness of our high-speed UOV assembly implementations.

​

​

​

​

Superoptimizing Post-Quantum Cryptography for the Arm Cortex-M7​​

​

• Collaboration with Amin Abdulrahman (Max Planck Institute for Security and Privacy)

• Description: Our SLOTHY superoptimizer (published at CHES 2024) has been used to verify a range of cryptographic primitives and a set of target platforms resulting in some of the fastest existing cryptographic implementations. We are collaborating with researchers at the Max Planck Institute for Security and Privacy to apply SLOTHY to more cryptographic schemes and more platforms, while also extending SLOTHY with more features.

​

​

​

​

Arm Neon implementations of the MAYO signature scheme​​

​

• Collaboration with Ward Beullens (IBM Research), Fabio Campos (RheinMain University of Applied Science), Sofía Celi (Brave Software), Basil Hess (IBM Research)

• Description: MAYO is one of the most promising digital signature schemes currently being considered for standardization by the US National Institute for Standards and Technology (NIST). It features one of the smallest combined public key and signature sizes of all post-quantum signature schemes. Currently high-speed implementations of MAYO only exist targeting low-end Arm microcontrollers and high-end Intel processors, thus far, no high-speed implementations targeting A-profile Arm processors have been published. We are working together with the MAYO team to produce Arm Neon implementations of MAYO which can achieve best performance on cores ranging from Raspberry Pis, smartphone processors, Apple M processors, and cloud platforms such as AWS Graviton. 

​

​

​

​

Post-Quantum FIDO​​

​

• Description: FIDO is a set of standards designed to enhance online authentication by replacing passwords with more secure, user-friendly methods using hardware tokens and cryptography. It aims to reduce the reliance on passwords by enabling strong, phishing-resistant authentication across websites and applications. As many of the features provided by FIDO require the use of public-key cryptography, they are vulnerable to quantum computer attacks and need to be migrated to post-quantum cryptography. We are collaborating with our partners in Taiwan to research the migration of FIDO to post-quantum cryptography. In particular, we are looking into migrating certain FIDO tokens to use the quantum-safe digital signature schemes ML-DSA and MAYO.