Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ProVerif-ATP can not be built #12

Open
zwkylkx opened this issue Jun 30, 2023 · 10 comments
Open

ProVerif-ATP can not be built #12

zwkylkx opened this issue Jun 30, 2023 · 10 comments

Comments

@zwkylkx
Copy link

zwkylkx commented Jun 30, 2023

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
Copy link
Owner

Which version of ocaml are you using?

@zwkylkx
Copy link
Author

zwkylkx commented Jul 2, 2023

I am using ocaml version 4.13.1

@zwkylkx
Copy link
Author

zwkylkx commented Jul 2, 2023

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

@darrenldl
Copy link
Owner

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
Copy link
Author

zwkylkx commented Jul 3, 2023

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
Copy link
Owner

darrenldl commented Jul 3, 2023

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
Copy link
Author

zwkylkx commented Jul 3, 2023

OK sure
Thank you very much for your help!

@Anhduchb01
Copy link

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

@ducdai12102001
Copy link

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

@ducdai12102001
Copy link

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

4 participants