Skip to main content
New
Stack Overflow Jobs powered by Indeed: A job site that puts thousands of tech jobs at your fingertips (U.S. only). Search jobs
40 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 ...
Biv's user avatar
  • 9,988
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 ...
Squeamish Ossifrage's user avatar
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 ...
Biv's user avatar
  • 9,988
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/...
e-sushi's user avatar
  • 17.9k
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 ...
fgrieu's user avatar
  • 142k
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 ...
Squeamish Ossifrage's user avatar
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 ...
Geoffroy Couteau's user avatar
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 ...
dade's user avatar
  • 1,323
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 ...
Luis Casillas's user avatar
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 ...
Squeamish Ossifrage's user avatar
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 ...
scof007's user avatar
  • 141
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, ...
ads's user avatar
  • 111
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 \...
poncho's user avatar
  • 148k
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 ...
Geoffroy Couteau's user avatar
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 ...
fgrieu's user avatar
  • 142k
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 ...
Mark Schultz-Wu's user avatar
  • 13.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{...
fgrieu's user avatar
  • 142k
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 ...
DannyNiu's user avatar
  • 9,409
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 ...
Biv's user avatar
  • 9,988
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 ...
Changyu Dong's user avatar
  • 4,178
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 ...
István András Seres's user avatar
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 ...
Squeamish Ossifrage's user avatar
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 /...
Maarten Bodewes's user avatar
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 ...
poncho's user avatar
  • 148k
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 ...
hlz2103's user avatar
  • 369
3 votes
Accepted

ECDSA-SHA256 HTTP Signature String Construction

Works for me: ...
dave_thompson_085's user avatar
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 ...
Luis Casillas's user avatar
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 ...
Paul Uszak's user avatar
  • 15.5k
2 votes

Can a device prove the identity of its own code?

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 ...
fgrieu's user avatar
  • 142k
2 votes

Can a device prove the identity of its own code?

Yes, with caveats*, this is possible without modifying hardware assuming the device has a TPM. The verification technique is called remote attestation. A TPM can be used in this way to verify software'...
forest's user avatar
  • 15.3k

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