Schedule

  • 9:00 - 9:50 Arrival
  • 9:50 - 10:00 Opening remarks from the University of Surrey President and Vice-Chancellor, Prof. Stephen Jarvis
  • 10:00 - 10:45 Rod Chapman (Amazon Web Services), Formal is fast: verification and optimization of crypto code at AWS
  • 10:45 - 11:15 Coffee break
  • 11:15 - 12:00 Chaoyun Li (University of Surrey), Towards Efficient Post-Quantum Cryptography: From Standards to Implementations
  • 12:00 - 13:30 Lunch
  • 13:30 - 14:15 Chloe Martindale (University of Bristol)
  • 14:15 - 14:30 Short break
  • 14:30 - 15:15 Amit Deo (Zama)
  • 15:15 - 15:45 Coffee break
  • 15:45 - 16:30 Eamonn Postlethwaite (King’s College London), Cool + Cruel = Dual, and New Benchmarks for Sparse LWE
  • 16:30 - 17:00 Lightning talks
  • 17:00 - 18:00 Reception

Registration

Registration is free but required. The registration will close at 23.59 on Wednesday 21st January, or beforehand if we reach full capacity. Please register here.

Speakers/Talks

Rod Chapman, Formal is fast: verification and optimization of crypto code at AWS

This presentation will go over our approach to formal verification of cryptographic code at AWS, concentrating on our recent efforts with ML-KEM and ML-DSA. We’ll cover our approach to assembly-language verification, and how we are verifying type-safety of C code within AWS-LC. Proof also enables “fearless optimization” of crypto code, where proofs of correctness and/or equivalence preserve functional behaviour while allowing and inspiring non-trivial performance improvements. We’re also using automated super-optimization of assembly language for our Graviton processors to unlock performance gains on specific micro-architectures. These technical approaches will be illustrated by the mlkem-native library - an open-source implementation of the recently-standardized ML-KEM algorithm that combines formal verification with state-of-the-art performance on all major platforms.

Bio: Rod is a senior principal applied scientist within the Cryptography group of Amazon Web Services. He specializes in the design, development and verification of cryptographic software, and has particular experience with programming language design and automated reasoning technologies. He also coaches development teams and leadership in high-assurance software development disciplines, technologies, and processes. He is a Fellow of the IET and an honorary visiting professor at the University of York.

Eamonn Postlethwaite, Cool + Cruel = Dual, and New Benchmarks for Sparse LWE

We describe a dimension reduction framework for the dual attack against the bounded distance decoding problem. Specialising to LWE (average case bounded distance decoding) we show that a known dual attack [Albrecht, EUROCRYPT 2017] falls into our framework and in particular show that the apparently novel ‘Cool and Cruel’ (C+C) attack is an instantiation of this known dual attack. Furthermore we prove that the C+C ‘phenomenon’ is an expression of the geometry of the well known Z-shape basis in qary lattices, despite claims to the contrary. Finally, we show that a correctly parametrised primal attack outperforms C+C both in the originally studied and new parameter regimes.

Bio: Eamonn Postlethwaite is a lecturer at King’s College London specialising in constructive and cryptanalytic aspects of post quantum cryptography. Prior to this he held a postdoctoral position at Centrum Wiskunde en Informatica in Amsterdam and wrote his PhD at Royal Holloway, University of London.

Chaoyun Li, Towards Efficient Post-Quantum Cryptography: From Standards to Implementations

Bio: Chaoyun Li is currently a lecturer in the Surrey Centre for Cyber Security at University of Surrey. He received the Ph.D. degree from COSIC, KU Leuven, Belgium in 2020. He was a postdoctoral researcher at COSIC, KU Leuven from 2020 to 2023, which was funded by an FWO postdoc fellowship. His research covers the full spectrum of cryptography and security, ranging from theoretical foundations to implementations and applications. His current research projects include fast and secure implementation of quantum-safe cryptography, mathematical and physical attacks, and data privacy.

Venue

UK Crypto Day will be held in the lecture theatre M of the LT Block, Stag Hill Campus, Guildford.

Room LTM,
Lecture Theatre Block,
Stag Hill Campus,
University of Surrey,
Guildford,
GU2 7XH

To locate the LT Block within the campus, you can use the following maps:

Accessibility information for the LT Block can be found clicking here.

Transport options

Stag Hill Campus can be reached by train, coach and car. Travel information can be found clicking here.

The closest railway station is Guildford. From the platform, follow signs saying “University” to the rear exit of the station (Guildford Park Rd). From there, you can either follow a 10-15 minutes walk (1.2 miles), or take the bus #1 from the Guildford Station (Stop D) bus stop on Guildford Park Rd, alighting at University of Surrey AX Building.

Contacts

General Chair: Rob Granger. For programme enquiries please email Catalin Dragan (c.dragan at surrey.ac.uk), for local organisation enquires, please email Fernando Virdia (f.virdia at surrey.ac.uk).

To propose a lightning talk (max. four minutes), please email Catalin with the subject “UK Crypto Day: lightning talk” and include your title and how long you will need.

We are looking forward to seeing you in Guildford!

Thanks

UK Crypto Day at Surrey was organised with support from: