Re: BoF session in Prague "Formal State Machines"

[Hannes Tschofenig <Hannes.Tschofenig at gmx.net>]

Hi Stephane,

I used formal languages for the verification of security protocols. I 
gave a presentation about the AVISPA project at IETF#59  (see 
http://www.tschofenig.com/avispa/).

I also applied them to some more recent protocols as well, including HIP and
http://www.tschofenig.com/svn/draft-vidya-mipshop-handover-keys-aaa/draft-vidya-mipshop-handover-keys-aaa-00.txt
(see Appendix E).

There are many nice things out there. The question is only: For whom is 
it helpful and how does it help them?

The above-mentioned formal method tool for verifying security protocols 
might help the protocol designers and people from a formal method 
community when reading IETF documents. The latter group is pretty small 
in size and regarding the former one I noticed that it only helps to the 
extend that they represent the protocol in a different way and could 
therefore discover some inconsistency in their document. The formal 
verification part is for most protocols useless since real problems are 
not discovered.

Here is my conclusion: it looks nice on paper but the tradeoff (effort 
to write compared to the value one gets) lead people to not use it.

So, coming back to the formal state machine language.

Have tried to apply your favorite language to a more complex, real-world 
protocol?
Have you been noticing real problems in the way how existing protocol 
specifications are written?
Why do you expect people to use it?
Have you spoken with implementers/protocol designers to determine 
whether you solve one of their problems?
Why do you think that the benefit is bigger than the effort?

In any case, I think that it is a useful thing to talk about this stuff 
and to give some guidance. It depends on how far you would like to go. 
If the idea is to give some guidance on how state machines could be 
described in IETF documents then that would be fine. If every working 
group suddenly has to write state machine documents using the developed 
language then some folks could get a bit nervous.

Ciao
Hannes

PS: My students have used  the following tools in past projects: the 
state machine compiler, available at http://smc.sourceforge.net, and for 
graphical representation they used 
http://www.research.att.com/sw/tools/graphviz/.

Stephane Bortzmeyer wrote:
> On Tue, Feb 06, 2007 at 10:09:09AM +0100,
>  Hannes Tschofenig <Hannes.Tschofenig at gmx.net> wrote
>  a message of 53 lines which said:
>
>> Why should I re-write my documents to comply to a more formal state
>> machine description?
>
> Figures (wether in ASCII-art, in Unicode-art, in SVG, in GIF or
> whatever) and informal tables are impossible to analyze automatically
> (for instance to check if they are deterministic, or to translate them
> automatically to software like Ragel). That's the main problem I have
> with informal descriptions: you cannot process them by software and
> you have to check them manually.
>
> Being parsable by a program is the main aim of the future language.


_______________________________________________
Cosmogol mailing list
Cosmogol at ietf.org
https://www1.ietf.org/mailman/listinfo/cosmogol