Module prio::pcp[−][src]

Expand description

(NOTE: This module is experimental. Applications should not use it yet.) This module implements a fully linear PCP (“Probabilistically Checkable Proof”) system based on [BBC+19, Theorem 4.3].

Overview

The proof system is comprised of three algorithms. The first, prove, is run by the prover in order to generate a proof of a statement’s validity. The second and third, query and decide, are run by the verifier in order to check the proof. The proof asserts that the input is an element of a language recognized by an arithmetic circuit. For example:

use prio::pcp::types::Boolean;
use prio::pcp::{decide, prove, query, Value};
use prio::field::{random_vector, FieldElement, Field64};

// The prover generates a proof `pf` that its input `x` is a valid encoding
// of a boolean (either `true` or `false`). Both the input and proof are
// vectors over a finite field.
let input: Boolean<Field64> = Boolean::new(false);

// The verifier chooses "joint randomness" that that will be used to
// generate and verify a proof of `x`'s validity. In proof systems like
// [BBC+19, Theorem 5.3], the verifier sends the prover a random challenge
// in the first round, which the prover uses to construct the proof.
let joint_rand = random_vector(input.joint_rand_len()).unwrap();

// The prover and verifier choose local randomness it uses to check the proof.
let prove_rand = random_vector(input.prove_rand_len()).unwrap();
let query_rand = random_vector(input.query_rand_len()).unwrap();

// The prover generates the proof.
let proof = prove(&input, &prove_rand, &joint_rand).unwrap();

// The verifier queries the proof `pf` and input `x`, getting a
// "verification message" in response. It uses this message to decide if
// the input is valid.
let verifier = query(&input, &proof, &query_rand, &joint_rand).unwrap();
let res = decide(&input, &verifier).unwrap();
assert_eq!(res, true);

If an input is not valid, then the verification step will fail with high probability:

use prio::pcp::types::Boolean;
use prio::pcp::{decide, prove, query, Value};
use prio::field::{random_vector, FieldElement, Field64};

use std::convert::TryFrom;

let input = Boolean::try_from(((), vec![Field64::from(23)].as_slice())).unwrap(); // Invalid input
let joint_rand = random_vector(input.joint_rand_len()).unwrap();
let prove_rand = random_vector(input.prove_rand_len()).unwrap();
let query_rand = random_vector(input.query_rand_len()).unwrap();
let proof = prove(&input, &prove_rand, &joint_rand).unwrap();
let verifier = query(&input, &proof, &query_rand, &joint_rand).unwrap();
let res = decide(&input, &verifier).unwrap();
assert_eq!(res, false);

The “fully linear” property of the proof system allows the protocol to be executed over secret-shared data. In this setting, the prover uses an additive secret sharing scheme to “split” its input and proof into a number of shares and distributes the shares among a set of verifiers. Each verifier queries its input and proof share locally. One of the verifiers collects the outputs and uses them to decide if the input was valid. This procedure allows the verifiers to validate a user’s input without ever seeing the input in the clear:

use prio::pcp::types::Boolean;
use prio::pcp::{decide, prove, query, Value, Proof, Verifier};
use prio::field::{random_vector, split_vector, FieldElement, Field64};

use std::convert::TryFrom;

// The prover encodes its input and splits it into two secret shares. It
// sends each share to two aggregators.
let input: Boolean<Field64> = Boolean::new(true);
let input_shares: Vec<Boolean<Field64>> = split_vector(input.as_slice(), 2)
    .unwrap()
    .into_iter()
    .map(|data| Boolean::try_from((input.param(), data.as_slice())).unwrap())
    .collect();

let joint_rand = random_vector(input.joint_rand_len()).unwrap();
let prove_rand = random_vector(input.prove_rand_len()).unwrap();
let query_rand = random_vector(input.query_rand_len()).unwrap();

// The prover generates a proof of its input's validity and splits the proof
// into two shares. It sends each share to one of two aggregators.
let proof = prove(&input, &prove_rand, &joint_rand).unwrap();
let proof_shares: Vec<Proof<Field64>> = split_vector(proof.as_slice(), 2)
    .unwrap()
    .into_iter()
    .map(Proof::from)
    .collect();

// Each verifier queries its shares of the input and proof and sends its
// share of the verification message to the leader.
let verifier_shares = vec![
    query(&input_shares[0], &proof_shares[0], &query_rand, &joint_rand).unwrap(),
    query(&input_shares[1], &proof_shares[1], &query_rand, &joint_rand).unwrap(),
];

// The leader collects the verifier shares and decides if the input is valid.
let verifier = Verifier::try_from(verifier_shares.as_slice()).unwrap();
let res = decide(&input_shares[0], &verifier).unwrap();
assert_eq!(res, true);

Note that the secret sharing provided by crate::field::split_vector is not the most efficient possible. A much more efficient secret sharing scheme is implemented in the crate::vdaf module.

The fully linear PCP system of [BBC+19, Theorem 4.3] applies to languages recognized by arithmetic circuits over finite fields that have a particular structure. Namely, all gates in the circuit are either affine (i.e., addition or scalar multiplication) or invoke a special sub-circuit, called the “gadget”, which may contain non-affine operations (i.e., multiplication). For example, the Boolean type uses the Mul gadget, an arity-2 circuit that simply multiples its inputs and outputs the result.