Readme for cpsa-2.2.12

CPSA: A Crptographic Protocol Shapes Analyzer This program has been built and tested using the Glasgow Haskell Compiler (GHC), which is available for Linux, Macs, and Windows. If possible, install Haskell Platform from <http://haskell.org> or from an operating system specific source. If the Internet is available, install CPSA with: $ cabal install cpsa Find the documentation directory by typing "cpsa -h" in a command shell, and view index.html in a browser. INSTALLING FROM A TARBALL If Haskell Platform is not available, install GHC and its parallel library, and then follow one of these operating system specific instructions. For example, to install on older Debian-based systems, ones that have only GHC 6, try: $ sudo apt-get install ghc6 libghc6-parallel-dev QUICK START (Linux) : To build and install CPSA type: $ make $ make install : To analyze a protocol you have put in prob.scm type: $ cpsa -o prob.txt prob.scm $ cpsagraph -o prob.xhtml prob.txt $ firefox -remote "openFile(`pwd`/prob.xhtml)" : Documentation and samples are in the directory given by $ cpsa -h : To view the user guide: $ firefox -remote "openFile($HOME/share/cpsa-X.Y.Z/doc/cpsauser.html)" : where X.Y.Z is the CPSA version number. QUICK START (Mac) : To build and install CPSA type: $ make $ make install : To analyze a protocol you have put in prob.scm type: $ cpsa -o prob.txt prob.scm $ cpsagraph -o prob.xhtml prob.txt $ open prob.xhtml : Documentation and samples are in the directory given by $ cpsa -h : To view the user guide: $ open $HOME/share/cpsa-X.Y.Z/doc/cpsauser.html : where X.Y.Z is the CPSA version number. QUICK START (Windows) The software has been tested on a Windows system on which neither MinGW or Cygwin has been installed. Install GHC and then from a command prompt type: C:\...> runghc Setup.hs configure C:\...> runghc Setup.hs build C:\...> runghc Setup.hs install If you do not have administrator privileges, configure with: C:\...> runghc Setup.hs configure --user Documentation and samples are in the directory given by C:\...> cpsa -h The installed programs can be run from the command prompt or via a batch file. Alternatively, copy doc/Make.hs into the directory containing your CPSA problem statements, and load it into a Haskell interpreter. Read the source for usage instructions. MAKEFILE The file $HOME/share/cpsa-X.Y.Z/doc/cpsa.mk contains useful GNU Make rules for inclusion, where X.Y.Z is CPSA version number. Alternatively, copy the file Make.hs in the same directory into the directory containing your CPSA problem statements. The source file has usage instructions. PARALLELISM CPSA is built so it can make use of multiple processors. To make use of more than one processor, start CPSA with a runtime flag that specifies the number of processors to be used, such as "+RTS -N4 -RTS". The GHC documentation describes the -N option in detail. DOCUMENTATION The starting point for CPSA documentation doc/index.html. Most users should read it and skip the rest of this section. To build the documentation, the file supp-pdf.tex must be installed. It is part of the TexLive texmf ConTeXt package. On Linux, the name of the package is context or texlive-context. The design document and the specification document require the xy-pic package, which is included in texlive-pictures. The documentation includes a user guide as an XHTML document, and three LaTeX documents. The CPSA Primer provides the background required to make effective use of the CPSA tool collection. For those interested in the implementation, The CPSA Theory contains a high-level description of the algorithm and the current state of the effort to show that when program terminates, it produces a description of every possible execution of the protocol consistent with the initial point-of-view skeleton. The CPSA Specification formally describes the implemented algorithm as a term reduction system. The CPSA Design describes implementation details and assumes The CPSA Specification has been read. The CPSA Design should be read if one is interested in reading the Haskell source for the tool collection. TEST SUITE : To run the test suite type: $ ./cpsatst Tests with the .scm extension are expected to complete without error, tests with the .lsp extension are expected to fail, and tests with the .lisp extension are not run. New users should read tst/README, and then browse the files it suggests while reading CPSA documentation. Don't develop your protocols in the tst directory. The Makefile is optimized for testing the cpsa program, not analyzing protocols. ADDITIONAL PROGRAMS The src directory of the source distributions includes programs written in Scheme, Prolog, and Elisp for performing tasks. Use them as templates for your special purpose CPSA analysis and transformation needs. Also, when given the --json option, the CPSA pretty printer cpsapp will transform CPSA S-expressions into JavaScript Object Notation (JSON). On Linux, the GHC runtime can request so much memory that thrashing results. The script in src/ghcmemlimit sets an environment variable that limits memory to the amount of free and reclaimable memory on your machine. WEB CPSA To make CPSA service available: (1) Install the four programs into the CGI bin directory. (2) Change directory to the src directory, and copy cpsacgi and cpsacgi.py into the CGI bin directory. (3) Copy index.html, ../doc/cpsauser.html, and ../doc/cpsaprimer.pdf into your choice of the web document directory. (4) Make an examples directory in the web document directory. (5) Copy ../tst/*.scm into the examples directory. SELINUX You must modify the default policy to allow unconfined executables to make their heap memory executable, has CPSA is written in Haskell, and its runtime puts executable code in its heap. The policy module is in src/httpd_allow_execmem.te. KNOWN BUGS Variable separation in generalization fails to separate variables in terms of the form (ltk a a).