http://www.cap-lore.com/CapTheory/Categories.html
There is an amusing meme that as one comes to understand category
theory, one becomes incapable of explaining it to others. Here is a
vague theory to explain such phenomena--a category of confusion.
Anecdote
Beware: "Category" below does not refer directly to category theory.
I use Keykos jargon here to keep myself honest. You do not need to
know the meanings of these technical terms for my pedagogical point.
I was explaining sensory keys to someone. A critical property of this
category of key is that the kernel can look at bits in a key and see
directly whether the key is 'sensory'. I knew this but my
correspondent did not. This was a difficult discovery. I realized
that what I claimed depended on this and I blurted something like
"But when I called it 'sensory' didn't you understand that the kernel
could just look and see?". My correspondent properly responded that
the adjective 'requestor's' as in 'requestor's key' was a key
category inaccessible to the kernel.
Ouch!
It flashed quickly into my head that there are categories of
categories. I was master of both yet unaware that there were
categories of categories. My manipulation of these meta categories
was reliable but entirely subconscious. My friends who helped invent
these ideas were presumably in the same boat as I. As such we were
unable to explain in plain English what was going on. In our
conversations with each other it was always contextually clear and
subconscious which sort of category we were dealing with. It was
effortless.
Just now I added "Kernel Category" to the glossary as one category of
key categories and marked each technical adjective that applies to a
key, whether it was a kernel category; about half were. I know
offhand about a dozen other such Keykos obscurities to be repaired.
---------------------------------------------------------------------
Most (all?) formal security arguments today assume some form of
computational physics which is in place by virtue of some body of
code, and certainly some body of hardware. This code is unnamed in
the formal theory. The meta theory may refer to it as the 'TCB'.
According to some it is insecure to rely on code outside the TCB. The
pejorative language is "relying on third parties", as if the TCB were
always provided by one of the first two parties. I think one could
cobble together a security proof for the Keykos factory but it would
be opaque for it would obscure the pattern that similar ideas are at
work at two different levels. This commonality makes the proof more
efficient for understanding.