[cap-talk] Forgeable capabilities

[David Wagner]

Toby Murray writes:
>S(t) = getAuthority?login?password ->
>  if login == X and password == Y then
>     return!t -> S(t)
>  else
>     return!null -> S(t)
>
>Alice(login,password) = getAuthority.login.password -> return?cap ->
>Alice(login,password)
>
>
>Now if we instantiate Alice as Alice(X,Y) and then check whether Alice
>can ever acquire t (using a safety analysis check) then we'd find she
>could.
>
>If we instantiate Alice otherwise (i.e. she doesn't know X and Y) she
>won't be able to acquire such permissions.

Well, that sounds unconvincing.  My reaction would be to suspect that
the model must be making unfounded assumptions if it comes to those
conclusions starting only from that information.  For instance, it
sounds like the model must be assuming that if Alice isn't instantiated
with the password then she cannot guess it and cannot learn it (e.g.,
from someone else who knows it); but that's not necessarily a reasonable
assumption.  Reasoning about knowledge is easy if you don't insist on
soundness.  The hard part is reasoning about knowledge in a sound way,
especially given the possibility of guessing, covert channels, timing
side-channels, leaks due to garbage collection and other oddities, and
so on.  Real systems have many features that pose a tremendous challenge
for sound reasoning about knowledge.