Issue #96
Paper of the Week:
Paper Title: IPDL: A Simple Framework for Formally Verifying Distributed Cryptographic Protocols.
TLDR:
Although there have been many successes in verifying proofs of non-interactive cryptographic primitives such as encryption and signatures, formal verification of interactive cryptographic protocols is still a nascent area.
While in principle, it seems possible to extend general frameworks such as Easy- crypt to encode proofs for more complex, interactive protocols, a big challenge is whether the human effort would be scalable enough for proof mechanization to eventually acquire mainstream usage among the cryptography community.
This paper works toward closing this gap by introducing a simple framework, Interactive Probabilistic Dependency Logic (IPDL), for reasoning about a certain well-behaved subset of cryptographic protocols.
A primary design goal of IPDL is for formal cryptographic proofs to resemble their on-paper counterparts. To this end, IPDL includes an equational logic to reason about approximate observational equivalence (i.e., computational indistinguishability) properties between protocols.
IPDL adopts a channel-centric core logic, which decomposes the behavior of the protocol into the behaviors along each communication channel. It supports straight-line programs with statically bounded loops.
The use of IPDL is demonstrated by a number of case studies, including a multi-use, secure message communication protocol, a multi-party coin toss with abort protocol, several oblivious transfer constructions, as well as the two- party GMW protocol for securely evaluating general circuits.
A mechanization of the IPDL proof system is provided and the case studies in Coq, and the code is open sourced.
Authors: Greg Morrisett*, Elaine Shi†, Kristina Sojakova‡, Xiong Fan§, and Joshua Gancher✜,
Affiliations: * Cornell Tech, † Carnegie Mellon University, ‡ INRIA, § University of Maryland, ✜ Cornell University.
Security:
1. Paper Title: A Security Framework for Distributed Ledgers.
Summary: The first framework for defining and analyzing the security of general distributed ledgers, with an ideal distributed ledger functionality.
Authors: Christoph Egger*, Mike Graf†, Ralf Kusters†, Daniel Rausch†, Viktoria Ronge*, and Dominique Schroder*
Affiliations: * Friedrich-Alexander University Erlangen-Nurnberg and † University of Stuttgart.
Privacy:
No papers.
Scalability:
No papers.
Proofs:
No papers.
Consensus:
1. Paper Title: Fast Validated Byzantine Broadcast.
Summary: A new broadcast formulation named partially synchronous validated Byzantine broadcast (psync-VBB) that solves a single-shot of BFT replication.
Authors: Ittai Abraham*, Kartik Nayak†, Ling Ren, Zhuolun Xiang
Affiliations: * VMware Research, † Duke University, and ‡ University of Illinois at Urbana-Champaign.
Tokenomics:
No papers.
Conferences’ Videos:
This newsletter is for informational purposes only. This content does not in any way constitute an offer or solicitation of an offer to buy or sell any investment solution or recommendation to buy or sell a security; nor it is to be taken as legal, business, investment, or tax advice. In fact, none of the information in this or other content on zk Capital should be relied on in any manner as advice. None of the authors, contributors, or anyone else connected with zk Capital, in any way whatsoever, can be responsible for your use of the information contained in this newsletter.