Alice has two secret numbers, a and b. She publishes c1=E(a), c2=E(b) and c3=E(a+b). Is there an encryption system E such that anyone would be able to prove that the c3 as published by Alice is actually E(a+b)?

EDIT: Modified the question to use "anyone" instead of "Bob".

Note that this is different from homomorphic encryption. In case of homomorphic encryption Bob is able to compute E(a+b) himself, but he is not necessarily able to prove that E(a+b) as computed by Alice is correct. What's needed here is a system where Bob is not necessarily able to compute E(a+b) but is able to prove Alice's result.

-
Btw, there's a system that can be used this way outlined in the accepted answer here: crypto.stackexchange.com/questions/6732/… however it requires revealing r3 to Bob. Can we do better? –  Martin Sustrik Oct 21 '13 at 8:44
–  Ricky Demer Oct 21 '13 at 9:39
How would you approach the problem via ZKP? Sorry, I am not a cryptographer, so I'm just trying to get my head around this. –  Martin Sustrik Oct 21 '13 at 10:27
You may specify more precisely why you are requiring this feature. If you have $c_1$ and $c_2$ in an authentic fashion, then anyone can recompute $c_3'$ and compare it to the obtained $c_3$ (this operation is deterministic in homomorphic encryption schemes). You may also look here: crypto.stackexchange.com/questions/10048/… –  DrLecter Oct 21 '13 at 11:08
Imagine a game with cards. Each participant has secret information (the cards in the hand) that he doesn't want to disclose to other participants. He can also perform an operation (say exchange one of the cards) but he doesn't want to disclose the result of the operation, i.e. the resulting set of cards in the hand should remain secret. However, other participants want to ensure that he played by rules, i.e. he exchanged exacly one card. In general, the goal is to ensure that every participant plays by rules without disclosing their secret. –  Martin Sustrik Oct 21 '13 at 11:30

One example of such a system is ElGamal over a group $G$ generated by $g$. The public key is $y$ and an encryption $(x,w)$ of a message $m$ is of the form $(g^r, y^r m)$ for some integer $r$.

You have three ciphertexts $(x_1, w_1)$, $(x_2, w_2)$ and $(x_3, w_3)$ which are encryptions of $m_1$, $m_2$ and $m_1m_2$, respectively. The random integers used is $r_1$, $r_2$ and $r_3$, respectively. Note that $r_3$ isn't $r_1+r_2$, it is a random number. You want to produce a proof that the encryptions are correct.

The idea is to observe that the ciphertext $(x_1x_2/x_3, w_1 w_2 / w_3)$ is an encryption of $1$. As such, you only need to prove that it is an encryption of $1$. This amounts to proving that the logarithm of $x_1x_2/x_3$ to the base $g$ equals the logarithm of $w_1w_2/w_3$ to the base $y$, which is done using a standard proof of equality of discrete logarithms.

You asked about additively homomorphic cryptosystems, and above I outlined a solution using multiplicative ElGamal. However, the approach works just as well for an additive variant of ElGamal or Paillier.

-
Didn't @martin-sustrik said that he didn't want to use any homomorphic cryptosystem? In your solution you're assuming that anyone has access to $c_1=(x_1,w_1)$ and $c_2=(x_2,w_2)$, and if that was the case, then anyone could also compute $E(a+b)$. –  LRM Oct 23 '13 at 10:44
Observe that c3 isn't the product of c1 and c2. It's a fresh encryption of the product of the messages. Sometimes, this is important. –  K.G. Oct 23 '13 at 14:06
Yes, but still you're using a homomorphic cryptosystem, otherwise $\frac{c_1 c_2}{c_3}$ wouldn't give you the encryption of $1$, isn't it? –  LRM Oct 24 '13 at 8:08
Using an essentially homomorphic cryptosystem makes the proofs simpler. (I use "essentially", since the above approach still works even if you make ElGamal non-homomorphic by adding a suitable Schnorr proof.) You can do something similar for an essentially non-homomorphic cryptosystem, but the proofs would be complicated, possibly even impractical. –  K.G. Oct 24 '13 at 8:40