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

[Kevin Sapper]

Also for defining protocols there is zproto (
https://github.com/zeromq/zproto) and to kick start your C project you
might check out zproject (https://github.com/zeromq/zproject). Both of them
are GSL tools so if they're not what your looking for the might help you as
an example for your on GSL project.

2016-04-14 11:37 GMT+02:00 Pieter Hintjens <ph at imatix.com>:

> I don't understand half of what you're asking :) But in any case do
> take a look at the tiny FSM / C code generator
> (
> https://github.com/imatix/gsl/blob/b0aa393a6d00df2859f21aab0ccf6f203e18db96/examples/fsm_c.gsl
> )
> that I've used happily in a few projects already.
>
> On Thu, Apr 14, 2016 at 11:30 AM, alex. <thissideup at riseup.net> wrote:
> > 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.
> > _______________________________________________
> > zeromq-dev mailing list
> > zeromq-dev at lists.zeromq.org
> > http://lists.zeromq.org/mailman/listinfo/zeromq-dev
> _______________________________________________
> zeromq-dev mailing list
> zeromq-dev at lists.zeromq.org
> http://lists.zeromq.org/mailman/listinfo/zeromq-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.zeromq.org/pipermail/zeromq-dev/attachments/20160414/3526c768/attachment.htm>