39
votes
Accepted
Formal verification in cryptography
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 ...
- 9,959
19
votes
Accepted
What is the difference between signatures and VRF?
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 ...
- 47.6k
12
votes
Accepted
Is there a formal language to define a cryptographic protocol?
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 ...
- 9,959
10
votes
How does one verify a GPG/PGP key revocation?
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/...
- 17.7k
9
votes
Accepted
Is there a way to get time from signature? Or is it possible to ensure the message was signed at the time that it says it was signed?
There is no way to get time of signature from a standard ECDSA signature: it does not embed recoverable information†.
And under the conditions in this related question or messages with structure ...
- 137k
8
votes
Verify partial message given hash of full message
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 ...
- 47.6k
7
votes
Accepted
Verifiable delay functions vs Proof of Sequential Work
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 ...
- 18.9k
5
votes
Proof of encrypted content
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 ...
- 1,323
5
votes
Accepted
Simple application of verifiable random function?
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 ...
- 47.6k
5
votes
Accepted
Quality test for an hardware source of randomness
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 ...
- 14.4k
4
votes
Accepted
Only allow specific types of data to be transmitted via an end-to-end encryption service
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, ...
- 111
4
votes
Accepted
How to calculate $v_k(s)$ in Quadratic Arithmetic Program?
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 ...
- 8,072
4
votes
Formal verification in cryptography
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 ...
- 141
4
votes
Accepted
Lightweight primality certificates for untrusted DH parameters
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 \...
- 143k
4
votes
Accepted
How can I prove the result of a long computation with a short string?
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 ...
- 18.9k
4
votes
Accepted
Is the verification process in ECDSA the same or different from in RSA?
TL;DR: the signature verification process in ECDSA is very different from the one in RSA. The question's description of these signature schemes is incorrect for ECDSA, approximate for RSA.
Alice who ...
- 137k
4
votes
How can 4 users generate a provable fair random number?
There's quite a bit of relevant cryptographic literature on this topic. Significant sticking points are the dual requirements of
The situation where a player disconnects from the casino server as
...
- 11.3k
4
votes
When using ECDSA P-384 for signing and verifying messages, should the public key be also included **INSIDE** the message before signing?
Leaving the JSON formatting aside, the question considers a server receiving public key $\mathrm{pk}$, an ECDSA signature $S$, and message $M$; and asks if the signature should be on $M$ or $\mathrm{...
- 137k
4
votes
Is there a way to get time from signature? Or is it possible to ensure the message was signed at the time that it says it was signed?
There needs to be a timestamping authority (TSA), but your need deviates slightly from what it achieves.
A signature from a TSA only guarantees the data existed before the said timestamp, where as you ...
- 8,648
3
votes
Why is cryptographic model not considered formal methods?
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 ...
- 9,959
3
votes
How can I formally verify fuzzy commitment scheme based security protocol?
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 ...
- 9,959
3
votes
How can I generate large primes for Pedersen commitment?
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 ...
- 4,138
3
votes
Accepted
Is this an error in the Pinocchio Protocol paper
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 ...
- 1,164
3
votes
Verify partial message given hash of full message
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 ...
- 47.6k
3
votes
Certificate validation on an IoT device using few bytes
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 /...
- 91.2k
3
votes
Accepted
Certificate validation on an IoT device using few bytes
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 ...
- 143k
3
votes
Proving I can solve an equation without disclosing the solution (zero-knowledge proof)
For the discrete case, you can just use any zk-SNARK that generalizes over arithmetic circuits.
There is no direct way to do a zero-knowledge proof over the reals. However, you can map linear ...
- 359
3
votes
Accepted
2
votes
Universally verifiable random beacon
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 ...
- 14.4k
2
votes
Universally verifiable random beacon
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 ...
- 15k
Only top scored, non community-wiki answers of a minimum length are eligible