Station-to-Station protocol questions Basic Station-to-Station protocol which authenticates Bob and Alice if they safely shared their long-term asymmetric public keys. 


Alice sends Bob her public key $A_K$
Bob receives $A_K$ and computes the shared secret key $K$
Bob signs with his long-term key $S_B(\mathit{B_K, A_K})$ and encrypts $E(S_B(B_K,A_K), K)$ using AES 128 GCM
Bob sends Alice $B_K, E(S_B(B_K,A_K), K)$
Alice computes $K$, decrypts $E(S_B(B_K,A_K), K)$ and verifies the sig. using Bob's long-term public key
Alice signs $S_A(\mathit{A_K, B_K})$, encrypts $E(S_A(A_K,B_K), K)$ and sends the resulted ciphertext
Bob decrypts $E(S_A(A_K,B_K), K)$ and verifies sig. $S_A(\mathit{A_K, B_K})$ using her long-term public key


I have three questions.


Before Bob computes $S_B(\mathit{B_K, A_K})$ does he hash $B_K$ and
$A_K$ using $SHA256$ for example so Alice can hash them herself and compare the hashes?
Does Bob use plain $K$ for encryption or does he use a key
derivation function like $HKDF$?
If Bob uses $HKDF$ can he include the salt at the end of the data he
sends to Alice?
1. Before Bob computes $S_B(\mathit{B_K, A_K})$ does he hash $B_K$ and
      $A_K$ using $SHA256$ for example so Alice can hash them herself and compare the hashes?


Generally the signature generation function already includes a hash operation (which might be SHA-256) so requiring a separate hashing step isn't required; it should be configured for the signature generation function.

You could use a separate hash if you don't want to involve the private key early in the protocol - but that's the only reason I can think of.


  2. Does Bob use plain $K$ for encryption or does he use a key
      derivation function like $HKDF$?


Depends.

Generally key agreement (which seems to be missing entirely from your protocol) will generate a shared secret. But this secret may not be well distributed and / or may be too large. So in that case a separate KDF is required. 

Note that sometimes a KDF is already configured within the key agreement protocol, so in that case a separate KDF is not required - just like with the hash function for the signature generation algorithm. Of course you could still use a separate KDF to derive more keys or keys with a different size if that's needed in your protocol.


  3. If Bob uses $HKDF$ can he include the salt at the end of the data he
      sends to Alice?


Sure, or the salt can be left out altogether. But HKDF does mention that adding a salt is preferred to achieve high amount of security.