[zeromq-dev] Using GSL to design an FSM protocol and translate it into a CSP protocol

[alex.]

First of all I wasn't really sure if it's okay to talk about the GSL
Universal Code Generator on this list, but I am writing anyway since it
didn't have its own mailing list. So forgive any insolence. :)


I was planning on writing my thesis about a traffic analysis resistant
multi-user file-transfer protocol and sure enough I wanted to do the
proof-of-concept implementation using ZeroMQ (so, yeah, expect to hear
more from me over the next months ;) ). Now I haven't ever written a
protocol myself but from the (little) research I did, I came to the
conclusion that it would be best to formalize it as best as possible, in
particular preventing any indeterminism. So the first idea was to use
finite state machines for formalization and for some reason the best
tool I could find for writing finite state machines that also lets me
write test cases AND generate all kinds of code (including graphics and
C-bindings) was made by the same people who created ZeroMQ. What about
that, I thought to myself.

Anyway after doing a little more research some papers indicated that a
better approach for writing communication protocols would be
communicating sequential processes (CSP). But they are somewhat of an
antithesis to FSMs: their basic elements are processes whereas in FSMs
the basic elements are states. Now I could brush CSPs aside and just go
for FSMs, but since my thesis is mostly security/cryptography related, I
also looked for security protocol analysers and every tool I could find
was using CSPs as well. In particular I found Casper[1], which uses a
special kind of CSP syntax to generate formalized CSP to be then checked
with FDR3[2].

In short, the scenario I would love to go for is basically:
- writing FSM in iMatix' GSL syntax,
- compile it to Casper's CSP syntax,
- compile that to general CSP to be checked by FDR3.


My question to this fine community is thus: Did anyone ever try to
produce a CSP using the GSL Universal Code Generator? Is something like
that even achievable (without wasting large amounts of precious time)
using GSL?
Or in general, did anyone ever try to translate FSMs into CSPs? Or am I
just too uninformed to know that something like this is simply absurd?

All the best,
alex.