[langsec-discuss] langsec modeling for crypto protocols

travis+ml-langsec at subspacefield.org travis+ml-langsec at subspacefield.org
Mon Nov 4 03:05:42 UTC 2013

On Mon, Nov 04, 2013 at 09:08:57AM +0530, Sashank Dara wrote:
> Interestingly this thesis models the security protocols in terms of
> automata .
> "Foundations of Security Protocol Analysis"
> http://www.imsc.res.in/xmlui/handle/123456789/105
> Their key results being "the secrecy problem, whether a protocol leaks
> secrets or not is Undecidable ! ". This could be dangerous in practice.
> They prove that only few sub class of protocols are decidable .

Wow, very cool.  Reminds me of this:


Back in 1995 I recall seeing a paper from the same department on
implementation of network protocols using finite state automata.  The
basic idea is relevant in that your network protocol is "parsed" by
something, and in this case the idea was (for security) to convert to
events which drive a FSA - because that part is well-understood, the
idea was that it would be safer.  I guess the piece which converted
network input into state changes for the FSA would be rougly
equivalent to a lexer/tokenizer.

I was routinely astounded by the number of vulnerabilities in protocol
dissectors, often used for security... this can bridge air gapped
networks, if you record packet captures and analyze them in a "secure"
network.  So, to summarize, network protocols are languages too :-)

Which reminds me of all the finite-state analysis stuff from the late
90s.  I guess some people are still doing it:

Becoming good at war often involves becoming bad at peace.
-- PopSci article on PTSD

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 834 bytes
Desc: not available
URL: <https://mail.langsec.org/pipermail/langsec-discuss/attachments/20131103/ccd015ef/attachment.pgp>

More information about the langsec-discuss mailing list