[langsec-discuss] Proving Code

Orion systmkor at gmail.com
Fri Jul 25 18:28:25 UTC 2014


For us mere mortal newbs. What is SPIN/murphi?And is FSA finite state
analysis?

On 07/24/2014 06:10 PM, travis+ml-langsec at 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 at 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.html>


More information about the langsec-discuss mailing list