[774] in Kerberos_V5_Development
[gerard@alice.att.com: availability of protocol validation software]
daemon@ATHENA.MIT.EDU (John T Kohl)
Mon Jul 15 07:55:35 1991
Date: Mon, 15 Jul 91 07:54:58 -0400
From: jtkohl@decvax.dec.com (John T Kohl)
To: krbdev@MIT.EDU
Might this be useful for Kerberos V5?
From: gerard@alice.att.com (Gerard J. Holzmann)
Newsgroups: comp.protocols.misc
Subject: availability of protocol validation software
Keywords: protocol design, protocol validation, sources
Date: 14 Jul 91 17:26:55 GMT
Organization: AT&T Bell Laboratories, Murray Hill NJ
I've had a lot of requests to make the validation software that
is described in my book ``Design and Validation of Computer Protocols''
(Prentice Hall, 1991, ISBN 0-13-539925-4) available in electronic form.
I'm delighted that I can now announce that it is available.
It should run on any Unix (r) system, and it is claimed to be the
fastest known system to help find design errors in protocol designs.
There is some rudimentary documentation with the distribution, but you'll
probably want the book to use it for real. Contact me for non-educational
usage. There's a little extra licensing dance to be done in this case.
Here are the remaining details:
Electronic Distribution of the Protocol Validator SPIN
======================================================
The SPIN software described in ``Design and Validation of
Computer Protocols'' is available free of charge from the
netlib distribution system, for educational purposes.
To get instructions on how to retrieve the software via
email (and lots of other math-related goodies)
send the following email message on internet:
mail netlib@research.att.com
send index
.
the response from netlib is automated.
To get the actual software, you send the message:
mail netlib@research.att.com
send index from spin
send bundle1 from spin
send bundle2 from spin
send bundle3 from spin
.
but it is best to obtain up-to-date instructions
with the first message shown above.
If there are any problem obtaining, installing
or using the software, please let me know.
gerard holzmann
gerard@research.att.com
