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

[Pieter Hintjens]

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