[Haskell-cafe] ANN: CPSA - Cryptographic Protocol Shapes Analyzer

[John D. Ramsdell]

>> We are working towards a version of CPSA with the property that
>> whenever it successfully terminates, every possible execution is
>> described by its output.  However, the current implementation
>> occasionally fails to find some executions.
>
> That is concerning - is it due to ...

We have formally specified the algorithm, but we haven't been able to
prove the algorithm finds all solutions.  In fact, we now have an
example in the test suite that shows it misses an answer.  The example
is in the source distribution in tst/missing-contraction.scm.  There
should be two answers, but CPSA only finds one.  We have a fix you can
try out in 2.0.4.  In src/CPSA/Lib/Strand.hs, you can change the flag
useDisplacement from False to True, and CPSA will find both answers.
We don't know if this fix is all one needs to ensure CPSA finds every
answer.

By the way, the algorithm is in doc/cpsaspec.pdf, which can be build
from a source distribution of CPSA.

> What is the current status of development both wrt openness and future direction?

Our highest priority is to resolve the correctness issue you just
raised.  As for openness, the sources are available to you.  We
haven't thought about other forms of openness.

> I'm wondering if you plan to add MQV or other non-trivial primitives.

I don't know what MQV is, so I can't say.

Thanks for your interest, Thomas.

John