POPL 2021 (series) / CPP 2021 (series) / Certified Programs and Proofs Lightning Talks /
Formalising MPC-in-the-head-based zero-knowledge
Recent work has focused on the formalization of Zero-Knowledge and Multi-Party Computations separately. Here we combine those two strands of research and use EasyCrypt to formalise the security of a new class of Multi-Party Computation protocols from which zero-knowledge protocols can be constructed. This class includes MPC-in-the-head protocols such as ZKBoo and picnic. Moreover, this restricted class of MPC protocols allow us to seamlessly define simulator-based proofs of security, something which has previously only been done in a formal setting for MPC protocols limited to one round, or replaced by non-interference-based definitions.
| Slides (formal_mpcbased_zk.pdf) | 83KiB |
Mon 18 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
20:00 - 21:00: Lightning TalksCPP / CPP Lightning Talks at CPP Chair(s): Natarajan ShankarSRI International, USA Streamed sessions: https://youtu.be/sFMJBTtbjTc | |||
| 20:00 - 20:05 Talk | Certified Semantics for miniKanren CPP Lightning Talks Dmitry RozplokhasSaint Petersburg State University and JetBrains Research, Andrey VyatkinSaint Petersburg State University, Petr LozovSain Petersburg State University, SPbGU, Dmitri BoulytchevSaint Petersburg State University / JetBrains Research Media Attached | ||
| 20:05 - 20:10 Talk | Cameleer: a Deductive Verification Tool for OCaml CPP Lightning Talks Mário PereiraNOVA LINCS & Nova School of Sciences and Tecnhology, Antonio RavaraDepartment of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS | ||
| 20:10 - 20:15 Talk | Gradualizing the Calculus of Inductive Constructions CPP Lightning Talks Meven Lennon-BertrandInria – LS2N, Université de Nantes, Kenji MaillardInria Nantes & University of Chile, Nicolas TabareauInria, Éric TanterUniversity of Chile Pre-print | ||
| 20:15 - 20:20 Talk | Formally Verified Decentralized Exchange with Mi-Cho-Coq CPP Lightning Talks Arvid JakobssonNomadic Labs, Colin GonzálezUniversité de Paris, Irif -- Nomadic Labs, Bruno BernardoNomadic Labs, Raphaël CauderlierNomadic Labs | ||
| 20:20 - 20:25 Talk | A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers CPP Lightning Talks Sören BleikertzDigital Asset, Andreas LochbihlerDigital Asset, Ognjen MarićDigital Asset, Simon MeierDigital Asset, Phoebe NicholsDigital Asset, Matthias SchmalzDigital Asset, Ratko G. VeprekDigital Asset File Attached | ||
| 20:25 - 20:30 Talk | Specification and model checking of Tendermint consensus in TLA+ CPP Lightning Talks | ||
| 20:30 - 20:35 Talk | Formalization of Combinatorics on Words in Isabelle/HOL CPP Lightning Talks Štěpán HolubCharles University, Štěpán StarostaFaculty of Information Technology, Czech Technical University in Prague Link to publication Media Attached File Attached | ||
| 20:35 - 20:40 Talk | Formalising MPC-in-the-head-based zero-knowledge CPP Lightning Talks Nikolaj SidorencoAarhus University, Sabine OechsnerAarhus University, Bas SpittersConcordium Blockchain Research Center, Aarhus University File Attached | ||
| 20:40 - 20:45 Talk | Mechanically-checked soundness of type-based null safety CPP Lightning Talks Alexander KogtenkovSchaffhausen Institute of Technology, Switzerland Media Attached File Attached | ||
| 20:45 - 20:50 Talk | Formalising MiniSail in Isabelle CPP Lightning Talks Mark WassellUniversity of Cambridge | ||
| 20:50 - 20:55 Talk | How to verify an ASN.1 Protocol C-language Stack in Coq? CPP Lightning Talks File Attached | ||
| 20:55 - 21:00 Talk | Monadic Second-Order Logic and Pomset Languages CPP Lightning Talks Tobias KappéCornell University | ||