TODO list

[cryslith]

Some things to work on in the near future:

• Encryption preconditions are syntactically burdensome. Try to have only 1 inductive?
• abstractions:
  • "Weaken" auth_safe to allow an eqwhp rewrite. Prove that these versions are just as useful as the old versions.
  • A helper function with interaction which outputs the set of old indices with respect to n, so that we can talk about terms being old wrt n. Prove:
    • The set of old indices is monotonic in n
    • Any index in (interaction n) is old wrt n
    • The indices generated by interaction at time (n + 1) are new wrt n
• Our formulation of public-key encryption has some confusion about nonces. Resolve this after getting a good idea of symmetric-key encryption down.
• n-step protocols to work on:
  • "kerberos" - trusted 3rd party which shares sym. keys with
    everyone; repeatedly negotiates a shared key between 2 people
    who use the shared key
  • build up towards TLS-like protocol:
    • "PGP" - regularly sign encryption keys; people check the
      signatures and send you messages
    • session keys (cf Hugo Krawczyk, SIGMA)
    • multiple clients
    • KEM/PKE/DH
    • auth/confidentiality/both
    • preshared keys (similar to ratcheting)
    • key derivation
  • ratcheting - each round, send a message and new encryption+mac keys
    • could even show ratcheting property
    • probably will have the most problems. not even really
      handled well by computational models
  • server which takes adv message, prepends with "adv said: ", signs;
    wts all messages begin with "adv said: "
    • more or less superseded by "PGP"
• compositionality of indist:
  if e, e' are independent from context C, then
  e ≈ e' -> C[e] ≈ C[e']
• prove no_nonce_reuse
  • x <> y -> whp $x != $y