FS2PV is a tool for analyzing implementation code of security protocols, written in F#, by translation into the pi-calculus format accepted by ProVerif.

FS2PV has been developed within the Samoa Project at Microsoft Research; the first applications have been to XML-based web services security protocols, but FS2PV should also be applicable to binary protocols.

FS2PV started as an intern project; the initial implementation was done by Stephen Tse during his internship in summer 2005.

Our first two papers describing the design and application of FS2PV are the following:

K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse. Verified interoperable implementations of security protocols. In 19th IEEE Computer Security Foundations Workshop (CSFW 2006), pages 139-152, Venice, July 5-7, 2006. IEEE Computer Society.

K. Bhargavan, C. Fournet, and A. D. Gordon. Verified reference implementations of WS-Security protocols. In 3rd International Workshop on Web Services and Formal Methods (WS-FM 2006), Vienna, September 8-9, 2006. Springer LNCS 4184:88-106.

Here is how to run FS2PV on the two examples in the release. The first example is called "pwdmac", a basic message authentication protocol described in our CSFW 2006 paper. The second example is the classic Otway-Rees key establishment protocol.

• Install cygwin, including make.
• Install F#. Our makefiles assume that the F# compiler, fsc.exe, is in your path.
• Download FS2PV from the MSR Downloads page, and extract to some directory.
• Download analyzer.exe from Bruno Blanchet's page at ENS. Copy analyzer.exe to the bin directory of the FS2PV release.
• Open a shell at examples/pwdmac, and run make.
• Similarly, open a shell at examples/otwayrees, and run make.

A central idea in our work is that we use the same source files for three separate tasks. First, we compile to generate a binary that runs the protocol, using concrete message formats over sockets. This is the binary that can be used in production or for interoperability testing with other implementations of the same protocol. Second, we compile to generate a symbolic implementation; this binary uses a symbolic format for messages, that is suitable for debugging the protocol. Third, we translate the source files down to ProVerif format, suitable for analysis. This translation uses the same symbolic message format as the symbolic implementation, but is for analysis rather than execution.

Here is the output from running make in examples/pwdmac.

fsc --define fs --define concrete -r System.Security.dll ../../lib/concrete-fs/ pi.fs ../../lib/interfaces/data.mli ../../lib/interfaces/db.mli ../../lib/interfaces/crypto.mli ../../lib/interfaces/xml.mli ../../lib/interfaces/net.mli ../../lib/concrete-fs/db.fs ../../lib/concrete-fs/data.fs ../../lib/concrete-fs/crypto.fs ../../lib/concrete-fs/xml.fs ../../lib/concrete-fs/net.fs pwdmac.mli pwdmac.ml -o pwdmac.exe [pwdmac.exe is a concrete implementation of the protocol.]

fsc --define fs ../../lib/interfaces/pi.mli ../../lib/symbolic/pi.ml ../../lib/interfaces/data.mli ../../lib/interfaces/db.mli ../../lib/interfaces/crypto.mli ../../lib/interfaces/xml.mli ../../lib/interfaces/net.mli ../../lib/symbolic/db.ml ../../lib/symbolic/data.ml ../../lib/symbolic/crypto.ml ../../lib/symbolic/xml.ml ../../lib/symbolic/net.ml pwdmac.mli pwdmac.ml -o pwdmac-a.exe [pwdmac-a.exe is a symbolic implementation of the protocol.]

../../bin/fs2pv.exe -maxopt -o pwdmac.pv -q pwdmac.query ../../lib/interfaces/data.mli ../../lib/interfaces/db.mli ../../lib/interfaces/crypto.mli ../../lib/interfaces/xml.mli ../../lib/interfaces/net.mli ../../lib/symbolic/db.ml ../../lib/symbolic/data.ml ../../lib/symbolic/crypto.ml ../../lib/symbolic/xml.ml ../../lib/symbolic/net.ml pwdmac.mli pwdmac.ml [pwdmac.pv is the pi-calculus representation of the protocol.]

../../bin/analyzer.exe -in pi pwdmac.pv > pwdmac.res; grep '^RESULT' pwdmac.res [pwdmac.res is the results of ProVerif's analysis of the protocol.]

RESULT ev:Ev(PwdmacAccept(text_264)) ==> ev:Ev(PwdmacSend(text_264)) is true. [This means that authentication works.]

RESULT not ev:Ev(PwdmacAccept(text_1015)) cannot be proved. [This means that (as intended) the event PwdmacAccept is reachable.]

RESULT not ev:Ev(PwdmacSend(text_1758)) cannot be proved. [Similarly, this means that (as intended) the event PwdmacSend is reachable.]

grep ^goal pwdmac.res > .tmp

../../bin/goal2gen.exe .tmp > pwdmac.html [pwdmac.html is a structured representation of the results from ProVerif.]

rm -f .tmp

This is our first external release of FS2PV. We'd be grateful to receive any feedback you may have.

[Update September 25, 2007]

A technical report, MSR-TR-2006-46, is now available, based on the material from the CSFW'06 and WSFM'06 papers, together with full proofs.