# Tag Info

7

I hope I got your point and try to answer your question. Actually, if I understand you right, then what you call an attack actually means an adversary acting in a specific attack model. To clarify this, we need to review the security models for digital signature schemes and when we have discussed this we can clarify issues. Basically, we have to discuss ...

5

None of the above answers seem to take into account that you apparently want to establish security with respect to the eCK model; the above answers are mostly about tools that verify some (related but different) properties. Afaik, there is current no automatic tool that can give you analysis with respect to the exact eCK model. In the symbolic setting, ...

5

Just wrapping my comment into an answer as it seems to be what you're looking for… CryptoVerif can be used for verification of security against polynomial time adversaries in the computational model. It's available via http://prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/cryptoverifbin.html Related to your "it doesn't work on my computer", here's ...

4

The equation $t'=t+n\cdot t_c$ is an estimation to put an upper limit on $t'$. It might be possible that an attacker $A'$ can use a different, more efficient algorithm. But since the attack will work with using $A$, there exists an attacker $A'$ with at most $t'$. This means it's actually not an equation, but an inequality $t' \leq t + n \cdot t_c$. And then ...

4

As the previous answer says, they are certainly NOT the same. However, there is certainly a connection between them. Specifically, the covert model just says that there is a deterrent parameter $\epsilon$ and the guarantee is that if the adversary tries to cheat then it will be caught with probability at least $\epsilon$. The question that arises is how ...

4

Advantage and success probability are just words. Their meaning is in practice decided by how the speakers of the language use the words. You have observed that people use the terms advantage and probability in this way. One could probably argue that this is confusing or illogical or something like that, but such is language. About dividing by two: ...

4

I can highly recommend AVISPA, a tool for automated verification of cryptographic protocols. It is available as a web service, so you can upload a description of your protocol to their web server and it will give you a security analysis of it. They have detailed documentation of how to use their system and of their specification language for protocols, so ...

3

I could add to the list (in alphabetical order): Casper (http://www.cs.ox.ac.uk/gavin.lowe/Security/Casper/) Proverif (proverif.di.ens.fr/index.php) Scyther (http://people.inf.ethz.ch/cremersc/scyther/)

3

I believe what you are describing is somewhat orthogonal to typical MPC adversary models. Typically in MPC we let the adversary know all information that corrupt parties know (so if a corrupt party learns the output, the adversary is allowed to learn the output). What we care about in MPC protocols is that the adversary is not able to learn any additional ...

3

Memory of the first round can't help the attacker win the second round. If it could: the attacker could simulate the first round on his own (picking his own key, pretending to play the game against himself), and then play the second round against the challenger. So, adversaries like this are not stronger -- not even if they have memory.

2

The traditional MPC definition of correctness has no notion of correctness on the inputs. The traditional MPC correctness property deals with the output, i.e., the protocol is correct if $y$ where $y=f(x_1,x_2,\dots,x_n)$ is guaranteed to be output. What the $x_1,\dots,x_n$ values are is completely up to the inputting party. So, if you want to check that ...

2

If the honest parties have commitments to the malicious parties' inputs or [encapsulations generated by honest parties] of those inputs, then the function can be modified to check those. ​ Otherwise, the value computed by the trusted party "taking honest party inputs and modified inputs of corrupted parties" by definition results in a correct output.

2

No they are different. A covert adversary is essentially just a relaxation of a regular malicious adversary. Rational cryptography, on other the hand, is a different way of analyzing a cryptographic scheme using game theory. Here the parties of a protocol are seen as rational in a game theoretic sense acting according to some utility. I am not very well ...

2

PFS, or perfect forward secrecy, is a desirable (in many cases) property for cryptographic protocols. It says that even if your long-term secret (or static key in the paper) is revealed at some point, messages sent in the past should still be kept secret. Right after that line you quote, they define their PFS game. I'll reword it here to make it more ...

1

You always need to have in mind that $A$ is a hypothetical algorithm, since our goal in the reduction is to contradict the existence of such an efficient $A$. Now to your concrete security framework: Here, you are not satisfied by the fact that a hypothetical poly-time $A$ implies a poly-time reduction $A'$, but your aim is that the reduction does not take ...

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