KPF
 aa :            asym_algo
 A, B, S :       principal
 keypair^aa PK, SK (principal)
 A knows A, PK(A), SK(A), B, S, PK(S), aa
 S knows S, SK(S), PK, aa
 a, b, s : principal
 {
  1. A -> S : A, B
  2. S -> A : { PK(B), B }_SK(S)^aa
 }
 s. session A=a, B=b, S=s