exactly, one service principal per (Coda realm, Kerberos realm) is
  sufficient, like coda/coda.realm_at_KRB.REALM as you say (note that the
  existing code forces one Coda realm - one Kerberos realm relation,
  while a Coda realm could otherwise use services of more than one
  independent Kerberos realms as well)

It would be really nice to write out the design and rules for
kerberos/coda interaction before the code.  Offhand, I would say that
it is reasonable to have more than one coda realm within a kerberos
realm, and that it is probably ok to require that all servers of each
coda realm are in the same krb realm.  But perhaps not.

So principals could be

coda/${coda-realm}@${KRB-REALM}

as you suggest.  (I made it a bit more explicit that the second 'coda'
is a variable, not a literal.

Or perhaps

auth2/${coda-realm}@${KRB-REALM}

for the user to talk to the auth2 server, rather than the coda servers
themselves.

But this raises another issue as to whether in the glorious future of
GSSAPI protected data traffic (rather than using krb5 to get auth2
tokens) the coda servers (rather than auth2 servers) have per-machine
principals.  That would make sense, from the principle of least
privilege, so that servers can't sniff traffic from other servers.
So in this case, we would use

coda/${fqdn-of-server}@${KRB-REALM}

for the service principal for a particular server.  The client would
then get tickets for servers as they need them.  This probably requires venus
to call a helper program as the user to request tickets, and then
install the resulting credentials into venus for use.


-- 
        Greg Troxel <gdt_at_ir.bbn.com>