search

darrenldl / ProVerif-ATP

ProVerif-ATP - Combining ProVerif and Automated Theorem Provers for Security Protocol Verification
23 stars 4 forks source link

ProVerif-ATP can not be built #12

Open zwkylkx opened 1 year ago

zwkylkx commented 1 year ago

How can I resolve it ? I have read the paper "Combining ProVerif and Automated Theorem Provers for Security Protocol Verification" and I would like to try the tool ProVerif-ATP . The file below is the error info while building ProVerif-ATP make failed.txt

darrenldl commented 1 year ago

Which version of ocaml are you using?

zwkylkx commented 1 year ago

I am using ocaml version 4.13.1

zwkylkx commented 1 year ago

I just tried Ocaml 4.07.1 compiler, it still doesn't work ProVerif-ATP make failed-4.07.1.txt

darrenldl commented 1 year ago

Sorry I'm busy with my new project which is part of my PhD thesis. What are you using ProVerif-ATP for? And how urgent do you need it working? It is likely I'll need to rewrite some parts of it.

zwkylkx commented 1 year ago

I am working on formal verification. I have try the XOR-ProVerif to resolve the xor in multi-factor authentication protocol, but I just always failed to build SWI-Prolog 5.6.14 which is required by XOR-ProVerif, and then I found your paper about ProVerif-ATP, I thought maybe ProVerif-ATP would work, so I download your source code and try to build it. It is not a very urgent thing, but it seems like there used to be a usable version used in the paper, so I would like to ask is source code of that version still avaliable?

darrenldl commented 1 year ago

It used to be buildable at the time, but I haven't updated this project for a few years, and in general I've moved off from proverif for now. I'll revisit this issue when I'm a bit more free.

Results from ProVerif-ATP might not be that useful as well, depending on what you are investigating of your multi-factor authentication protocol. Namely the translation from pi-calculus to FOL clauses lacks soundness argument for attacks found by an ATP, and the overall pipeline lacks algorithm for "attack reconstruction" (from ProVerif) to double check if an attack is a false attack or an actual attack.

Feel free to reach out to me at dilong.li AT anu.edu.au to discuss further.

zwkylkx commented 1 year ago

OK sure Thank you very much for your help!

Anhduchb01 commented 1 year ago

@zwkylkx I also received the same error. Did you have a solution for this problem?

ducdai12102001 commented 11 months ago

I also got this error. Is there a way to fix it?

ducdai12102001 commented 11 months ago

@darrenldl I got an error on the narato part, is there any way to fix it?