Prudent Engineering Practice
============================

* Abadi's principles

 A1. Every message should say what it means
 A2. Conditions for message acceptance should be clearly layed out
 A3. Mention principal's names in messages
 A4. Be clear about why encryption is done
 A5. Don't assume signer of encrypted message knows what it contains
 A6. Make sure to bind nonces to relevant other parts of a message
 A7. If attacker might be able to replay messages, use nonces, not counters
 A8. If timestamps are used for freshness, but securely bound clock skew
 A9. Don't assume a key is fresh because the message it encrypts is
A10. A message's encoding must be clear from message, not from context
A11. Know what trust relations the protocol depends on and why

* A few of my own principles to add to the list

D1. Use a MAC around any network message you encrypt
D2. Don't rely on long-lived keys for secrecy
D3. Don't assume synchronized clocks in your protocol


* Examples

** Denning Sacco

 A -> S:  A, B
 S -> A:  CA, CB
 A -> B:  CA, CB, {{Kab, Ta}_Ka^-1}_Kb

[B can re-encrypt {{Kab, Ta}_Ka^-1}_Kc and impersonate A to C.]

** Woo Lam

 A -> B:  A
 B -> A:  Nb
 A -> B:  {Nba}_Kas
 B -> S:  {{A, {Nba}_Kas}_Kbs
 S -> B:  {Nba}_Kbs

[Just initiate two concurrent connections, from A (impersonated) and C.
In second message send {Nba}_Kcs for both--instead of {Nba}_Kas for
one.]

** SSH

 A -> B:  Na
 B -> A:  Nb, KBh, KBs
 A -> B:  {{H(previous msgs), K}_KBs}_KBh
 A -> B:  {A, Ka, {H(A, Na, Nb,)}_Ka^-1}_K

 use K as session key

[B can connect to C with Na, use Nb=Nc, then gain access to C as A.]

** AKA

 A -> B:  Ka
 B -> A:  KBh, KBs
 A -> B:  {Na, A}_KBs
 B -> A:  {Nb}_Ka, {{Na}_KBh^-1}_Ka
 A -> B:  {H(Nb)}_KBs

 Use Na XOR Nb as session key

[C can pretend to be B.  Substitute KCs for KBs and Kc for Ka, and
play man-in-the-middle.]