RE: protocol standards that use formal specification of behavior?

["P.H.Welch" <P.H.Welch@xxxxxxxxxx>]

Hi,

Sorry - I'm a bit late with my input ...

A classic review of the use of CSP in protocols ensuring security is
given by Steve Schneider in:

  "Verifying Security Protocols: an application of CSP", S. Schneider,
  in "Communicating Sequential Processes, The First 25 Years"
  http://www.springerlink.com/content/tapxhaw7vb211x6l/

I also remember a seminar two years ago at Kent from Rod Chapman of
Praxis Critical Systems Ltd.  He described designing secure protocols
in CSP before implementing them is SPARK Ada - a real commercial project
on smart cards.  You had better check with him though - my memory
may not be accurate!

Eric and Larry corresponded:;
> > Personnally I find CSP a bit too primitive to describe protocols as one
> > needs to expres everything in low level channel communication and at least
> > two processes. I am still looking for a tool or way that takes a whole
> > protocol (like expressed in a MSC) as a single interaction between
> > concurrent entities.
> >
> > Eric
> 
> If the channel ends pre-exist, wouldn't it be possible to express such a
> tool as a CPA (occam-like) procedure callable as a process in parallel,

For occam-pi, we have been thinking of introducing formal CONTRACTs,
attached to PROC headers and CHAN TYPE declarations.  The latter two
concepts merely give "pin" in/out shapes to a process interface.
A CONTRACT would specify how that interface must be used.  This could
be a trace specification or something a little stronger.  The trick
is to enable checks that the CONTRACT is honoured - both by the
implementation of the process and by the environment that uses it.
Whether this would be through an contract-checking extra process
(i.e. at run-time) or some CSP specification (at compile-time) is open.

These are not new ideas - there have been several papers on this theme
at CPA conferences.  For example:

  Marcel Boosten, "Formal Contracts: Enabling Component Composition"
  in "Proceedings CPA 2003"
  http://www.wotug.org/static/cpa2003_long.shtml

which (I think) won the best paper award that year.

Also, the Microsoft Singularity project defines something like this in:

  http://research.microsoft.com/~tharris/papers/2006-sysml.pdf

Their "contracts" are finite state machines defining channel useage.

(Let's hope we never end up with "prior art" disputes over their patenting
of the ideas ... as my BlueJ colleagues have encountered:

  Google: "BlueJ Microsoft patent"  :(

But ... just as I write the above, I've received a new email ... it seems
Microsoft have relented and, even, apologised:

  http://blogs.msdn.com/danielfe/archive/2007/01/28/update-response-to-bluej-patent-issues.aspx

So, all's well after all, :))

Thanks,

Peter.