# Tag Info

35

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 ...

13

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 ...

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 : ...

9

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 ...

8

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 ...

6

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 ...

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

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 ...

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

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 ...

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

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

Can this be done? In general, there is a way: you can prove the statement you sketch using zero-knowledge proofs. Due to  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 ... 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 < pq > \sqrt{p}q \mid p-1g^q \equiv 1 \pmod pq$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 ... 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 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 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). ... 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 ... 3 The first part of the question is answered in the comments. Regarding the second part, yes, indeed, you are right! It's a typo in the Pinocchio paper, Section 2.3. Protocol 1., you also linked. The problem is that the left hand side of the verification equation enumaretes the I/O related coefficients twice in the left wire polynomial, V, therefore$g^{v_0}.g^...

3

Suppose you found an error-detecting code $f(H(m), m')$ (forget random oracles, second-preimage resistance, etc.) with the following properties: $|H(m)| = O(1)$, i.e. the checksum overhead is independent of the message length. $f(H(m_0 \mathbin\| m_1), m_0) = f(H(m_0 \mathbin\| m_1), m_0 \mathbin\| m_1) = 1$ $f(H(m_0 \mathbin\| m_1), m_0 + \delta) = 0$ with ...

3

Generally you'd let the device establish a symmetric / secret key first, e.g. using ECDH and then use that secret key with a MAC algorithm to perform the message authentication. In that case 16 bytes / 128 bits is plenty. For direct signatures, the BLS signature scheme is probably still the best out there, but for 128 bit level encryption - the lowest we ...

3

I'm asking if you guys know some method/algorithme to do this verification with only 17bytes max When you talk about public key algorithms with signatures that short, the number of options aren't great. You might be able to use a BLS signature with a specially constructed small pairing friendly curve; however the security wouldn't be that overwhelming (...

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

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

No, a device can't "prove the identity of its own code" assuming no hardware modification, if we want this secure and achieved automatically from arbitrary software image made available in machine form representing what's supposed to be the executable code, at least when said image is in part adversarially built (and arguably neither if it is built per ...

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