Main page

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 fS depending on the behavior of S (briefly, S|X |= f iff X |= fS.)

Finally, we need only to decide the satisfiability of the formula fS. The construction of the formula fS 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 (, 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:

What you need to input:

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: