owned this note
owned this note
Published
Linked with GitHub
 **Home Edition**
# Discussion notes #4.1: SoK - Formalising Σ-Protocols and Commitment Schemes using CryptHOL
Presenter: David Butler
Authors:
- David Aspinall
- David Butler
- Adria Gascon
- Andreas Lochbilher
To be presented on 2020-04-30.
Resources:
* [Latest PDF version](https://docs.zkproof.org/pages/standards/accepted-workshop3/sok-sigma_protocols_crypthol.pdf)
* [Miro Whiteboard](https://zkproof.org/workshop3-board)
* [SoK Working Group](https://community.zkproof.org/g/SOK_WG_CRYPTHOL)
* [Additional related links](https://hackmd.io/@HtwXZr-PTFCniCs7fWFSmQ/B1AwbdI_8)
----
## Real-time notes
_Note taker: Daira.
> Others are welcome to augment/annotate using notes. Add your name. ---Eran Tromer
> ---Markulf Kohlweiss
Bio: David Butler worked on verification of ZK and aircrafts/spacecrafts
Problem statement: Formalizing ZK (and commitments, though not in this talk). Investigate how formal verification can help with the standardization process.
Motivation:
- we generate more proofs than we carefully verify --S. Halevi
- many proofs in crypto have become essentially unverifiable --Bellare and Rogaway
- Cryptographic proofs are rare prickly beasts --Bristol blog
- etc.
Example: Isabelle/HOL proof of Schnorr Sigma-protocol
Machine-checked proofs give:
- higher guarantees of proof correctness
- explicit definitions and assumptions (still need to be checked by human 'verifier')
- guarantee of no gaps
- increased rigour.
Tools: CertiCrypt (Coq), CryptHOL (Isabelle/HOL), FCF (Coq), EasyCrypt, ProVerif (pi-calculus)
How can we integrate formal methods with the standardization process?
Summary of Sigma protocols
A "conversation" is the tuple of messages sent by prover and verifier.
In Sigma protocols we aim for honest-verifier ZK.
Problem with formalizing OR construction for Sigma protocols.
To prove completenes of the composition one needs that the simulator works for 'all' x, not just for x in the language.
> Q: how is 'all' defined? valid_pub? --Markulf Kohlweiss
Solution: simulator should always output a valid conversation. This fix was in Cramer's PhD but didn't filter down into modern textbook definitions.
Formal methods can capture these subtleties.
Introduction to Isabelle theorem prover. Well-established, used for proof of Kepler conjecture.
CryptHOL is a framework for crypto that provides a probabilistic programming framework.
Modularization comes naturally in Isabelle. E.g. we can prove correctness of generic constructions such as
Sigma protocol => commitment scheme.
CryptHOL uses Isabelle's module systems (locales) to define generic protocols and defines concrete protocols using a probabiltiy monad.
This also allows to define generic compilers such as the OR compiler that takes two Sigma-protocols and generates a Sigma-protocol for the OR-relation.
Some problems with definitions will only be found by considering more complicated constructions/compositions.
Formal proof could focus on parts where intuition breaks down.
Can be used as a prototyping tool for protocols.
Feedback from formal methods to standardization, e.g. TLS 1.3.
----
Questions:
* Justin Thaler: "The more complicated the protocol, the more man-hours. Do you have a sense of whether it's feasible to attempt to formalize complete modern protocols?"
- Successes such as formalizing UC. General state-of-the-art protocols are a bit beyond us.
- Justin: It could be worthwhile to tackle building blocks such as sumcheck etc.
- Markulf: Cédric Fournet, Chantal Keller, Vincent Laporte: A Certified Compiler for Verifiable Computing. CSF 2016: 268-280
- Justin: barrier to entry of tools is very high; tools are developed outside the crypto community.
* Yael Kalai: "Going back to the goal of formal verification, is the goal to convince myself, or to convince the community?"
- Indeed, and you can either use it as a prototyping environment that gives you confidence in a paper proof. It would be great to have proofs available for larger protocols in the long term.
- Important to be able to reference standard definitions.
* Michele Orrù: [didn't catch the question]
- Current tools aren't focussed on verifying implementations.
- Proofs do consider hardness assumptions.
- Mary Maller: often easier to have a division of work between human and machine verification.
- Justin: The link between paper and machine proofs is critical, since problems can be pushed to that interface.
* Justin Thaler: "In the TLS example, community settled on one protocol and there was great effort to make it secure. Not the same situation in the zk community."
* Thomas Kerber: "Field is moving so quickly, and it takes a long time to apply formal methods. Even if you had a proof of, say, Groth16, no guarantee anyone is using it a year later."
- Markulf: On the other hand, standardizing Sigma protocols is a good idea because they are used very often. Still many things that go wrong in practical implementations.
* Yael: "Not sure what you mean by a formal machine-checkable definition. I agree that we sometimes define the 'same' things in different ways. But I want to understand more clearly what you mean by 'formal'."
- Dave: We check a formalization of a protocol against the definition. Includes type correctness.
- Markulf: just the same definition written as a program in a formal logic.
* AntoineR: "I don't see the community reaching consensus on which proof system should rule them all; it's a matter of trade-offs. So we should formally verify Groth16. To anyone who has written R1CS, it is very complicated to do right; missing a single gate results in failing to capture the intent."
* Daira: "What is the scope of what formal methods can currently do? Give an example of a nontrivial optimization that is proven correct."
Poll: should we focus on providing definitions (and testing them) or proofs for a protocol that we care about?
Results: 76% definitions; 54% generate proofs
----
Sponsors pitch: Evan Cheng, Calibra research group (subsidiary of Facebook).
1.1m people underbanked; Calibra/Facebook wants to help with that. Cannot trust a single company to have control of infrastructure for money. Libra trying to work in the open, public protocols etc. Recognized that they need to drive cutting-edge research, with the scientific community.
----
Lightning talk: Youssef El Housni, EY blockchain team
"Optimized and secure pairing-friendly elliptic curves suitable for one layer proof composition"
https://eprint.iacr.org/2020/351
Summary of recursive verification. For efficiency, use cycle/chain of pairing-friendly elliptic curves [BCTV14, BCG+20].
Field size of one curve is equal to subgroup size of the other, and vice-versa.
Examples: MNT4/6 (e.g. MNT4/6-753 used originally in Coda), BLS12-377/SW6 used in Zexe.
This work: curve like SW6 but more efficient.
For SNARKs, we want:
- high 2-adicity (r-1 has large 2^k factor)
- for a 2-chain, use Cocks-Pinch algorithm
Use variant of Brezing--Weng to find a 761-bit curve (as opposed to 782 for SW6). Has embedding degree 6 and sextic twist, efficient optimal ate pairing, CM discriminant -3 (hence endomorphisms for efficient scalar mul).
---
**Lightning talk: Abilash Soundararajan, TruthShare
"Clean Social Media Technology - using ZKP, MPC and Game Theory"**
Proving the identity of the originator of a cybercrime and preventing spread of cybercrime content in social media platforms, including end to end encrypted platforms, is not possible without privacy violation.
Most of the social media platforms are anonymous either by user identity or by content, hence AI based systems have limited utility in establishing culpability.
Clean Social Media technology, which can help achieve the objectives with
* game theory based solution modelling
* privacy preserving zero knowledge proof based interactions between stakeholders
* secure multi party compute protocol integrating zero knowledge interactions.
The solution is designed to ensure compliance with GDPR requirements for data subjects, at the same time built on proofs which are binding, hiding and compressive time commitments.
The designed MPC protocol has the attributes of:
* multi-output and reactive by functionality
* a network model with broadcast mode for criminal content removal
* oblivious transfer for origin identification
* adversary can be both active and passive
* addresses dishonest majority fully secure MPC with solitary output.
Thus, the technology framework disincentivizes cybercrime on social media platforms, making them a cleaner and safer place for humanity to interact.
"Criminal content is not being penalized." Use ZK to help with social media moderation. Protect E2E encryption by allowing moderation compatible with E2E.
email: abilash@truthshare.tech
LinkedIn: https://www.linkedin.com/in/abilashsss/
----
Charter Ideas
Goals:
- Formalize definitions
- Formalize constructions and compositions
- Infuence standardization, integrate formalization into standardization process
Milestones:
-
----
## Discussion topics
_Suggestions welcome! Please append at the end, and the moderators will incorporate into the schedule._
~15 minutes each, by default.
1) What are the most important ways in which formalization efforts can benefit cryptographers (zk proofs in particular)?
2) What is the community's opinion on machine-hybrid proofs?
3) How could formalization be integrated into the standardization effort?
