PaMoChSA v1.0

PaMoChSA v1.0 (Partial Model Checking Security Analyzer) is a software tool for automatically checking the correctness of cryptographic protocols (with a limited number of sessions). Its underlying theory extends the partial model checking techniques to a process algebra using cryptographic primitives.

Security-sensitive protocols commonly use cryptography to achieve some form of confidentiality and integrity for the data transmitted over open networks. The design of such protocols is very challenging; due to the nature of the data handled, there is the need to consider the presence of active intruders in the net, which are ready to interfere with the normal execution of the protocol to achieve some advantage for themselves. Intruders may intercept, fake and eaves-drop exchanged messages.

During these actions, they may learn new messages for attacking the protocol. In this scenario, it seems convenient to define the security properties as properties of open systems, where the undefined components may be used to denote the presence of such intruders whose behavior cannot be predicted a priori. Thus, assume that a violation of a security property may be expressed by a formula f. Then, PaMoChSA v1.0 may be used to check this kind of statements:

There exists an intruder  X  s.t.  S|X |= f            (1)

If the previous statement does not hold then the system S is correct against every possible intruder X.

To analyze statements as (1) we decide to suitably apply the partial model checking techniques: To check that S|X |= f is equivalent to check that X by itself satisfies a formula f_S depending on the behavior of S (briefly, S|X |= f iff X |= f_S.)

Finally, we need only to decide the satisfiability of the formula fS. The construction of the formula f_S and the checking of its satisfiability are performed “on the fly”, i.e. during the analysis of S.

The tool is written in the functional language ocaml (http://pauillac.inria.fr/ocaml/), with a graphical interface based on the package mlgtk (http://cristal.inria.ft/~cuoq/mlgtk.html). Our implementation runs on a Pentium III machine with Linux RedHat 6.2 operating system.

Currently, PaMoChSA 1.0 allows the following security properties to be checked:

• Secrecy: checks are made whether X is able to discover a particular message m, declared to be a secret between some processes in S;
  
• Entity Authentication: (based on correspondence actions) checks are made about the occurrences of certain control actions, which represent the status of agents in the protocol.
  

What you need to input:

• The protocol description, written in Crypto-CCS, basically a variant of Robin Milner’s CCS process algebra;
• The initial intruder knowledge;
  
• The predicate p on the intruder knowledge, which expresses the security property to be checked.
  

PaMoChSA 1.0 does not need the intruder specification as input and it makes no assumption on intruder’s behavior.

The tool gives as output the trace for a potential attack on the protocol, if such attack exists.

Several security protocols have been analyzed with PaMoChSA 1.0; some examples:

• Needham-Schroeder Public-Key Protocol
• Secure Socket Layer 3.0 Protocol
• ISO SC27 Protocol
• The enrollment procedure of a Certification Authority (based on the open source code OpenCA)
• The SCEP Protocol (Simple certificate Enrollment Protocol)

References:

•  F. Martinelli. Languages for description and analysis of authentication protocols. In Proceedings of 6th Italian Conference on Theoretical Computer Science, Prato, Italy. World Scientific Press. 1998. 
  
• D. Marchignoli, F. Martinelli. Automatic verification of cryptographic protocols through compositional analysis techniques. In Proceedings of the International Conference on Tools and Algorithms for the Analysis and the Construction of Systems (TACAS), volume 1579 of Lectures Notes in Computer Science, pages 148--163, 1999. 
  
• A. Giani, F. Martinelli, A. Vaccarelli. Analysis of the e nrollment procedure of a certification Authority. Tech. Rep. IAT-B4-2000-024, Dec. 2000. 
  
• A. Giani, F. Martinelli, M. Petrocchi, A. Vaccarelli. A case study with PaMoChSA: A tool for the automatic analysis of cryptographic protocols. In Proc. of SCI/ISAS2001. Orlando (U.S.), July 2001. 
  
• F. Martinelli. Analysis of security protocols as open systems. Accepted for publication on TCS.