Forbid explicit_nonce reuse in inbound TLS records

[themighty1]

Currently in MPC-TLS we don't check if server used the same explicit_nonce more than once.

UPDATE: I realized that the attack described below is not possible since the prover will fail to verify the tag on a tampered TLS record.
However, I still think it is worth forbidding nonce reuse, especially if doing so simplifies the formal proof (there will be no need to account for such malicious behaviour in the proof).

This opens up a potential attack for a malicious verifier `V`. The attack is possible under these conditions:

• V learned previous TLS record's ciphertext with its explicit_nonce.

• that TLS record's ciphertext was an encryption of publicly-known data, which allowed V to learn the keystream by locally computing ciphertext XOR public data.

The essense of the attack is that V intercepts the prover's connection to the server and replaces a valid explicit_nonce of an inbound TLS record with explicit_nonce which V learned earlier.

This will result in the prover computing the wrong keystream and decrypting the ciphertext into a plaintext which the server did not send.

Under very contrived circumstances this may result in a selective failure on the prover's side, revealing some info about the prover's private data.

[themighty1]

since we are not planning to have a formally proven protocol, this issue is moot.