SPIN is a model checker: https://en.wikipedia.org/wiki/SPIN_model_checker
For more information on model checking generally, this is a good start: https://en.wikipedia.org/wiki/Model_checking FSA is a Finite State Automata. On Sat, Jul 26, 2014 at 8:00 AM, <langsec-discuss-requ...@mail.langsec.org> wrote: > Send langsec-discuss mailing list submissions to > langsec-discuss@mail.langsec.org > > To subscribe or unsubscribe via the World Wide Web, visit > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss > or, via email, send a message with subject or body 'help' to > langsec-discuss-requ...@mail.langsec.org > > You can reach the person managing the list at > langsec-discuss-ow...@mail.langsec.org > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of langsec-discuss digest..." > > > Today's Topics: > > 1. Re: Proving Code (Orion) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 25 Jul 2014 11:28:25 -0700 > From: Orion <systm...@gmail.com> > To: langsec-discuss@mail.langsec.org > Subject: Re: [langsec-discuss] Proving Code > Message-ID: <53d2a1c9.1030...@gmail.com> > Content-Type: text/plain; charset="iso-8859-1" > > For us mere mortal newbs. What is SPIN/murphi?And is FSA finite state > analysis? > > On 07/24/2014 06:10 PM, travis+ml-lang...@subspacefield.org wrote: > > +1 would much like to add a section on formal methods to my online book: > > > > http://www.subspacefield.org/security/security_concepts.html > > > > Have not updated in years, so does not reflect everything I've learned > > since becoming too busy to write. > > > > Lately been doing a lot of TLS research and summarizing (38 pages > > worth) and that is a hot mess of prehistoric complexity that is badly > > in need of an update. Back in the late 90s I was astounded they > > didn't even use SPIN/murphi or another FSA to verify the protocol, > > which bespeaks a gap in education between practicioners and academics > > which your doc could fill. Worth reading: > > > > > http://blog.cryptographyengineering.com/2012/09/on-provable-security-of-tls-part-1.html > > > http://blog.cryptographyengineering.com/2012/09/on-provable-security-of-tls-part-2.html > > > > > > _______________________________________________ > > langsec-discuss mailing list > > langsec-discuss@mail.langsec.org > > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss > > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: < > https://mail.langsec.org/pipermail/langsec-discuss/attachments/20140725/76b6016b/attachment-0001.html > > > > ------------------------------ > > _______________________________________________ > langsec-discuss mailing list > langsec-discuss@mail.langsec.org > https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss > > > End of langsec-discuss Digest, Vol 23, Issue 15 > *********************************************** >
_______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
