Thank you very much. Reading ahoy! :)
On 07/26/2014 08:11 PM, GreyHat LispHacker wrote: > 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 > <mailto:langsec-discuss-requ...@mail.langsec.org>> wrote: > > Send langsec-discuss mailing list submissions to > langsec-discuss@mail.langsec.org > <mailto: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 > <mailto:langsec-discuss-requ...@mail.langsec.org> > > You can reach the person managing the list at > langsec-discuss-ow...@mail.langsec.org > <mailto: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 <mailto:systm...@gmail.com>> > To: langsec-discuss@mail.langsec.org > <mailto:langsec-discuss@mail.langsec.org> > Subject: Re: [langsec-discuss] Proving Code > Message-ID: <53d2a1c9.1030...@gmail.com > <mailto: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 > <mailto:travis%2bml-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 > <mailto: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 > <mailto: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
_______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
