Added Responder Authentication to Online Protocol

[cwaldm]

Added responder authentication property to the Online Protocol.
This can be used as a first example for introducing events. (It is very similar to the NSL example with only one event)

For events, we need the order

1. storing the new state
2. sending the message

That is the opposite order of what we previously had for the secrecy property of the Online protocol (compare to

dolev-yao-star-tutorial-code/examples/Online_with_secrecy/DY.OnlineS.Protocol.fst

Lines 44 to 58 in e175080

	val send_ping: principal -> principal -> state_id -> traceful (option (state_id & timestamp))
	let send_ping alice bob keys_sid =
	// TODO: explain high-level idea of "intended readers"
	let* n_a = gen_rand_labeled (nonce_label alice bob) in
	let ping = Ping {alice; n_a} in
	// encrypt the message for bob
	let*? ping_encrypted = pke_enc_for alice bob keys_sid key_tag ping in
	let* msg_ts = send_msg ping_encrypted in
	let ping_state = SentPing {bob; n_a} in
	let* sid = start_new_session alice ping_state in
	return (Some (sid, msg_ts))

Maybe we should swap this order already in the Online secrecy model (and the Two-Message protocol model)?

[cwaldm]

Closing this for now, since there are several version to add authentication and I first need to find out, which is the best.