You can jump straight to the paper here but the main page also has git instructions for reproduction.
Congratulations on the formal proof and otherwise solid work. You’re almost at EAL7 with I think only one other VPN being designed as strong. Navy cancelled it, though, right before evaluation. Just add covert-channel analysis and source to object code verification to top it off. Then you’ll be Number 1 far as the implementation.
EDIT: Also, we have a formal methods tag now to highlight these posts.
I guess getting the big vendors like e.g. Cisco, Check Point and Fortinet to support it will be the hardest part.
It would be idea but don’t get your hopes up: big vendors usually want to use stuff like this for free or create crappy knock-offs. High-assurance security gets little love from either proprietary or FOSS sectors. It’s almost always CompSci people/companies, defense contractors, smartcard companies, or an occasional private company/person trying to create something better w/ security as differentiator. When they do, it’s uncommon for it to be FOSS (outside CompSci) since high-assurance software takes a lot of labor. They usually want something in return.
This problem led in the 1990’s to the concept of “incremental” assurance. You create a solution for the clients the fast, market-grabbing, money-making way. Make sure it’s decomposable w/ decent API or whatever to facilitate rewrites. Part of the money you make on your main product/service can be put into redoing critical parts of the software with high-assurance security. Although little data to test that, a co-founder of INFOSEC, Paul Karger, used it in his last project at IBM to fund a high-assurance, smartcard OS (Caernarvon). Broke up long-term project into intermediate deliverables IBM could sell independently and/or at least see something produced to justify funding.
I’m not a security expert, but it’s awesome to see new (from what I read) viable alternative to VPN protocols.