Tag Info

Hot answers tagged

6

I hope I got your point and try to answer your question. Actually, if I understand you right, then what you call attack can also be seen as an adversary acting in a specific attack model. Therefore I briefly review the security models for digital signature schemes. Goal of an adversary: We start by discussing the goals of an adversary beginning with the ...


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 ...


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, ...


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

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

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.


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

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

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: ...


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