# Tag Info

16

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 lets make sure we talk about the same concepts: Formal Verification: The act of proving the correctness of ...

10

The usual approach to prove IND-CPA security is to construct a logical argumentation called "reduction". In this argumentation you first start with the assumption that certain computational problem is hard (for example, the Decisional Diffie-Hellman assumption), and then you proceed to demonstrate that if your crypto scheme were insecure with respect to IND-...

10

The answer to this question is not straightforward and has a lot to do with the "conference culture" of computer science. Unlike other fields, the main publication venues for CS are conferences and not journals. This isn't to say that journals don't have an important role; rather, you don't follow journals to see what research is being done - you follow ...

9

This is very confusing because it seems as it should be something really easy to prove. However, it actually is not, and in fact the proof uses the Borel-Cantelli lemma. Anyway, it was formally proven by Rudich and Impagliazzo in their groundbreaking work on black-box separations. You can find a formal proof in Rudich's thesis, Section 6.2, or in the paper ...

9

This is based on an averaging argument (which is also used in the proof of the Goldreich-Levin hardcore bit). First, I assume that when writing $Pr[A(x,y)=1] \geq \epsilon$, then the probability is taken over a random choice of both $x$ and $y$. Now, the claim is that there exists a subset of $x$ values of a large enough size'' so that for every $x$ in ...

8

Just looking for a Turing machine vs circuit is a bit misleading. The important distinction is uniform (complexity class BPP) vs non-uniform (complexity class P/poly) adversaries. You can characterize P/poly in terms of circuit families, but also in terms of Turing machines with arbitrary "advice strings." In fact, the latter is the more traditional ...

7

I have written a tutorial on how to write simulation-based proofs. I think that it should be helpful.

7

Let me try to answer your second question, and hopefully shed some light on the first one in doing so. When we encrypt a message, it's because we want to keep something about that message secret. But what is it that we actually want to protect? Let's say the message we're encrypting is AGENT DOE REPORTS 23 UNITS ON BOARD SHIP TO BASE ALPHA, DEPARTED ON ...

7

I think @CortAmmon hit the nail on the head: cryptographic structures (hashes, ciphers, etc) are specifically designed to be hard for bad guys to analyse / reverse / find patterns in. It should come as no surprise that this is a double-edged sword: they are also hard for good guys to analyse in the form of mathematical proofs. As @CortAmmon said: ...

6

This is in principle similar as how "normal" cryptosystems are proven. With some algorithms we can reduce them to some "hard problem", but we do not know that those problems are actually hard to solve. Only that we cannot solve them efficiently. For example, the Diffie-Hellman problem is not even known to be NP-hard, never mind the whole issue of P vs. NP. ...

6

As the other answers already state here, game-based definitions are easier to write proofs for, but simulation-based definitions are often clearer in terms of the security guarantee that you get. The best example of this is IND-CPA (game-based definition) versus semantic security (simulation-based definition). Note that IND-CPA is really not a convincing ...

5

Informally, CCA2 does not permit any kind of modification of ciphertexts, while RCCA permits some alteration as long as it does not alter the original message. For example, think of a publicly randomizable encryption scheme, that is, a scheme that permits to alter the original randomness used during encryption. CCA2 would consider these ciphertexts as ...

5

What does this mean, exactly? The purpose of the environment is to model "everything else happening in the universe" besides the protocol execution. In the UC model, the adversary is allowed to talk to the environment during the execution of the protocol. So UC security means "security no matter what else is going on in the world, even if other things are ...

5

The first remark is that the cryptosystems are used with independent keys. This is important, otherwise it is usually very hard to prove anything. The simple solution Now, the simple solution is, as is mentioned in the comment and the linked question, is to secret-share your message into two shares and encrypt each share separately. The final ciphertext ...

5

In the vast majority of cases, the simulator sets the random tape of the adversary simply because it has to (by the definition). So, the simulator sets it in the beginning to be uniform, and this is then ignored from then on. There is one cases that I know of that this is actually really important, and this is non-black-box zero knowledge. Specifically, in ...

5

