POPL 2024
Sun 14 - Sat 20 January 2024 London, United Kingdom
Wed 17 Jan 2024 16:50 - 17:10 at Turing Lecture - Domain-Specific Languages Chair(s): Satnam Singh

Differential cryptanalysis is a powerful algorithmic-level attack, playing a central role in evaluating the security of symmetric cryptographic primitives. In general, the resistance against differential cryptanalysis can be characterized by the maximum differential characteristic probability. In this paper, we present generic and extensible approaches based on mixed integer linear programming (MILP) to bound such probability. We design a high-level cryptography-specific language EasyBC tailored for block ciphers and provide various rigorous procedures, formulated as differential denotational semantics, to automate the generation of MILP from block ciphers written in EasyBC. We implement an open-sourced tool that provides support for fully automated resistance evaluation of block ciphers against differential cryptanalysis. The tool is extensively evaluated on 22 real-life cryptographic primitives including all the 10 finalists of the NIST lightweight cryptography standardization process. The experiments confirm the expressivity of EasyBC and show that the tool can effectively prove the resistance against differential cryptanalysis for all cryptographic primitives under consideration. EasyBC makes resistance evaluation against differential cryptanalysis easily accessible to cryptographers.

Wed 17 Jan

Displayed time zone: London change

16:50 - 18:10
Domain-Specific LanguagesPOPL at Turing Lecture
Chair(s): Satnam Singh Groq
16:50
20m
Talk
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
POPL
Pu Sun ShanghaiTech University, Fu Song State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, and University of Chinese Academy of Sciences Beijing, China, Yuqi Chen ShanghaiTech University, China, Taolue Chen University of London
17:10
20m
Talk
A Core Calculus for Documents: Or, Lambda: The Ultimate Document
POPL
Will Crichton Brown University, Shriram Krishnamurthi Brown University
Pre-print
17:30
20m
Talk
Validation of Modern JSON Schema: Formalization and Complexity
POPL
Lyes Attouche Université Paris-Dauphine -- PSL, Mohamed-Amine Baazizi Sorbonne Université, Dario Colazzo Université Paris-Dauphine -- PSL, Giorgio Ghelli Universita di Pisa, Carlo Sartiani Università della Basilicata, Stefanie Scherzinger Universität Passau
DOI
17:50
20m
Talk
Shoggoth - A Formal Foundation for Strategic Rewriting
POPL
Xueying Qin The University of Edinburgh, Liam O'Connor University of Edinburgh, Rob van Glabbeek The University of Edinburgh, Peter Hoefner Australian National University, Ohad Kammar University of Edinburgh, Michel Steuwer TU Berlin; University of Edinburgh
Pre-print