BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Drupal iCal API//EN
X-WR-CALNAME:Events items teaser
X-WR-TIMEZONE:America/Toronto
BEGIN:VTIMEZONE
TZID:America/Toronto
X-LIC-LOCATION:America/Toronto
BEGIN:DAYLIGHT
TZNAME:EDT
TZOFFSETFROM:-0500
TZOFFSETTO:-0400
DTSTART:20260308T070000
END:DAYLIGHT
BEGIN:STANDARD
TZNAME:EST
TZOFFSETFROM:-0400
TZOFFSETTO:-0500
DTSTART:20251102T060000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
UID:69d80959e386a
DTSTART;TZID=America/Toronto:20260417T103000
SEQUENCE:0
TRANSP:TRANSPARENT
DTEND;TZID=America/Toronto:20260417T113000
URL:https://uwaterloo.ca/combinatorics-and-optimization/events/crypto-readi
 ng-group-maggie-simmons-formally-verified
SUMMARY:Crypto Reading Group - Maggie Simmons-Formally Verified Correctness
 \nBounds for Lattice-Based Cryptography
CLASS:PUBLIC
DESCRIPTION:SPEAKER:\n\n Maggie Simmons\n\nAFFILIATION:\n University of Wat
 erloo\n\nLOCATION:\n MC 6029\n\nABSTRACT:\n\nDecryption errors play a cruc
 ial role in the security of KEMs based on\n\nFujisaki-Okamoto because the 
 concrete security guarantees provided by \nthis transformation directly de
 pend on the probability of such an\nevent \nbeing bounded by a small real 
 number. In this paper we present an \napproach to formally verify the clai
 ms of statistical probabilistic \nbounds for incorrect decryption in latti
 ce-based KEM constructions.\nOur \nmain motivating example is the PKE encr
 yption scheme underlying\nML-KEM. \nWe formalize the statistical event tha
 t is used in the literature to \nheuristically approximate ML-KEM decrypti
 on errors and confirm that\nthe \nupper bounds given in the literature for
  this event are correct. We \nconsider FrodoKEM as an additional example\,
  to demonstrate the wider \napplicability of the approach and the verifica
 tion of a correctness \nbound without heuristic approximations. We also di
 scuss other \n(non-approximate) approaches to bounding the probability of 
 ML-KEM \ndecryption.
DTSTAMP:20260409T201729Z
END:VEVENT
END:VCALENDAR