Module session 

Type-state secure-channel state machine.

Spec: Annex D.4

States are phantom-typed so that calling out-of-order is a compile error rather than a runtime fault. The intended sequence is:

Disconnected --challenge(RND.A)----> Challenged
Challenged   --recv_ccrypt(...)----> Cryptogrammed
Cryptogrammed--recv_rmac_i(...)----> Secure

Calls from any state may transition back to Disconnected on error.

Structs

Challenged

Phantom: ACU has sent CHLNG and is awaiting CCRYPT.

Cryptogrammed

Phantom: ACU has verified CCRYPT and is awaiting RMAC_I.

Disconnected

Phantom: session not started.

Secure

Phantom: SC fully established.

Session

Secure-channel session state.