34

Disclaimer: I use Coq on daily basis... I have seen in some places that people use formal verification and/or computer-aided verification for cryptography. To my knowledge, there aren't that many places that do such a thing. First, let's define our concepts: Formal Verification: The act of proving the correctness of algorithms with respect to a certain ...


12

Disclaimer: I use Coq on daily basis... About the tools As you are looking for a formal verification, I would advise you to take a look at Coq. Even though mainly used by Academics, it provides a logical framework and an interface to write formal and interactive proofs. Based this language there exists some libraries dedicated to cryptographic proof : ...


11

First, you need more than just a signature, because a VRF produces both an output and a proof. To an observer, the output is uniformly distributed unless the observer also has the proof, which can be used to verify the output. With a signature scheme and a random oracle $H$, you could use a signature $s$ on a message $m$ as a proof and $h = H(s)$ as an ...


7

How does one verify a key revocation? As Jon Callas already stated: you simply don’t. In case a different wording helps, here’s a quote related to the exact same question… https://lists.gnupg.org/pipermail/gnupg-users/2014-February/049100.html … I revoked my key and on the public key server it says: "* KEY REVOKED * [not verified]" Why does ...


7

No, the user of the key does. A revocation issued by the key itself, or by a designated revoker, which is some different key. If I am going to encrypt to you, I look at the key before I do, and I look to see if your key is revoked. Similarly, if I am verifying a signature your key made, I look to see if the key is revoked.


5

NIST has a statistical test suite for testing (pseudo) random number generators. There are a number of other suites as well, such as Diehard, Dieharder, and TestU01. But all these tests can do is disprove the claim that your generator is random; they cannot prove it. So you really need, in addition, an independent argument for why your generator's output ...


5

Sharon Goldberg's research group at Boston University has a web site on VRFs with research references and applications, including key transparency in CONIKS, authenticated enumeration-resistant denial of existence in DNSSEC with NSEC5, and the Byzantine agreement protocol Algorand. Here's a quick history of how negative answers work in DNS and DNSSEC. The ...


5

You've asked for a way to hash a file into a short string $h$ so that given a partial download $c'_0 \mathbin\| c'_1 \mathbin\| c'_2 \mathbin\| \cdots \mathbin\| c'_{i-1}$ of the file that should start with $c_0 \mathbin\| c_1 \mathbin\| c_2 \mathbin\| \cdots \mathbin\| c_{i-1}$ but may have been modified in transit, you can compute some verification ...


4

Formal verification is used to verify the security services of your algorithm or your protocol. It uses specific high level modeling specification to specify your security solution and uses a back end formal verification tools to see whether or not there are security breaches or not. The outcome of the formal verification will tell you if your protocol is ...


4

One (very generalized) solution would be to use a general ZKP solution like libsnark. In libsnark (and other tools like it), you would write a function that accepts both public and private inputs, and outputs a proof that the inputs satisfy the logic of the function. This proof can then be verified, at a much lower cost than it took to generate it. E.g., ...


4

In my experience the persons doing the standardization may not know about formal methods in the first place. And even if a formal method was used, they would not know how to assess it. Note that whatever mathematical method is applied, the security of a protocol is still dependent on how the domain was modelled. If the model is even slightly incorrect, a ...


4

There are several option - none of which is trivial to implement. A bit of background first. Essentially, verifiable delegation of computation boils down to being able to prove relations between inputs and outputs, so that the verification time is way smaller than the computation time, for relations that can be computed in polynomial time. In contrast, the ...


4

Well, one possibility to generate a moderately lightweight certificate would be to use this theorem: If we have values $p, q, g$ such that: $1 < g < p$ $q > \sqrt{p}$ $q \mid p-1$ $g^q \equiv 1 \pmod p$ $q$ is prime Then $p$ is prime. So, for a certificate, we would have a list of $(p_i, g_i)$ values such that $p_{i-1}, p_i, g_i$ meet the above ...


4

A typical thing which you cannot do with a proof of sequential work is achieving time-lock encryption. In time lock encryption, you want the user to be able to retrieve the hidden message only after some time (i.e., you want to "send a message to the future", as its inventors initially put it). With a VDF, you can use the unique secret to mask the secret ...


3

This might not be the answer you are looking for, but as you are looking for a formal verification, I would advise you to take a look at Coq. Even though mainly used by Academics, it provides a logical framework and an interface to write formal and interactive proofs. Based this language there exists some libraries dedicated to cryptographic proof : ...


3

The canonical algorithm to construct the QAP polynomials from an arithmetic circuit does not yield a polynomial in the standard form ($a_0 + a_1x + \dots$), but as a set of $(x,f(x))$ points. In order to compute $f(s)$ for arbitrary $s$, as required by the protocol, you have to run some interpolation algorithm to reconstruct the polynomial from all the ...


