[langsec-discuss] Will we ever "solve" security, or prove that we can't?
jon at callas.org
Thu Jan 19 03:09:25 UTC 2017
-----BEGIN PGP SIGNED MESSAGE-----
I have an informal proof that we can't.
Consider a security system S to be a tuple of formal language L and and set T, <L,T>. Also consider S to be "secure" if <L,T> is consistent, and "insecure" if it is not. (I will also observe that L and T are likely finite, but at most countable.) Also note that in this definition, a given system is isomorphic to a Model, which is also a tuple of a formal language and a set.
The Adversary gets to play a game in which they make elementary extensions of S by writing new symbols of their choosing into L giving L', and in some circumstances creating an extension set of T, T'. If they can produce a contradiction, they win. Note that this is equivalent to doing things like taking a lock that might be secure, but mounting it in a glass door, or finding yourself a saws-all to cut through the wall, or introducing side channels like power and timing analysis. The system is "truly secure" if there is no way for the adversary to create an extension with a contradiction. It is "situationally secure" if you can show that a given system or extension is consistent.
While there are certainly some S that are secure, there are many that are not and proving the general case is equivalent to proving that models are consistent and complete within their extensions.
It's a complete hand wave, but I think it's pretty obvious that you can get some situationally secure systems, but not in the general case.
-----BEGIN PGP SIGNATURE-----
Version: PGP Universal 3.3.0 (Build 9060)
-----END PGP SIGNATURE-----
More information about the langsec-discuss