Ricardo Corin, Sandro Etalle, Ari Saptawijaya

CoProVe is a tool for security protocol analysis using constraint solving approach.

CoProVe is an improvement of Constraint Solver, a security protocol analyzer developed by J. Millen and V. Shmatikov. With respect to its predecessor, CoProVe features (1) a significantly more efficient implementation, (2) a monotonic behavior, which also allows to detect flaws associated to partial runs and (3) a more expressive syntax, in which a principal may also perform explicit checks.

In this page you will find the link that provides an online demonstration of CoProVe. The code, written in Prolog, is also downloadable. To run this tool on your own system, you need a Prolog interpreter. In our online demonstration, we use XSB Prolog as the back-end engine.

Latest Release

• CoProVe, with guessing attacks [CMAE03].
  Online demonstration .
• CoProVe [CE02].
  Online demonstration .

References

• [CMAE03] R. Corin, S. Malladi, J. Alves-Foss and S. Etalle. "Guess what? Here is a new tool that finds some new guessing attacks (Extended Abstract)" , IFIP WG 1.7 and ACM SIGPLAN Workshop on Issues in the Theory of Security (WITS), R. Gorrieri and R. Lucchi (eds.) , published by Dipartamento di Scienze dell'Informazione Universita di Bologna, Italy, held in Warsaw, Poland, Apr. , 2003, pp. 62-71 PDF
• [CE02] R. Corin and S. Etalle. "An Improved Constraint-based system for the verification of security protocols" , 9th Int. Static Analysis Symp. (SAS), vol. LNCS 2477, M. V. Hermenegildo and G. Puebla (eds.) , published by Springer-Verlag, Berlin, held in Madrid, Spain, Sep. , 2002, pp. 326-341 PDF