[Verifpal] Major Revision to Verifpal Paper

Nadim Kobeissi nadim at symbolic.software
Fri May 1 17:15:36 CEST 2020


Hello everyone,

The Verifpal paper on ePrint has been majorly revised: https://eprint.iacr.org/2019/971

Changes:

	- The paper now has two co-authors: Georgio Nicolas and Mukesh Tiwari.
	- The paper showcases our complete formalization of the Verifpal semantics in Coq using the Verifpal Coq Library, and sketches out how we plan to use Coq to attest the soundness of Verifpal’s analysis methodology. 
	- We present the first-ever formal model of a COVID-19 tracing protocol in Verifpal by modeling and analyzing DP-3T.
	- Far better and more complete sections, most of them rewritten, for pretty much everything: introduction, related work, the languages, fundamental types in Verifpal, how primitives are defined, analysis logic, etc. etc. all the way to the conclusion. For sure Verifpal itself is much better formalized and explained.
	- Our contributions are more well-organized.

Feedback welcome,

Nadim Kobeissi
Symbolic Software • https://symbolic.software



More information about the Verifpal mailing list