1) In the selective unforgeability game (often also denoted universal unforgeability), the adversary is given the public key and a target message for which it needs to produce a forgery (instead of giving the adversary only the public key and letting the adversary choose the target message). 2) No, any scheme that is EUF-CMA is also SUF-CMA (this is easy ...

5

There is actually a field of study regarding provably secure block ciphers. The seminal paper was "How to construct pseudorandom permutations from pseudorandom functions" (1988) by Luby and Rackoff. Their paper used pseudorandom round functions in a Feistel construction, and proved that 4 rounds were sufficient to make the resulting block cipher a ...

5

In order for information-theoretic security to imply computational security, you need to require that the simulator run in time that is polynomial in the running time of the real adversary. This is the standard definition, specifically to avoid protocols such as you presented in your question. So, the answer is: If you allow the simulator to be unbounded ...

5

If $H(X)$ and $H(Y)$ were not evaluated as a part of selecting $X$ and $Y$, then yes; the assumption of a random Oracle is that $H(Z)$ is an independent and uniformly distributed variable for every new (not previously submitted to the Oracle) value $Z$. If this isn't the case, then this need not hold. One obvious counterexample is: $X := 1; Y := 2 \textit{... 4 There is quite a bit of confusion in your question. First, differentiate between the real and ideal models. The adversary in the ideal model sends the adversary's input and gets its output (and can also sometimes determine if the honest party gets output, depending on the model). We often call the ideal adversary a "simulator" since this is how we build the ... 4 The point why a simulation must not deviate too much from the real game is due to the following reasoning. You assume you have an adversary that wins the original game, but you do not know how the adversary acts if you deviate from the behaviour of the real game and the adversary can notice this. Exactly because you make no assumption whatsoever about the ... 4 Realizes vs Implements Given the context of the cited papers, they mean the same thing. That said, I would prefer realizes. Implements has a connotation of a source code implementation. There could be implementation flaws (buffer overflow, etc) that impact security. The protocol design is secure, but the implementation is not. That, to me, is the primary ... 4 This is very strange, and somewhat suspect. The abort here is one that prevents the client from getting output. However, the real-world adversary may behave in a way that the client does get output. I suggest writing to the authors to ask and/or going through this very carefully. Without having gone through the details at all, my initial guess is that this ... 4 Ricky already gave the answer, but here are some additional details. "Entropy smoothing" hash functions are randomness extractors. Extractors are functions that extract almost uniform bits from weak sources of entropy. In a way, they spread the min-entropy of the input source almost evenly over the (shorter) extracted source, hence the smoothing. The ... 4 Why don't we have any, say, public-private key system that is NP complete to break?$\mathbf{NP}$-completeness is not the appropriate framework to think about the "security" of an encryption scheme, both in theory and in practice. Remember that the complexity classes$\mathbf{P}$,$\mathbf{NP}$, et al. are classes of decision problems, which are basically ... 4 In symmetric cryptography it is hard to prove security properties on algorithm. Most of block ciphers relies on showing resistances to the current attacks (cf the paper you linked or any paper that introduce a new block cipher). As nobody can know what will be the next attack vector, it is not possible to be prepared against it. From The design of Rijndael (... 4 There exists a distinguisher that works with nontrivial advantage,$O(1/\log \phi(m))$. This is because$q_0$must be a multiple of$p_0$; however$q_1$is a random value between$0$and$\phi(m)-1$. Hence, the distinguisher is "test both for primality, if one is prime, say that one is$r \cdot p_1 \bmod \phi(m)$"$q_1$is a random value, and hence it ... 4 (I assume you are asking about this paper based on your previous questions.) They do not prove BDDH in their security proofs. Assume that an attacker$A$breaks IND-sMID-CPA of the above scheme with probability greater than$\epsilon$within time$t$[...]. We show that using$A$, one can construct an attacker$B\$ for solving the BDDH problem. In ...

3

Detection of malicious behavior can happen anywhere. However, it is not true that you can run semi-honest protocols and then check later. This is because such protocols can reveal the honest party's input when interacting with a malicious adversary. In such as case, even if you detect the cheating, security is not achieved. Thus, you need to make sure that ...

3

Since the keys are fixed from beginning (the sub-protocols input are ciphertexts), isn't it possible to give the secret key to the (non-uniform) distinguisher as an extra advice (the only restrictions for the advice is that its bitlength is polynomial in the security parameter), and thus allowing the distinguisher to decrypt? This is up to your security ...

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