ProVerif-ATP icon indicating copy to clipboard operation
ProVerif-ATP copied to clipboard

Published 20 hours ago • verified publisher icon darrenldl

ProVerif-ATP can not be built

Open zwkylkx opened this issue 1 year ago • 10 comments

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

zwkylkx avatar Jun 30 '23 04:06 zwkylkx

Which version of ocaml are you using?

darrenldl avatar Jul 01 '23 04:07 darrenldl

I am using ocaml version 4.13.1

zwkylkx avatar Jul 02 '23 03:07 zwkylkx

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

zwkylkx avatar Jul 02 '23 07:07 zwkylkx

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.

darrenldl avatar Jul 02 '23 10:07 darrenldl

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?

zwkylkx avatar Jul 03 '23 03:07 zwkylkx

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.

darrenldl avatar Jul 03 '23 04:07 darrenldl

OK sure Thank you very much for your help!

zwkylkx avatar Jul 03 '23 08:07 zwkylkx

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

Anhduchb01 avatar Jul 23 '23 04:07 Anhduchb01

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

ducdai12102001 avatar Aug 10 '23 06:08 ducdai12102001

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

ducdai12102001 avatar Aug 21 '23 13:08 ducdai12102001