3

Give a zero-knowledge proof that $y_1 \times y_2$ is a Quadratic Residue. [Extra verbage included because a one line answer feels too brief] If we have $y_1 = x_1^2 t^{b_1}$ and $y_2 = x_2^2 t^{b_2}$, then $y_1 y_2 = (x_1x_2)^2 t^{b_1 + b_2}$. If $b_1 = b_2$, this product is either $(x_1x_2)^2$ (if $b_1 = b_2 = 0$), or $(x_1x_2t)^2$ (if $b_1 = b_2 = 1$), ...


3

Can this be done? In general, there is a way: you can prove the statement you sketch using zero-knowledge proofs. Due to [1] we know that zero-knowledge proofs for any language in NP exist. Let us write down what you want to prove as an NP language $L$. Therefore let $\sf (sk, pk)$ be the key pair, consisting of a secret key $\sf sk$ and a public key $\sf ...


3

You can find two algorithms for generating such $p$ and $q$ in Appendix A.1, FIPS-186-4 (digital signature standard). edited to add: Essentially, the two algorithms generate a pseudorandom prime number $q$ of the desired size first, then generate a pseudorandom random number $p$ (such that $q|(p-1)$) of the desired size, and test whether $p$ is prime. If ...


2

Reform the problem. Instead of each participant picking their givee (which they give to), have them select a giver (which they receive from). Each participant randomly generates a number (appropriately large) and anonymously submits it (e.g., via the tor network) to the site. This number represents them as giver. After all participants have entered, the ...


2

In context of interactive proof systems (including zero-knowledge proofs) completeness means the same as the term correctness as used for many other (interactive) cryptographic schemes or protocols. I guess that's mainly due to historical reasons (there are even some people that use correctness instead of completeness in context of zero-knowledge proofs). ...


2

I believe a zero knowledge proof that $-1$ is a quadratric nonresidue would accomplish that. If we know that $n$ has two prime factors, and that $n \equiv 1 \pmod{4}$, then $n$ is either a product of two primes both $1 \bmod 4$, or two primes both $3 \bmod 4$. If it were the former, then $-1$ is a QR modulo $p$, and $-1$ is a QR modulo $q$, and hence $-1$ ...


2

It looks fine; whether you use the secret $S_0, S_1$ as the HMAC key, or whether you use the random value $r$ as the HMAC key; if $t' = t$, it implies that either $S_0 = S_1$, or we found a collision in the underlying hash function. I would personally suggest you use $S_0, S_1$ as the key. With HMAC, it doesn't really matter; however if we extend this to ...


2

Thinking about this and considering Paul Uszak's very useful (albeit perhaps pessimistic) remarks, one idea to consider for this is to use measurements of randomly fluctuating natural phenomena of high public interest that are published regularly by multiple independent parties that have strong incentives to provide accurate measurements. The key ideas to ...


2

There is no sensible solution to this. It is impossible, even if this was not a hypothetical question. It cannot be done for primarily two reasons:- You cannot have the nodes measure any analogue quantity. Analogue measurement noise will govern the accuracy of the reading. Coupled with the typical hash based randomness extractors, the avalanche effect ...


2

Disclaimer: I'm currently doing a PhD in Formal Methods and Cryptography and I'm not really sure of my answer. The first application of Formal Methods is to be applied to pieces of software. The goal is to prove security properties on them. These are usually safety critical softwares (those you find in planes, trains, nuclear facilities...) This field is ...


2

This is to ensure $v$ is in the cyclic sub-group $G$ of $Z_N^*$ that has a large enough order $m=p'\cdot q'$. Moreover, with a large probability $v$ is a generator of $G$, so that $v_i=v^{s_i}$ is a one-to-one mapping from $s_i$ to $v_i$, which is important when proving correctness of the shares.


2

Yes. Say the message is $m$ and the commitment is $C$ such that $C = g^mh^r$. Since you can use verifiable encryption to prove that a given ciphertext encrypts $m$ in relation $g^m = y$ where $g$ and $y$ are also public knowledge, using the Schnorr protocol you can prove that the $m$ in relation $g^m = y$ is same as the $m$ in $C$


1

It is well known that it is not possible to achieve complete fairness in the two party setting, to agree on a random unbiased coin. See Limits on the security of coin flips when half the processors are faulty. The functionality you are looking for seems to reduce to this functionality, which in turn is not possible.


1

Theoretically it seems to be possible. First idea: If Alice and Bob have a way to verify that the information is correct one approach would be for them to give the algorithm for that to a trusted third party. Then this third party can check the information and only exchange the values if both of them are correct. If the third party is not trusted but does ...


Only top voted, non community-wiki answers of a minimum length are eligible