8
$\begingroup$

I want a tool that (runs on Win7 and) can perform automated verification of a protocol in the eCK security model as described in Microsoft Research's paper "Stronger Security of Authenticated Key Exchange".

Does anyone know such a tool?

Improve this question
$\endgroup$
0

4 Answers 4

Reset to default
5
$\begingroup$

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 an example how to test if it works (which it will on Win7 - which you previously wrote you're using):

  1. create c:\cv\ and decompress the contents of the downloaded package in there.
  2. Open a command-line prompt and go to c:\cv\ where the cryptoverif.exe resides.
  3. Run cryptoverif.exe c:\cv\examples\fdh.cv

As for your question about TEX output, it would go like this:

cryptoverif.exe -tex somefilename.tex c:\cv\examples\fdh.cv

The manual, which is included in the download package, will provide you with the rest of the commandline parameters and a detailed description on how to use it.

Here's a screenshot of the --help parameter:

screenshot

EDIT

A bit late, but The Scyther Tool may come handy too.

Improve this answer
$\endgroup$
2
  • $\begingroup$ i'm afraid that you've made two mistakes. one is that the filename is cryptoverif1.16 , so when you decompress the downloaded package in c:\cv` then it will be that c:\cv\cryptoverif1.16\ as your step 2. Another is that "cryptoverif.exe c:\cv\examples\fdh.cv -tex somefilename.tex" should be cryptoverif.exe -tex somefilename.tex c:\cv\examples\fdh.cv, you put them in the wrong order. $\endgroup$
    – T.B
    Sep 8, 2013 at 9:09
  • 1
    $\begingroup$ @Alex If you decompress by creating a folder out of the filename, you indeed run into that problem. I spoke about decompressing the contents of the package in there... as in "put the contents of the compressed file into that dir. As for the rest, I've edited the answer and added some final info to get you going. Mind you, I'm not going to provide any tech-support beyond this to be sure this Q&A stays somewhat on-topic. In fact... for Crypto.SE, I've already provided a bit too much tech support. But I'm pretty sure you'll manage to work out the rest yourself from this point. $\endgroup$
    – e-sushi
    Sep 8, 2013 at 10:14
6
$\begingroup$

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, which does not give you a reduction to a known hard problem as in the real eCK model, Scyther and Tamarin have been used to analyze protocols like Naxos etc. in a symbolic version of the eCK model. So that includes revealing the randomness, revealing session keys of non-matching sessions, weak perfect forward secrecy, etc.

If the reduction to the computational hardness problem is your main goal, you could try to do a computational proof with CryptoVerif. Afaik, no one has used it for the eCK model and such (relatively) complex protocols yet.

Short summary of my opinion: if you want an automatic tool to

  • reduce to known hard computational problem, but care less about specific details of the eCK model: try CryptoVerif. (There's a good pointer to CryptoVerif references above.)

  • capture main aspects of eCK model, but care less about computational aspects: try Tamarin (or Scyther). Papers that discuss their use for eCK-like models are here and here, respectively.

Improve this answer
$\endgroup$
2
  • $\begingroup$ thanks for your answer. But what's the deference between "reduce to known hard computational problem" and eCK model? And given a key-exchange protocol, which method should i use? $\endgroup$
    – T.B
    Sep 16, 2013 at 23:46
  • $\begingroup$ Most security models for key exchange protocols, including eCK, are descendants of [Bellare Rogaway 1993][1]. The differences among these variants are subtle and AFAIK there is no agreement on which one you should use. This is still a topic of active research so don't expect a definite answer here. [1]: cseweb.ucsd.edu/~mihir/papers/eakd.pdf $\endgroup$
    – user4621
    Sep 16, 2013 at 23:56
4
$\begingroup$

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 you can model your protocol in their language. They integrate with multiple protocol verification back-ends and automatically analyze your protocol with all available back-ends. It's great stuff: give it a try.

You might also check out the ProVerif system. It is more sophisticated and flexible -- but also has a substantially steeper learning curve.

I'm not familiar with the eCK security model, so you'll have to investigate on your own whether these tools can be used for what you want.

(I have no relationship to either project, other than being a fan of their work and a happy user of their tools.)

Improve this answer
$\endgroup$
8
  • 1
    $\begingroup$ i have seen that web, it does't offer the eCK model $\endgroup$
    – T.B
    Sep 8, 2013 at 0:58
  • $\begingroup$ @Alex Some alternative analysis tools besides AVISPA (which is used for reachability and correspondence assertions) would be: KISS (for static equivalence), YAPA (for static equivalence), and CryptoVerif (for verification of security against polynomial time adversaries in the computational model). Yet, I'm not sure if any of them will reliably be able to completely verify NAXOS (the two-pass AKE protocol which is described in the paper you've linked to). $\endgroup$
    – e-sushi
    Sep 8, 2013 at 3:41
  • $\begingroup$ @e-sushi i've got the CryptoVerif but it seens that it doesn't work on my computer $\endgroup$
    – T.B
    Sep 8, 2013 at 4:03
  • $\begingroup$ @Alex, odds are it's a problem on your end. You shouldn't give up on it so quickly. If you're going to expect a tool for this sort of thing, you're going to have to be resourceful, to be prepared to do some non-trivial hacking, and to deal with research-quality code, not polished commercial offerings. If that sounds unappetizing, then I recommend you give up on your idea of finding tools for protocol verification, and hire a consultant who will do the cryptographic analysis for you. $\endgroup$
    – D.W.
    Sep 8, 2013 at 4:16
  • 1
    $\begingroup$ @Alex It works flawlessly on my Win7 system. Be sure to download your binary from prosecco.gforge.inria.fr/personal/bblanche/cryptoverif/… and then read the contained "READMEBIN" on details of intallation and usage. Quick hint: install it to "C:\cv\", open command prompt and go to "C:\cv\", and launch one of the examples by running "cryptoverif.exe c:\cv\examples\fdh.cv" from your command prompt. You'll see a message ending with the line "All queries proved." As said: reading the "READMEBIN", which is nothing else but a text file, will help you a lot… RTFM ;) $\endgroup$
    – e-sushi
    Sep 8, 2013 at 4:27
4
$\begingroup$

I could add to the list (in alphabetical order):

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ I don't know about the first one but the last two work in the symbolic model while the eCK model expresses computational security. $\endgroup$
    – Alexandre Yamajako
    Sep 9, 2013 at 11:58
  • $\begingroup$ Casper is similarly symbolic in that it's a security protocol modification / front end / new language that sits on top of CSP. $\endgroup$
    – Savara
    Aug 23, 2015 at 21:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.