(********************************************************************)
(*                                                                  *)
(*  tls.s7i       Support for Transport Layer Security (TLS/SSL).   *)
(*  Copyright (C) 2013 - 2019, 2021 - 2023  Thomas Mertes           *)
(*                                                                  *)
(*  This file is part of the Seed7 Runtime Library.                 *)
(*                                                                  *)
(*  The Seed7 Runtime Library is free software; you can             *)
(*  redistribute it and/or modify it under the terms of the GNU     *)
(*  Lesser General Public License as published by the Free Software *)
(*  Foundation; either version 2.1 of the License, or (at your      *)
(*  option) any later version.                                      *)
(*                                                                  *)
(*  The Seed7 Runtime Library is distributed in the hope that it    *)
(*  will be useful, but WITHOUT ANY WARRANTY; without even the      *)
(*  implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR *)
(*  PURPOSE.  See the GNU Lesser General Public License for more    *)
(*  details.                                                        *)
(*                                                                  *)
(*  You should have received a copy of the GNU Lesser General       *)
(*  Public License along with this program; if not, write to the    *)
(*  Free Software Foundation, Inc., 51 Franklin Street,             *)
(*  Fifth Floor, Boston, MA  02110-1301, USA.                       *)
(*                                                                  *)
(********************************************************************)


include "socket.s7i";
include "asn1.s7i";
include "x509cert.s7i";
include "hmac.s7i";
include "elliptic.s7i";
include "cipher.s7i";
include "arc4.s7i";
include "des.s7i";
include "tdes.s7i";
include "aes.s7i";
include "aes_gcm.s7i";


const type: cipherSuite is integer;

const cipherSuite: TLS_NULL_WITH_NULL_NULL                 is 16#0000;
const cipherSuite: TLS_RSA_WITH_RC4_128_MD5                is 16#0004;
const cipherSuite: TLS_RSA_WITH_RC4_128_SHA                is 16#0005;
const cipherSuite: TLS_RSA_WITH_DES_CBC_SHA                is 16#0009;
const cipherSuite: TLS_RSA_WITH_3DES_EDE_CBC_SHA           is 16#000a; # Mandatory TLS 1.1 Cipher
const cipherSuite: TLS_RSA_WITH_AES_128_CBC_SHA            is 16#002f; # Mandatory TLS 1.2 Cipher
const cipherSuite: TLS_RSA_WITH_AES_256_CBC_SHA            is 16#0035;
const cipherSuite: TLS_RSA_WITH_AES_128_CBC_SHA256         is 16#003c;
const cipherSuite: TLS_RSA_WITH_AES_256_CBC_SHA256         is 16#003d;
const cipherSuite: TLS_ECDHE_ECDSA_WITH_AES_128_CBC_SHA    is 16#c009;
const cipherSuite: TLS_ECDHE_ECDSA_WITH_AES_256_CBC_SHA    is 16#c00a;
const cipherSuite: TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA      is 16#c013;
const cipherSuite: TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256 is 16#c02b;
const cipherSuite: TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384 is 16#c02c;
const cipherSuite: TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256   is 16#c02f;
const cipherSuite: TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384   is 16#c030;

const array cipherSuite: supportedCiphers is [] (
    TLS_RSA_WITH_3DES_EDE_CBC_SHA,
    TLS_RSA_WITH_RC4_128_SHA,
    TLS_RSA_WITH_RC4_128_MD5,
    TLS_RSA_WITH_DES_CBC_SHA,
    TLS_RSA_WITH_AES_128_CBC_SHA,
    TLS_RSA_WITH_AES_256_CBC_SHA,
    TLS_RSA_WITH_AES_128_CBC_SHA256,
    TLS_RSA_WITH_AES_256_CBC_SHA256,
    TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA,
    TLS_ECDHE_ECDSA_WITH_AES_128_CBC_SHA,
    TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256,
    TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256
  );

const string: SSL_3_0 is "\3;\0;";
const string: TLS_1_0 is "\3;\1;";
const string: TLS_1_1 is "\3;\2;";
const string: TLS_1_2 is "\3;\3;";
const string: TLS_1_3 is "\3;\4;";

const type: keyExchangeAlgorithm is new enum
    RSA, EC_DIFFIE_HELLMAN
  end enum;

const type: tlsParameters is new struct
    var boolean:              isClient                 is TRUE;
    var string:               session_id               is "";
    var string:               hostName                 is "";
    var cipherSuite:          cipher_suite             is TLS_NULL_WITH_NULL_NULL;
    var keyExchangeAlgorithm: key_exchange_algorithm   is RSA;
    var cipherAlgorithm:      bulk_cipher_algorithm    is NO_CIPHER;
    var boolean:              block_cipher             is FALSE;
    var integer:              key_size                 is 0;
    var integer:              key_material_length      is 0;
    var integer:              block_size               is 0;
    var integer:              iv_size                  is 0;
    var boolean:              is_exportable            is FALSE;
    var digestAlgorithm:      mac_algorithm            is NO_DIGEST;
    var integer:              hash_size                is 0;
    var integer:              compression_algorithm    is 0;
    var string:               tls_version              is TLS_1_2;  # TLS_1_1;
    var string:               master_secret            is ""; # length: 48
    var string:               client_random            is ""; # length: 32
    var string:               server_random            is ""; # length: 32
    var certAndKey:           serverCertificates       is certAndKey.value;
    var certAndKey:           clientCertificates       is certAndKey.value;
    var rsaKey:               publicRsaCertificateKey  is rsaKey.value;
    var rsaKey:               privateRsaCertificateKey is rsaKey.value;
    var ecPoint:              publicEccCertificateKey  is ecPoint.value;
    var bigInteger:           privateEccCertificateKey is 0_;
    var ellipticCurve:        curve                    is ellipticCurve.value;
    var integer:              signatureScheme          is 0;
    var eccKeyPair:           ownEccKeyPair            is eccKeyPair.value;
    var ecPoint:              publicEccKeyOfServer     is ecPoint.value;
    var string:               readMacSecret            is "";
    var string:               writeMacSecret           is "";
    var cipherState:          readCipherState          is cipherState.value;
    var cipherState:          writeCipherState         is cipherState.value;
    var integer:              readSequenceNumber       is 0;
    var integer:              writeSequenceNumber      is 0;
    var boolean:              writeEncryptedRecords    is FALSE;
    var string:               handshake_messages       is "";
  end struct;

const char: NO_MESSAGE         is EOF;
const char: CHANGE_CIPHER_SPEC is '\20;';
const char: ALERT              is '\21;';
const char: HANDSHAKE          is '\22;';
const char: APPLICATION_DATA   is '\23;';

const char: CLIENT_HELLO        is '\1;';
const char: SERVER_HELLO        is '\2;';
const char: SESSION_TICKET      is '\4;';
const char: CERTIFICATE         is '\11;';
const char: SERVER_KEY_EXCHANGE is '\12;';
const char: CERTIFICATE_REQUEST is '\13;';
const char: SERVER_HELLO_DONE   is '\14;';
const char: CERTIFICATE_VERIFY  is '\15;';
const char: CLIENT_KEY_EXCHANGE is '\16;';
const char: FINISHED            is '\20;';

const char: CLOSE_NOTIFY        is '\0;';
const char: UNEXPECTED_MESSAGE  is '\10;';
const char: BAD_RECORD_MAC      is '\20;';
const char: DECRYPTION_FAILED   is '\21;';
const char: HANDSHAKE_FAILURE   is '\40;';
const char: BAD_CERTIFICATE     is '\42;';
const char: ILLEGAL_PARAMETER   is '\47;';
const char: PROCOCOL_VERSION    is '\70;';
const char: NO_RENEGOTIATION    is '\100;';

# Extensions:
const integer: SERVER_NAME                            is     0;  # RFC6066
const integer: MAX_FRAGMENT_LENGTH                    is     1;  # RFC6066
const integer: CLIENT_CERTIFICATE_URL                 is     2;  # RFC6066
const integer: TRUSTED_CA_KEYS                        is     3;  # RFC6066
const integer: TRUNCATED_HMAC                         is     4;  # RFC6066
const integer: STATUS_REQUEST                         is     5;  # RFC6066
const integer: USER_MAPPING                           is     6;  # RFC4681
const integer: CLIENT_AUTHZ                           is     7;  # RFC5878
const integer: SERVER_AUTHZ                           is     8;  # RFC5878
const integer: CERT_TYPE                              is     9;  # RFC6091
const integer: ELLIPTIC_CURVES                        is    10;  # RFC4492
const integer: EC_POINT_FORMATS                       is    11;  # RFC4492
const integer: SRP                                    is    12;  # RFC5054
const integer: SIGNATURE_ALGORITHMS                   is    13;  # RFC5246
const integer: USE_SRTP                               is    14;  # RFC5764
const integer: HEARTBEAT                              is    15;  # RFC6520
const integer: APPLICATION_LAYER_PROTOCOL_NEGOTIATION is    16;  # RFC7301
const integer: STATUS_REQUEST_V2                      is    17;  # RFC6961
const integer: SIGNED_CERTIFICATE_TIMESTAMP           is    18;  # RFC6962
const integer: CLIENT_CERTIFICATE_TYPE                is    19;  # RFC7250
const integer: SERVER_CERTIFICATE_TYPE                is    20;  # RFC7250
const integer: PADDING                                is    21;  # RFC7685
const integer: ENCRYPT_THEN_MAC                       is    22;  # RFC7366
const integer: EXTENDED_MASTER_SECRET                 is    23;  # RFC7627
const integer: TOKEN_BINDING                          is    24;  # RFC8472
const integer: CACHED_INFO                            is    25;  # RFC7924
const integer: TLS_LTS                                is    26;
const integer: COMPRESS_CERTIFICATE                   is    27;  # RFC8879
const integer: RECORD_SIZE_LIMIT                      is    28;  # RFC8449
const integer: PWD_PROTECT                            is    29;  # RFC8492
const integer: PWD_CLEAR                              is    30;  # RFC8492
const integer: PASSWORD_SALT                          is    31;  # RFC8492
const integer: TICKET_PINNING                         is    32;  # RFC8672
const integer: TLS_CERT_WITH_EXTERN_PSK               is    33;  # RFC8773
const integer: DELEGATED_CREDENTIAL                   is    34;  # RFC9345
const integer: SESSION_TICKET_TLS                     is    35;  # RFC4507
const integer: PRE_SHARED_KEY                         is    41;  # RFC8446
const integer: EARLY_DATA                             is    42;  # RFC8446
const integer: SUPPORTED_VERSIONS                     is    43;  # RFC8446
const integer: COOKIE                                 is    44;  # RFC8446
const integer: PSK_KEY_EXCHANGE_MODES                 is    45;  # RFC8446
const integer: CERTIFICATE_AUTHORITIES                is    47;  # RFC8446
const integer: OID_FILTERS                            is    48;  # RFC8446
const integer: POST_HANDSHAKE_AUTH                    is    49;  # RFC8446
const integer: SIGNATURE_ALGORITHMS_CERT              is    50;  # RFC8446
const integer: KEY_SHARE                              is    51;  # RFC8446
const integer: TRANSPARENCY_INFO                      is    52;  # RFC9162
const integer: CONNECTION_ID_DEPRECATED               is    53;  # RFC9146
const integer: CONNECTION_ID                          is    54;  # RFC9146
const integer: EXTERNAL_ID_HASH                       is    55;  # RFC8844
const integer: EXTERNAL_SESSION_ID                    is    56;  # RFC8844
const integer: QUIC_TRANSPORT_PARAMETERS              is    57;  # RFC9001
const integer: TICKET_REQUEST                         is    58;  # RFC9149
const integer: DNSSEC_CHAIN                           is    59;  # RFC9102
const integer: NEXT_PROTOCOL_NEGOTIATION              is 13172;
const integer: ENCRYPTED_CLIENT_HELLO                 is 65037;
const integer: RENEGOTIATION_INFO                     is 65281;  # RFC5746

# Elliptic curves:
const integer: SECP192K1 is 18;
const integer: SECP192R1 is 19;
const integer: SECP224K1 is 20;
const integer: SECP224R1 is 21;
const integer: SECP256K1 is 22;
const integer: SECP256R1 is 23;
const integer: SECP384R1 is 24;
const integer: SECP521R1 is 25;

const array ellipticCurve: curveByNumber is [SECP192K1] (
    secp192k1, secp192r1, secp224k1, secp224r1, secp256k1,
    secp256r1, secp384r1, secp521r1);

const char: NAMED_CURVE is '\3;';

const array digestAlgorithm: signatureHashByNumber is [1] (
    MD5, SHA1, SHA224, SHA256, SHA384, SHA512);

const integer: RSA_PKCS1_MD5_SHA1     is 16#0100;
const integer: RSA_PKCS1_SHA1         is 16#0201;
const integer: RSA_PKCS1_SHA224       is 16#0301;
const integer: RSA_PKCS1_SHA256       is 16#0401;
const integer: RSA_PKCS1_SHA384       is 16#0501;
const integer: RSA_PKCS1_SHA512       is 16#0601;
const integer: ECDSA_SHA1             is 16#0203;
const integer: ECDSA_SECP256R1_SHA256 is 16#0403;

const array integer: signatureSchemes is [] (
    ECDSA_SECP256R1_SHA256, RSA_PKCS1_SHA256, RSA_PKCS1_SHA1, ECDSA_SHA1, RSA_PKCS1_MD5_SHA1);

const array integer: serverSignatureSchemesRsa is [] (
    RSA_PKCS1_SHA512, RSA_PKCS1_SHA384, RSA_PKCS1_SHA256, RSA_PKCS1_SHA1,
    RSA_PKCS1_MD5_SHA1);

const array integer: serverSignatureSchemesEcdsa is [] (
    ECDSA_SECP256R1_SHA256, ECDSA_SHA1);

const type: tlsParseState is new struct
    var char: contentType is NO_MESSAGE;
    var integer: length is 0;
    var string: message is "";
    var integer: pos is 1;
    var char: alert is CLOSE_NOTIFY;
  end struct;

(**
 *  [[file|File]] implementation type for TLS.
 *  This type supports communication TLS. A ''tlsFile'' is
 *  not seekable. The functions [[null_file#length(in_null_file)|length]],
 *  [[null_file#seek(in_null_file,in_integer)|seek]] and
 *  [[null_file#tell(in_null_file)|tell]] raise FILE_ERROR.
 *)
const type: tlsFile is sub null_file struct
    var file: sock is STD_NULL;
    var tlsParseState: parseState is tlsParseState.value;
    var tlsParameters: parameters is tlsParameters.value;
    var string: readBuffer is "";
  end struct;

const type: clientSession is new struct
    var string:              session_id              is "";
    var cipherAlgorithm:     bulk_cipher_algorithm   is NO_CIPHER;
    var string:              master_secret           is "";
    var time:                last_use                is time.value;
  end struct;

const duration: clientCacheValid is 1 . MINUTES;
const type: clientSessionCacheType is hash [socketAddress] clientSession;

var clientSessionCacheType: clientSessionCache is clientSessionCacheType.value;

const string: MD5_PAD1 is "\16#36;" mult 48;
const string: MD5_PAD2 is "\16#5c;" mult 48;
const string: SHA_PAD1 is "\16#36;" mult 40;
const string: SHA_PAD2 is "\16#5c;" mult 40;


# Showtls defines showTlsMsg(), showTlsMsgType(), showHandshakeMsg() and showX509Cert().
# Activate it, to debug tls.s7i.
# include "showtls.s7i";


const func integer: getEllipticCurveNumber (in ellipticCurve: curve) is func
  result
    var integer: curveNumber is 0;
  begin
    if curve.name = "secp192k1" then
      curveNumber := SECP192K1;
    elsif curve.name = "secp192r1" then
      curveNumber := SECP192R1;
    elsif curve.name = "secp224k1" then
      curveNumber := SECP224K1;
    elsif curve.name = "secp224r1" then
      curveNumber := SECP224R1;
    elsif curve.name = "secp256k1" then
      curveNumber := SECP256K1;
    elsif curve.name = "secp256r1" then
      curveNumber := SECP256R1;
    elsif curve.name = "secp384r1" then
      curveNumber := SECP384R1;
    elsif curve.name = "secp512r1" then
      curveNumber := SECP521R1;
    end if;
  end func;


const proc: storeCipherSuite (inout tlsParameters: parameters) is func
  begin
    # writeln("cipher_suite: " <& ord(parameters.cipher_suite) radix 16 lpad0 4);
    if parameters.cipher_suite = TLS_NULL_WITH_NULL_NULL then
      parameters.bulk_cipher_algorithm := NO_CIPHER;
      parameters.key_material_length := 0;
      parameters.mac_algorithm := NO_DIGEST;
    elsif parameters.cipher_suite = TLS_RSA_WITH_RC4_128_MD5 then
      parameters.bulk_cipher_algorithm := RC4;
      parameters.key_material_length := 16;
      parameters.mac_algorithm := MD5;
    elsif parameters.cipher_suite = TLS_RSA_WITH_RC4_128_SHA then
      parameters.bulk_cipher_algorithm := RC4;
      parameters.key_material_length := 16;
      parameters.mac_algorithm := SHA1;
    elsif parameters.cipher_suite = TLS_RSA_WITH_3DES_EDE_CBC_SHA then
      parameters.bulk_cipher_algorithm := TDES;
      parameters.key_material_length := 24;
      parameters.mac_algorithm := SHA1;
    elsif parameters.cipher_suite = TLS_RSA_WITH_DES_CBC_SHA then
      parameters.bulk_cipher_algorithm := DES;
      parameters.key_material_length := 8;
      parameters.mac_algorithm := SHA1;
    elsif parameters.cipher_suite = TLS_RSA_WITH_AES_128_CBC_SHA then
      parameters.bulk_cipher_algorithm := AES;
      parameters.key_material_length := 16;
      parameters.mac_algorithm := SHA1;
    elsif parameters.cipher_suite = TLS_RSA_WITH_AES_256_CBC_SHA then
      parameters.bulk_cipher_algorithm := AES;
      parameters.key_material_length := 32;
      parameters.mac_algorithm := SHA1;
    elsif parameters.cipher_suite = TLS_RSA_WITH_AES_128_CBC_SHA256 then
      parameters.bulk_cipher_algorithm := AES;
      parameters.key_material_length := 16;
      parameters.mac_algorithm := SHA256;
    elsif parameters.cipher_suite = TLS_RSA_WITH_AES_256_CBC_SHA256 then
      parameters.bulk_cipher_algorithm := AES;
      parameters.key_material_length := 32;
      parameters.mac_algorithm := SHA256;
    elsif parameters.cipher_suite = TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA then
      parameters.key_exchange_algorithm := EC_DIFFIE_HELLMAN;
      parameters.bulk_cipher_algorithm := AES;
      parameters.key_material_length := 16;
      parameters.mac_algorithm := SHA1;
    elsif parameters.cipher_suite = TLS_ECDHE_ECDSA_WITH_AES_128_CBC_SHA then
      parameters.key_exchange_algorithm := EC_DIFFIE_HELLMAN;
      parameters.bulk_cipher_algorithm := AES;
      parameters.key_material_length := 16;
      parameters.mac_algorithm := SHA1;
    elsif parameters.cipher_suite = TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 then
      parameters.key_exchange_algorithm := EC_DIFFIE_HELLMAN;
      parameters.bulk_cipher_algorithm := AES_GCM;
      parameters.key_material_length := 16;
      parameters.iv_size := 4;  # Implicit salt of the GCM nonce
      parameters.mac_algorithm := NO_DIGEST;
    elsif parameters.cipher_suite = TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256 then
      parameters.key_exchange_algorithm := EC_DIFFIE_HELLMAN;
      parameters.bulk_cipher_algorithm := AES_GCM;
      parameters.key_material_length := 16;
      parameters.iv_size := 4;  # Implicit salt of the GCM nonce
      parameters.mac_algorithm := NO_DIGEST;
    else
      writeln("Unsupported cipher_suite: " <& ord(parameters.cipher_suite) radix 16 lpad0 4);
      # raise RANGE_ERROR;
    end if;
    parameters.block_size := blockSize(parameters.bulk_cipher_algorithm);
    if parameters.iv_size = 0 then
      parameters.iv_size := parameters.block_size;
    end if;
    parameters.hash_size := digestSize(parameters.mac_algorithm);
  end func;


const proc: computeMasterSecret (inout tlsParameters: parameters,
    in string: preMasterSecret) is func
  begin
    # writeln("preMasterSecret: " <& hex(preMasterSecret));
    if parameters.tls_version = SSL_3_0 then
      parameters.master_secret := keyBlockFunction(preMasterSecret,
          parameters.client_random & parameters.server_random, 48);
    elsif parameters.tls_version >= TLS_1_2 then
      parameters.master_secret := p_hash(SHA256, preMasterSecret,
          "master secret" & parameters.client_random & parameters.server_random, 48);
    else
      parameters.master_secret := pseudoRandomFunction(preMasterSecret,
          "master secret", parameters.client_random & parameters.server_random, 48);
    end if;
    # writeln("master_secret: " <& hex(parameters.master_secret));
  end func;


const proc: storeKeys (inout tlsParameters: parameters) is func
  local
    var string: key_block is "";
    var integer: key_block_pos is 1;
    var string: client_write_MAC_secret is "";
    var string: server_write_MAC_secret is "";
    var string: client_write_key is "";
    var string: server_write_key is "";
    var string: client_initialization_vector is "";
    var string: server_initialization_vector is "";
  begin
    # writeln("client_random: " <& hex(parameters.client_random));
    # writeln("server_random: " <& hex(parameters.server_random));
    if parameters.tls_version = SSL_3_0 then
      key_block := keyBlockFunction(parameters.master_secret,
          parameters.server_random & parameters.client_random,
          2 * parameters.hash_size + 2 * parameters.key_material_length + 2 * parameters.iv_size);
    elsif parameters.tls_version >= TLS_1_2 then
      key_block := p_hash(SHA256, parameters.master_secret,
          "key expansion" & parameters.server_random & parameters.client_random,
          2 * parameters.hash_size + 2 * parameters.key_material_length + 2 * parameters.iv_size);
    else
      key_block := pseudoRandomFunction(parameters.master_secret,
          "key expansion", parameters.server_random & parameters.client_random,
          2 * parameters.hash_size + 2 * parameters.key_material_length + 2 * parameters.iv_size);
    end if;
    # writeln("key_block: " <& hex(key_block));
    # writeln("length(key_block): " <& length(key_block));
    client_write_MAC_secret := key_block[key_block_pos fixLen parameters.hash_size];
    key_block_pos +:= parameters.hash_size;
    server_write_MAC_secret := key_block[key_block_pos fixLen parameters.hash_size];
    key_block_pos +:= parameters.hash_size;
    client_write_key := key_block[key_block_pos fixLen parameters.key_material_length];
    key_block_pos +:= parameters.key_material_length;
    server_write_key := key_block[key_block_pos fixLen parameters.key_material_length];
    key_block_pos +:= parameters.key_material_length;
    client_initialization_vector := key_block[key_block_pos fixLen parameters.iv_size];
    key_block_pos +:= parameters.iv_size;
    server_initialization_vector := key_block[key_block_pos fixLen parameters.iv_size];
    # writeln("client_write_MAC_secret: " <& hex(client_write_MAC_secret));
    # writeln("server_write_MAC_secret: " <& hex(server_write_MAC_secret));
    # writeln("client_write_key: " <& hex(client_write_key));
    # writeln("server_write_key: " <& hex(server_write_key));
    # writeln("client_initialization_vector: " <& hex(client_initialization_vector));
    # writeln("server_initialization_vector: " <& hex(server_initialization_vector));
    if parameters.isClient then
      parameters.readMacSecret := server_write_MAC_secret;
      parameters.writeMacSecret := client_write_MAC_secret;
      parameters.readCipherState := setCipherKey(parameters.bulk_cipher_algorithm,
          server_write_key, server_initialization_vector);
      parameters.writeCipherState := setCipherKey(parameters.bulk_cipher_algorithm,
          client_write_key, client_initialization_vector);
    else
      parameters.readMacSecret := client_write_MAC_secret;
      parameters.writeMacSecret := server_write_MAC_secret;
      parameters.readCipherState := setCipherKey(parameters.bulk_cipher_algorithm,
          client_write_key, client_initialization_vector);
      parameters.writeCipherState := setCipherKey(parameters.bulk_cipher_algorithm,
          server_write_key, server_initialization_vector);
    end if;
  end func;


const func string: genRsaSignature (in string: signature, in digestAlgorithm: digestAlg) is func
  result
    var string: signatureString is "";
  local
    var algorithmIdentifierType: algorithmIdentifier is algorithmIdentifierType.value;
  begin
    case digestAlg of
      when {SHA1}:   algorithmIdentifier.algorithm := SHA1_OID;
      when {SHA256}: algorithmIdentifier.algorithm := SHA256_OID;
      when {SHA384}: algorithmIdentifier.algorithm := SHA384_OID;
      when {SHA512}: algorithmIdentifier.algorithm := SHA512_OID;
    end case;
    signatureString := genAsn1Sequence(
            genAlgorithmIdentifier(algorithmIdentifier) &
            genAsn1Element(tagOctetString, signature));
  end func;


const func boolean: verifySignature (in string: hashParameter, in integer: signatureScheme,
    in string: signatureStri, in tlsParameters: parameters, inout tlsParseState: state) is func
  result
    var boolean: verified is FALSE;
  local
    var string: signatureHash is "";
    var string: decryptedSignature is "";
    var rsaSignatureType: rsaSignature is rsaSignatureType.value;
    var ecdsaSignatureType: ecdsaSignature is ecdsaSignatureType.value;
  begin
    case signatureScheme of
      when {RSA_PKCS1_MD5_SHA1}:
        signatureHash := md5(hashParameter) & sha1(hashParameter);
        verified := rsassaPkcs1V15Decrypt(parameters.publicRsaCertificateKey, signatureStri) = signatureHash;
      when {RSA_PKCS1_SHA1, RSA_PKCS1_SHA224, RSA_PKCS1_SHA256, RSA_PKCS1_SHA384, RSA_PKCS1_SHA512}:
        signatureHash := msgDigest(signatureHashByNumber[signatureScheme mdiv 256],
                                   hashParameter);
        decryptedSignature := rsassaPkcs1V15Decrypt(parameters.publicRsaCertificateKey, signatureStri);
        rsaSignature := getRsaSignature(decryptedSignature);
        verified := rsaSignature.signature = signatureHash;
      when {ECDSA_SECP256R1_SHA256}:
        signatureHash := sha256(hashParameter);
        ecdsaSignature := getEcdsaSignature(signatureStri);
        verified := verify(secp256r1, bytes2BigInt(signatureHash, UNSIGNED, BE),
                           ecdsaSignature, parameters.publicEccCertificateKey);
      when {ECDSA_SHA1}:
        signatureHash := sha1(hashParameter);
        ecdsaSignature := getEcdsaSignature(signatureStri);
        verified := verify(parameters.curve, bytes2BigInt(signatureHash, UNSIGNED, BE),
                           ecdsaSignature, parameters.publicEccCertificateKey);
    end case;
  end func;


const func string: genSignature (in string: hashParameter, in tlsParameters: parameters) is func
  result
    var string: signatureStri is "";
  local
    var string: signatureHash is "";
    var string: rsaSignatureStri is "";
    var digestAlgorithm: digestAlg is NO_DIGEST;
    var ecdsaSignatureType: ecdsaSignature is ecdsaSignatureType.value;
  begin
    case parameters.signatureScheme of
      when {RSA_PKCS1_MD5_SHA1}:
        signatureHash := md5(hashParameter) & sha1(hashParameter);
        signatureStri := rsassaPkcs1V15Encrypt(parameters.privateRsaCertificateKey, signatureHash);
      when {RSA_PKCS1_SHA1, RSA_PKCS1_SHA224, RSA_PKCS1_SHA256, RSA_PKCS1_SHA384, RSA_PKCS1_SHA512}:
        digestAlg := signatureHashByNumber[parameters.signatureScheme mdiv 256];
        signatureHash := msgDigest(digestAlg, hashParameter);
        rsaSignatureStri := genRsaSignature(signatureHash, digestAlg);
        signatureStri := rsassaPkcs1V15Encrypt(parameters.privateRsaCertificateKey, rsaSignatureStri);
      when {ECDSA_SECP256R1_SHA256}:
        signatureHash := sha256(hashParameter);
        ecdsaSignature := sign(secp256r1, bytes2BigInt(signatureHash, UNSIGNED, BE),
                               parameters.privateEccCertificateKey);
        signatureStri := genAsn1Sequence(
            genAsn1Element(tagInteger, bytes(ecdsaSignature.r, SIGNED, BE)) &
            genAsn1Element(tagInteger, bytes(ecdsaSignature.s, SIGNED, BE)));
    end case;
    signatureStri := bytes(parameters.signatureScheme, UNSIGNED, BE, 2) &
                     bytes(length(signatureStri),      UNSIGNED, BE, 2) &
                     signatureStri;
  end func;


const proc: validateCertificates (in array x509Cert: cert) is func
  local
    var integer: index is 1;
    var integer: issuerIndex is 1;
    var string: commonName is "";
    var certSubjectIndexHashType: certSubjectIndexHash is certSubjectIndexHashType.value;
    var boolean: validated is FALSE;
  begin
    for key index range cert do
      # writeln("examine Cert-" <& index);
      if time(NOW) >= cert[index].tbsCertificate.validity.notBefore and
          time(NOW) <= cert[index].tbsCertificate.validity.notAfter then
        if COMMON_NAME_OID in cert[index].tbsCertificate.subject then
          if cert[index].tbsCertificate.subject[COMMON_NAME_OID] not in certSubjectIndexHash then
            commonName := cert[index].tbsCertificate.subject[COMMON_NAME_OID];
            # writeln("commonName: " <& commonName);
            certSubjectIndexHash @:= [commonName] index;
          else
            writeln("***** Second certificate with same common name.");
          end if;
        else
          writeln("***** Certificate without common name.");
        end if;
      else
        writeln("***** Certificate invalid now.");
      end if;
    end for;

    repeat
      index := issuerIndex;
      if COMMON_NAME_OID in cert[index].tbsCertificate.issuer and
          cert[index].tbsCertificate.issuer[COMMON_NAME_OID] in certSubjectIndexHash then
        issuerIndex := certSubjectIndexHash[cert[index].tbsCertificate.issuer[COMMON_NAME_OID]];
        # writeln("validate Cert-" <& index <& " with Cert-" <& issuerIndex);
        validated := validateSignature(cert[index], cert[issuerIndex].tbsCertificate.subjectPublicKeyInfo);
        # writeln(validated);
      else
        # writeln("Issuer not found.");
        issuerIndex := 0;
        validated := FALSE;
      end if;
    until index = issuerIndex or not validated;
    if index = 1 and issuerIndex = 1 then
      writeln("Self signed certificate.");
    elsif not validated then
      writeln("***** Cannot be validated.");
    end if;
  end func;


const proc: processCertificate (inout tlsParameters: parameters, inout tlsParseState: state) is func
  local
    var integer: startPos is 0;
    var integer: sequenceLen is 0;
    var integer: certLen is 0;
    var integer: index is 1;
    var array x509Cert: cert is 0 times x509Cert.value;
  begin
    # writeln("certificate");
    startPos := state.pos;
    state.pos +:= 4;
    sequenceLen := bytes2Int(state.message[state.pos fixLen 3], UNSIGNED, BE);
    state.pos +:= 3;
    while state.pos <= 3 + sequenceLen do
      certLen := bytes2Int(state.message[state.pos fixLen 3], UNSIGNED, BE);
      state.pos +:= 3;
      parameters.serverCertificates.certList &:= [] (state.message[state.pos len certLen]);
      state.pos +:= certLen;
    end while;
    cert := length(parameters.serverCertificates.certList) times x509Cert.value;
    for key index range parameters.serverCertificates.certList do
      # writeln("read Cert-" <& index);
      cert[index] := getX509Cert(parameters.serverCertificates.certList[index]);
    end for;
    # showX509Cert(cert[1]);
    # validateCertificates(cert);
    parameters.publicRsaCertificateKey := cert[1].tbsCertificate.subjectPublicKeyInfo.publicRsaKey;
    parameters.publicEccCertificateKey := cert[1].tbsCertificate.subjectPublicKeyInfo.publicEccKey;
    # writeln("rsa key: " <& literal(parameters.publicRsaCertificateKey));
    # writeln("ecc key: " <& literal(parameters.publicEccCertificateKey));
    if  parameters.publicRsaCertificateKey.modulus = 0_ and
        parameters.publicRsaCertificateKey.exponent = 0_ and
        parameters.publicEccCertificateKey.x = 0_ and
        parameters.publicEccCertificateKey.y = 0_ then
      state.alert := BAD_CERTIFICATE;
    end if;
    parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  end func;


const proc: processClientCertificate (inout tlsParameters: parameters, inout tlsParseState: state) is func
  local
    var integer: startPos is 0;
    var integer: sequenceLen is 0;
    var integer: certLen is 0;
    var integer: index is 1;
    var array x509Cert: cert is 0 times x509Cert.value;
  begin
    # writeln("client_certificate");
    startPos := state.pos;
    state.pos +:= 4;
    sequenceLen := bytes2Int(state.message[state.pos fixLen 3], UNSIGNED, BE);
    state.pos +:= 3;
    while state.pos <= 3 + sequenceLen do
      certLen := bytes2Int(state.message[state.pos fixLen 3], UNSIGNED, BE);
      state.pos +:= 3;
      parameters.clientCertificates.certList &:= [] (state.message[state.pos len certLen]);
      state.pos +:= certLen;
    end while;
    cert := length(parameters.clientCertificates.certList) times x509Cert.value;
    for key index range parameters.clientCertificates.certList do
      # writeln("read Cert-" <& index);
      cert[index] := getX509Cert(parameters.clientCertificates.certList[index]);
    end for;
    # showX509Cert(cert[1]);
    # validateCertificates(cert);
    # parameters.publicRsaCertificateKey := cert[1].tbsCertificate.subjectPublicKeyInfo.publicRsaKey;
    # parameters.publicEccCertificateKey := cert[1].tbsCertificate.subjectPublicKeyInfo.publicEccKey;
    parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  end func;


const proc: processCertificateVerify (inout tlsParameters: parameters, inout tlsParseState: state) is func
  local
    var integer: startPos is 0;
    var integer: length is 0;
  begin
    # writeln("certificate_verify");
    startPos := state.pos;
    incr(state.pos);
    length := bytes2Int(state.message[state.pos fixLen 3], UNSIGNED, BE);
    state.pos +:= 3;
    state.pos +:= length;
    parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  end func;


const proc: processEllipticCurvesExtension (inout tlsParameters: parameters,
    in string: extensionData) is func
  local
    var integer: pos is 1;
    var integer: length is 0;
    var integer: curveNumber is 0;
  begin
    length := bytes2Int(extensionData[pos fixLen 2], UNSIGNED, BE);
    pos +:= 2;
    while pos < length(extensionData) and parameters.curve.bits = 0 do
      curveNumber := bytes2Int(extensionData[pos fixLen 2], UNSIGNED, BE);
      # writeln("curveNumber: " <& curveNumber);
      pos +:= 2;
      if curveNumber >= minIdx(curveByNumber) and curveNumber <= maxIdx(curveByNumber) then
        parameters.curve := curveByNumber[curveNumber];
      end if;
    end while;
    # writeln("curve.name: " <& parameters.curve.name);
  end func;


const proc: processSignatureAlgorithmsExtension (inout tlsParameters: parameters,
    in string: extensionData) is func
  local
    var integer: pos is 1;
    var integer: length is 0;
    var integer: signatureScheme is 0;
    var integer: schemeFromList is 0;
  begin
    length := bytes2Int(extensionData[pos fixLen 2], UNSIGNED, BE);
    pos +:= 2;
    while pos < length(extensionData) and parameters.signatureScheme = 0 do
      signatureScheme := bytes2Int(extensionData[pos fixLen 2], UNSIGNED, BE);
      # writeln("signatureScheme: " <& signatureScheme radix 16 lpad0 4);
      pos +:= 2;
      if parameters.key_exchange_algorithm = EC_DIFFIE_HELLMAN then
        for schemeFromList range serverSignatureSchemesEcdsa until parameters.signatureScheme <> 0 do
          if schemeFromList = signatureScheme then
            parameters.signatureScheme := signatureScheme;
          end if;
        end for;
      else
        for schemeFromList range serverSignatureSchemesRsa until parameters.signatureScheme <> 0 do
          if schemeFromList = signatureScheme then
            parameters.signatureScheme := signatureScheme;
          end if;
        end for;
      end if;
    end while;
    # writeln("signatureScheme: " <& parameters.signatureScheme radix 16 lpad0 4);
  end func;


const proc: processClientExtensions (inout tlsParameters: parameters, in string: extensions) is func
  local
    var integer: pos is 1;
    var integer: extensionType is 0;
    var integer: dataSize is 0;
    var string: data is "";
  begin
    while pos < length(extensions) do
      extensionType := bytes2Int(extensions[pos fixLen 2], UNSIGNED, BE);
      pos +:= 2;
      dataSize := bytes2Int(extensions[pos fixLen 2], UNSIGNED, BE);
      pos +:= 2;
      data := extensions[pos len dataSize];
      pos +:= dataSize;
      case extensionType of
        when {ELLIPTIC_CURVES}:
          processEllipticCurvesExtension(parameters, data);
        when {SIGNATURE_ALGORITHMS}:
          processSignatureAlgorithmsExtension(parameters, data);
      end case;
    end while;
  end func;


const proc: processClientHello (inout tlsParameters: parameters, inout tlsParseState: state) is func
  local
    var integer: startPos is 0;
    var integer: length is 0;
    var integer: beyond is 0;
    var integer: sessionIdLen is 0;
    var integer: numCipherSuites is 0;
    var integer: numCompressionMethods is 0;
    var integer: extensionBytes is 0;
    var integer: index is 0;
    var integer: cipher_suite_number is ord(TLS_NULL_WITH_NULL_NULL);
    var integer: searchIndex is 0;
    var integer: minIndex is succ(length(supportedCiphers));
  begin
    # writeln("client_hello");
    startPos := state.pos;
    incr(state.pos);
    length := bytes2Int(state.message[state.pos fixLen 3], UNSIGNED, BE);
    state.pos +:= 3;
    beyond := state.pos + length;
    if state.message[state.pos len 2] >= SSL_3_0 and
        state.message[state.pos len 2] <= TLS_1_3 then
      if state.message[state.pos len 2] < parameters.tls_version then
        parameters.tls_version := state.message[state.pos len 2];
      end if;
      state.pos +:= 2;
      parameters.client_random := state.message[state.pos len 32];
      state.pos +:= 32;
      sessionIdLen := ord(state.message[state.pos]);
      incr(state.pos);
      # writeln("SessionId: " <& hex(state.message[state.pos len sessionIdLen]));
      state.pos +:= sessionIdLen;
      numCipherSuites := bytes2Int(state.message[state.pos fixLen 2], UNSIGNED, BE) div 2;
      state.pos +:= 2;
      for index range 1 to numCipherSuites do
        cipher_suite_number := bytes2Int(state.message[state.pos fixLen 2], UNSIGNED, BE);
        for key searchIndex range supportedCiphers do
          if ord(supportedCiphers[searchIndex]) = cipher_suite_number and
              searchIndex < minIndex then
            minIndex := searchIndex;
          end if;
        end for;
        state.pos +:= 2;
      end for;
      if minIndex <= length(supportedCiphers) then
        parameters.cipher_suite := supportedCiphers[minIndex];
        # writeln("cipher_suite: " <& parameters.cipher_suite radix 16 lpad0 4);
        storeCipherSuite(parameters);
      else
        state.alert := HANDSHAKE_FAILURE;
      end if;
      numCompressionMethods := ord(state.message[state.pos]);
      state.pos +:= 1 + numCompressionMethods;
      if state.pos <= beyond - 2 then
        extensionBytes := bytes2Int(state.message[state.pos fixLen 2], UNSIGNED, BE);
        state.pos +:= 2;
        processClientExtensions(parameters, state.message[state.pos len extensionBytes]);
        state.pos +:= extensionBytes;
      end if;
    else
      state.alert := PROCOCOL_VERSION;
    end if;
    parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  end func;


const proc: processServerHello (inout tlsParameters: parameters, inout tlsParseState: state) is func
  local
    var integer: startPos is 0;
    var integer: length is 0;
    var integer: beyond is 0;
    var integer: sessionIdLen is 0;
    var integer: extensionBytes is 0;
  begin
    # writeln("server_hello");
    startPos := state.pos;
    incr(state.pos);
    length := bytes2Int(state.message[state.pos fixLen 3], UNSIGNED, BE);
    state.pos +:= 3;
    beyond := state.pos + length;
    if state.message[state.pos len 2] >= SSL_3_0 and
        state.message[state.pos len 2] <= parameters.tls_version then
      parameters.tls_version := state.message[state.pos len 2];
      state.pos +:= 2;
      parameters.server_random := state.message[state.pos len 32];
      state.pos +:= 32;
      sessionIdLen := ord(state.message[state.pos]);
      incr(state.pos);
      parameters.session_id := state.message[state.pos len sessionIdLen];
      state.pos +:= sessionIdLen;
      parameters.cipher_suite := cipherSuite conv bytes2Int(state.message[state.pos fixLen 2], UNSIGNED, BE);
      # writeln("Cipher: " <& ord(parameters.cipher_suite));
      storeCipherSuite(parameters);
      state.pos +:= 2;
      parameters.compression_algorithm := ord(state.message[state.pos]);
      incr(state.pos);
      if state.pos <= beyond - 2 then
        extensionBytes := bytes2Int(state.message[state.pos fixLen 2], UNSIGNED, BE);
        state.pos +:= 2 + extensionBytes;
      end if;
    else
      state.alert := PROCOCOL_VERSION;
    end if;
    parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  end func;


const proc: processServerKeyExchange (inout tlsParameters: parameters, inout tlsParseState: state) is func
  local
    var integer: startPos is 0;
    var integer: length is 0;
    var integer: beyond is 0;
    var integer: paramsStartPos is 0;
    var integer: curveNumber is 0;
    var integer: pointLength is 0;
    var string: pointData is "";
    var string: serverParams is "";
    var integer: signatureScheme is 0;
    var integer: signatureLength is 0;
    var string: signatureStri is "";
    var boolean: verified is FALSE;
  begin
    # writeln("server_key_exchange");
    startPos := state.pos;
    incr(state.pos);
    length := bytes2Int(state.message[state.pos fixLen 3], UNSIGNED, BE);
    state.pos +:= 3;
    beyond := state.pos + length;
    if parameters.key_exchange_algorithm = EC_DIFFIE_HELLMAN then
      if state.message[state.pos] = NAMED_CURVE then
        paramsStartPos := state.pos;
        incr(state.pos);
        curveNumber := bytes2Int(state.message[state.pos fixLen 2], UNSIGNED, BE);
        state.pos +:= 2;
        if curveNumber < minIdx(curveByNumber) or curveNumber > maxIdx(curveByNumber) then
          state.alert := ILLEGAL_PARAMETER;
        else
          parameters.curve := curveByNumber[curveNumber];
          pointLength := ord(state.message[state.pos]);
          incr(state.pos);
          pointData := state.message[state.pos len pointLength];
          parameters.publicEccKeyOfServer := ecPointDecode(parameters.curve, pointData);
          state.pos +:= pointLength;
          serverParams := state.message[paramsStartPos .. pred(state.pos)];
          signatureScheme := bytes2Int(state.message[state.pos fixLen 2], UNSIGNED, BE);
          state.pos +:= 2;
          if parameters.tls_version >= TLS_1_2 then
            signatureLength := bytes2Int(state.message[state.pos fixLen 2], UNSIGNED, BE);
            state.pos +:= 2;
          else
            signatureLength := beyond - state.pos;
          end if;
          signatureStri := state.message[state.pos len signatureLength];
          state.pos +:= signatureLength;
          if not verifySignature(parameters.client_random &
                                 parameters.server_random &
                                 serverParams, signatureScheme, signatureStri,
                                 parameters, state) then
            state.alert := HANDSHAKE_FAILURE;
          end if;
        end if;
      else
        state.alert := ILLEGAL_PARAMETER;
      end if;
    end if;
    parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  end func;


const proc: processCertificateRequest (inout tlsParameters: parameters, inout tlsParseState: state) is func
  local
    var integer: startPos is 0;
    var integer: length is 0;
  begin
    # writeln("certificate_request");
    startPos := state.pos;
    incr(state.pos);
    length := bytes2Int(state.message[state.pos fixLen 3], UNSIGNED, BE);
    state.pos +:= 3;
    state.pos +:= length;
    parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  end func;


const proc: processServerHelloDone (inout tlsParameters: parameters, inout tlsParseState: state) is func
  local
    var integer: startPos is 0;
    var integer: length is 0;
  begin
    # writeln("server_hello_done");
    startPos := state.pos;
    incr(state.pos);
    length := bytes2Int(state.message[state.pos fixLen 3], UNSIGNED, BE);
    state.pos +:= 3;
    parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  end func;


const proc: processClientKeyExchange (inout tlsParameters: parameters, inout tlsParseState: state) is func
  local
    var integer: startPos is 0;
    var integer: length is 0;
    var integer: encryptedSecretLength is 0;
    var string: encryptedPreMasterSecret is "";
    var string: preMasterSecret is "";
    var integer: pointLength is 0;
    var string: pointData is "";
    var ecPoint: publicEccKeyOfClient is ecPoint.value;
    var ecPoint: sharedSecretEcPoint is ecPoint.value;
  begin
    # writeln("client_key_exchange");
    startPos := state.pos;
    incr(state.pos);
    length := bytes2Int(state.message[state.pos fixLen 3], UNSIGNED, BE);
    state.pos +:= 3;
    if parameters.key_exchange_algorithm = RSA then
      if parameters.tls_version = SSL_3_0 then
        encryptedSecretLength := length;
      else
        encryptedSecretLength := bytes2Int(state.message[state.pos fixLen 2], UNSIGNED, BE);
        state.pos +:= 2;
      end if;
      encryptedPreMasterSecret := state.message[state.pos len encryptedSecretLength];
      state.pos +:= encryptedSecretLength;
      # writeln("encryptedPreMasterSecret: " <& hex(encryptedPreMasterSecret));
      # writeln("length(encryptedPreMasterSecret): " <& length(encryptedPreMasterSecret));
      preMasterSecret := rsaesPkcs1V15Decrypt(parameters.privateRsaCertificateKey,
          encryptedPreMasterSecret);
    elsif parameters.key_exchange_algorithm = EC_DIFFIE_HELLMAN then
      pointLength := ord(state.message[state.pos]);
      incr(state.pos);
      pointData := state.message[state.pos len pointLength];
      publicEccKeyOfClient := ecPointDecode(parameters.curve, pointData);
      state.pos +:= pointLength;
      sharedSecretEcPoint := multFast(parameters.curve, publicEccKeyOfClient,
                                      parameters.ownEccKeyPair.privateKey);
      # writeln("sharedSecretEcPoint.x: " <& sharedSecretEcPoint.x radix 16);
      # writeln("length: " <& getSizeInBytes(parameters.curve));
      preMasterSecret := bytes(sharedSecretEcPoint.x, UNSIGNED, BE,
                               getSizeInBytes(parameters.curve));
    end if;
    # writeln("preMasterSecret: " <& hex(preMasterSecret));
    computeMasterSecret(parameters, preMasterSecret);
    # writeln("master_secret: " <& hex(parameters.master_secret));
    storeKeys(parameters);
    parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  end func;


const proc: processChangeCipherSpec (inout tlsParameters: parameters, inout tlsParseState: state) is func
  begin
    # writeln("change_cipher_spec");
    incr(state.pos);
  end func;


const proc: processFinished (inout tlsParameters: parameters, inout tlsParseState: state) is func
  local
    var integer: startPos is 0;
    var integer: length is 0;
    var string: finished_label is "";
    var string: verify_data is "";
    var string: handshake_hash is "";
    var string: computed_verify_data is "";
  begin
    # writeln("finished");
    startPos := state.pos;
    incr(state.pos);
    length := bytes2Int(state.message[state.pos fixLen 3], UNSIGNED, BE);
    state.pos +:= 3;
    verify_data := state.message[state.pos len length];
    state.pos +:= length;
    # writeln("verify_data: " <& hex(verify_data));
    # writeln("master_secret: " <& hex(parameters.master_secret));
    # writeln("handshake_messages: " <& hex(parameters.handshake_messages));
    # writeln("tls_version: " <& literal(parameters.tls_version));
    if parameters.tls_version = SSL_3_0 then
      if parameters.isClient then
        finished_label := "SRVR";  # The sender is a server.
      else
        finished_label := "CLNT";  # The sender is a client.
      end if;
      # writeln("finished_label: " <& literal(finished_label));
      computed_verify_data := md5(parameters.master_secret & MD5_PAD2 &
                                  md5(parameters.handshake_messages & finished_label &
                                      parameters.master_secret & MD5_PAD1)) &
                              sha1(parameters.master_secret & SHA_PAD2 &
                                   sha1(parameters.handshake_messages & finished_label &
                                        parameters.master_secret & SHA_PAD1));
    else
      if parameters.isClient then
        finished_label := "server finished";  # The sender is a server.
      else
        finished_label := "client finished";  # The sender is a client.
      end if;
      # writeln("finished_label: " <& literal(finished_label));
      if parameters.tls_version >= TLS_1_2 then
        computed_verify_data := p_hash(SHA256, parameters.master_secret, finished_label &
                                       sha256(parameters.handshake_messages), 12);
      else
        handshake_hash := md5(parameters.handshake_messages) &
                          sha1(parameters.handshake_messages);
        # writeln("handshake_hash: " <& hex(handshake_hash));
        # writeln("handshake_hash size: " <& length(handshake_hash));
        computed_verify_data := pseudoRandomFunction(parameters.master_secret, finished_label,
                                                     handshake_hash, 12);
      end if;
    end if;
    # writeln("computed_verify_data: " <& hex(computed_verify_data));
    if verify_data <> computed_verify_data then
      writeln(" ***** Handshake not verified");
      raise RANGE_ERROR;
    end if;
    parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  end func;


const proc: getTlsMsgRecord (inout file: sock, inout tlsParseState: state) is func
  local
    var integer: missing is 0;
    var string: msg2 is "";
  begin
    # writeln("in getTlsMsgRecord");
    if state.pos > length(state.message) then
      state.message := gets(sock, 5);
      if length(state.message) = 5 and
          state.message[1] >= CHANGE_CIPHER_SPEC and state.message[1] <= APPLICATION_DATA then
        state.contentType := state.message[1];
        state.length := bytes2Int(state.message[4 fixLen 2], UNSIGNED, BE);
        missing := state.length;
        repeat
          msg2 := gets(sock, missing);
          state.message &:= msg2;
          missing -:= length(msg2);
        until missing = 0 or eof(sock);
        if missing = 0 then
          state.pos := 6;
        else
          state.contentType := NO_MESSAGE;
          state.length := 0;
        end if;
      else
        state.contentType := NO_MESSAGE;
        state.length := 0;
        # writeln("EOF = " <& eof(sock));
        # writeln("length(message) = " <& length(state.message));
        # writeln("message = " <& literal(state.message));
        # raise RANGE_ERROR;
      end if;
    end if;
    # writeln("getTlsMsgRecord -> " <& length(state.message) <& " " <& literal(state.message));
    # showTlsMsgType(state.message);
    # showTlsMsg(state.message);
  end func;


const proc: loadCompleteHandshakeMsg (inout file: sock, inout tlsParseState: state) is func
  local
    var integer: lengthOfHandshakeMsg is 0;
    var integer: remainingBytesInMsgRecord is 0;
    var integer: totallyMissing is 0;
    var string: stri is "";
    var integer: recordLength is 0;
    var integer: missing is 0;
    var string: msg2 is "";
  begin
    if length(state.message) >= state.pos + 3 then
      # Determine the length of the handshake message.
      lengthOfHandshakeMsg := bytes2Int(state.message[state.pos + 1 fixLen 3], UNSIGNED, BE);
      remainingBytesInMsgRecord := length(state.message) - state.pos - 3;
      if lengthOfHandshakeMsg > remainingBytesInMsgRecord then
        # In the current TLS message record are not enough characters.
        totallyMissing := lengthOfHandshakeMsg - remainingBytesInMsgRecord;
        # writeln("totallyMissing: " <& totallyMissing);
        repeat
          # Get the next TLS message record.
          stri := gets(sock, 5);
          if length(stri) = 5 and stri[1] = HANDSHAKE then
            # We are reading additional data for a handshake message.
            recordLength := bytes2Int(stri[4 fixLen 2], UNSIGNED, BE);
            missing := recordLength;
            repeat
              msg2 := gets(sock, missing);
              state.message &:= msg2;
              missing -:= length(msg2);
            until missing = 0 or eof(sock);
            totallyMissing -:= recordLength;
          else
            state.alert := UNEXPECTED_MESSAGE;
          end if;
        until totallyMissing <= 0 or eof(sock);
      end if;
    end if;
  end func;


const func string: genExtension (in integer: extensionType, in string: data) is
  return bytes(extensionType, UNSIGNED, BE, 2) &
         bytes(length(data),  UNSIGNED, BE, 2) & data;


const func string: serverNameExtension (in string: serverName) is
  return bytes(length(serverName) + 3, UNSIGNED, BE, 2) & "\0;" &
         bytes(length(serverName),     UNSIGNED, BE, 2) & serverName;


const func string: genEllipticCurvesExtension (in array ellipticCurve: curves) is func
  result
    var string: extensionBytes is "";
  local
    var integer: curveNumber is 0;
  begin
    extensionBytes := bytes(length(curves) * 2, UNSIGNED, BE, 2);
    for key curveNumber range curves do
      extensionBytes &:= bytes(curveNumber, UNSIGNED, BE, 2);
    end for;
  end func;


const func string: int16BeArrayExtension (in array integer: intArray) is func
  result
    var string: extensionBytes is "";
  local
    var integer: intValue is 0;
  begin
    extensionBytes := bytes(length(intArray) * 2, UNSIGNED, BE, 2);
    for intValue range intArray do
      extensionBytes &:= bytes(intValue, UNSIGNED, BE, 2);
    end for;
  end func;


const func string: genClientExtensions (in tlsParameters: parameters) is func
  result
    var string: extensionBytes is "";
  begin
    if parameters.hostName <> "" then
      extensionBytes &:= genExtension(SERVER_NAME, serverNameExtension(parameters.hostName));
    end if;
    extensionBytes &:= genExtension(ELLIPTIC_CURVES, genEllipticCurvesExtension(curveByNumber));
    extensionBytes &:= genExtension(SIGNATURE_ALGORITHMS, int16BeArrayExtension(signatureSchemes));
    if extensionBytes <> "" then
      extensionBytes := bytes(length(extensionBytes), UNSIGNED, BE, 2) & extensionBytes;
    end if;
  end func;


const func string: genClientHello (inout tlsParameters: parameters, in string: sessionId) is func
  result
    var string: clientHello is "";
  local
    var integer: length is 0;
    var integer: count is 0;
    var cipherSuite: cipher is TLS_NULL_WITH_NULL_NULL;
  begin
    parameters.client_random :=
        bytes(timestamp1970(time(NOW)),      UNSIGNED, BE,  4) &  # Random - gmt_unix_time
        bytes(rand(0_, 2_ ** (28 * 8) - 1_), UNSIGNED, BE, 28);   # Random - random_bytes
    clientHello := str(HANDSHAKE) &               # ContentType (index: 1)
                   parameters.tls_version &       # Version: 3.1
                   "\0;\0;" &                     # Length: filled later (index: 4)
                   str(CLIENT_HELLO) &            # HandshakeType (index: 6)
                   "\0;\0;\0;" &                  # Length: filled later
                   parameters.tls_version &       # Version: 3.1
                   parameters.client_random &     # Random - random_bytes
                   str(chr(length(sessionId))) &  # SessionId length
                   sessionId &                    # SessionId
                   bytes(2 * length(supportedCiphers), UNSIGNED, BE, 2);  # Number of Ciphers in bytes
    for cipher range supportedCiphers do
      clientHello &:= bytes(ord(cipher), UNSIGNED, BE, 2);
    end for;
    clientHello &:= "\1;" &                       # Number of CompressionMethods: 1 (1 byte)
                    "\0;";                        # CompressionMethod-1: 0
    clientHello &:= genClientExtensions(parameters);
    length := length(clientHello);
    clientHello @:= [4] bytes(length - 5, UNSIGNED, BE, 2);
    clientHello @:= [8] bytes(length - 9, UNSIGNED, BE, 2);
    parameters.handshake_messages &:= clientHello[6 ..];
  end func;


const func string: genServerHello (inout tlsParameters: parameters) is func
  result
    var string: serverHello is "";
  local
    const integer: SESSION_ID_LEN is 32;
    var integer: length is 0;
    var integer: count is 0;
  begin
    parameters.server_random :=
        bytes(timestamp1970(time(NOW)),      UNSIGNED, BE,  4) &  # Random - gmt_unix_time
        bytes(rand(0_, 2_ ** (28 * 8) - 1_), UNSIGNED, BE, 28);   # Random - random_bytes
    parameters.session_id :=
        bytes(rand(0_, 2_ ** (SESSION_ID_LEN * 8) - 1_), UNSIGNED, BE, SESSION_ID_LEN);  # SessionId
    serverHello := str(HANDSHAKE) &            # ContentType (index: 1)
                   parameters.tls_version &    # Version: take version from client_hello.
                   "\0;\0;" &                  # Length: filled later (index: 4)
                   str(SERVER_HELLO) &         # HandshakeType (index: 6)
                   "\0;\0;\0;" &               # Length: filled later
                   parameters.tls_version &    # Version: take version from client_hello.
                   parameters.server_random &  # Random
                   str(chr(SESSION_ID_LEN)) &  # SessionId length
                   parameters.session_id &     # SessionId
                   bytes(ord(parameters.cipher_suite), UNSIGNED, BE, 2) &
                   "\0;";                      # CompressionMethod: 0
    length := length(serverHello);
    serverHello @:= [4] bytes(length - 5, UNSIGNED, BE, 2);
    serverHello @:= [8] bytes(length - 9, UNSIGNED, BE, 2);
    parameters.handshake_messages &:= serverHello[6 ..];
  end func;


const func string: genCertificate (inout tlsParameters: parameters, in array string: certList) is func
  result
    var string: certificate is "";
  local
    var integer: length is 0;
    var integer: index is 0;
  begin
    certificate := str(HANDSHAKE) &          # ContentType (index: 1)
                   parameters.tls_version &  # Version: take version from client_hello.
                   "\0;\0;" &                # Length: filled later (index: 4)
                   str(CERTIFICATE) &        # HandshakeType (index: 6)
                   "\0;\0;\0;" &             # Length: filled later
                   "\0;\0;\0;";              # Sequence length: filled later
    for key index range certList do
      certificate &:= "\0;" &
                      bytes(length(certList[index]), UNSIGNED, BE, 2) &
                      certList[index];
    end for;
    length := length(certificate);
    certificate @:= [ 4] bytes(length -  5, UNSIGNED, BE, 2);
    certificate @:= [ 8] bytes(length -  9, UNSIGNED, BE, 2);
    certificate @:= [11] bytes(length - 12, UNSIGNED, BE, 2);
    parameters.handshake_messages &:= certificate[6 ..];
  end func;


const func string: genServerKeyExchange (inout tlsParameters: parameters) is func
  result
    var string: serverKeyExchange is "";
  local
    var integer: length is 0;
    var string: serverParams is "";
    var string: pointData is "";
    var string: signatureHash is "";
    var string: signatureStri is "";
  begin
    # writeln("genServerKeyExchange");
    serverKeyExchange := str(HANDSHAKE) &            # ContentType (index: 1)
                         parameters.tls_version &    # Version: 3.1
                         "\0;\0;" &                  # Length: filled later (index: 4)
                         str(SERVER_KEY_EXCHANGE) &  # HandshakeType (index: 6)
                         "\0;\0;\0;";                # Length: filled later
    if parameters.key_exchange_algorithm = EC_DIFFIE_HELLMAN then
      # writeln("curve.name: " <& parameters.curve.name);
      parameters.ownEccKeyPair := genEccKeyPair(parameters.curve);
      # writeln("curve number: " <& getEllipticCurveNumber(parameters.curve));
      pointData := ecPointEncode(parameters.curve, parameters.ownEccKeyPair.publicKey);
      serverParams &:= str(NAMED_CURVE) &
                       bytes(getEllipticCurveNumber(parameters.curve), UNSIGNED, BE, 2) &
                       str(chr(length(pointData))) & pointData;
      signatureStri := genSignature(parameters.client_random &
                                    parameters.server_random &
                                    serverParams, parameters);
      serverKeyExchange &:= serverParams & signatureStri;
    end if;
    length := length(serverKeyExchange);
    serverKeyExchange @:= [4] bytes(length - 5, UNSIGNED, BE, 2);
    serverKeyExchange @:= [8] bytes(length - 9, UNSIGNED, BE, 2);
    parameters.handshake_messages &:= serverKeyExchange[6 ..];
  end func;


const func string: genCertificateRequest (inout tlsParameters: parameters) is func
  result
    var string: certificateRequest is "";
  local
    var integer: length is 0;
    var integer: signatureAlgorithm is 0;
  begin
    certificateRequest := str(HANDSHAKE) &            # ContentType (index: 1)
                          parameters.tls_version &    # Version: take version from client_hello.
                          "\0;\0;" &                  # Length: filled later (index: 4)
                          str(CERTIFICATE_REQUEST) &  # HandshakeType (index: 6)
                          "\0;\0;\0;" &               # Length: filled later
                          "\1;" &                     # Bytes in certificate_types list
                          "\1;";                      # Certificate type: rsa_sign
    if parameters.tls_version >= TLS_1_2 then
      if parameters.key_exchange_algorithm = EC_DIFFIE_HELLMAN then
        certificateRequest &:= bytes(length(serverSignatureSchemesEcdsa) * 2, UNSIGNED, BE, 2);
        for signatureAlgorithm range serverSignatureSchemesEcdsa do
          certificateRequest &:= bytes(signatureAlgorithm, UNSIGNED, BE, 2);
        end for;
      else
        certificateRequest &:= bytes(length(serverSignatureSchemesRsa) * 2, UNSIGNED, BE, 2);
        for signatureAlgorithm range serverSignatureSchemesRsa do
          certificateRequest &:= bytes(signatureAlgorithm, UNSIGNED, BE, 2);
        end for;
      end if;
    end if;
    certificateRequest &:= "\0;\0;";                  # Bytes in certificate_authorities list
    length := length(certificateRequest);
    certificateRequest @:= [4] bytes(length - 5, UNSIGNED, BE, 2);
    certificateRequest @:= [8] bytes(length - 9, UNSIGNED, BE, 2);
    parameters.handshake_messages &:= certificateRequest[6 ..];
  end func;


const func string: genServerHelloDone (inout tlsParameters: parameters) is func
  result
    var string: serverHelloDone is "";
  local
    var integer: length is 0;
  begin
    serverHelloDone := str(HANDSHAKE) &          # ContentType (index: 1)
                       parameters.tls_version &  # Version: take version from client_hello.
                       "\0;\0;" &                # Length: filled later (index: 4)
                       str(SERVER_HELLO_DONE) &  # HandshakeType (index: 6)
                       "\0;\0;\0;";              # Length: 0
    length := length(serverHelloDone);
    serverHelloDone @:= [4] bytes(length - 5, UNSIGNED, BE, 2);
    parameters.handshake_messages &:= serverHelloDone[6 ..];
  end func;


const func string: genClientKeyExchange (inout tlsParameters: parameters) is func
  result
    var string: clientKeyExchange is "";
  local
    var integer: length is 0;
    var string: preMasterSecret is "";
    var string: encryptedPreMasterSecret is "";
    var string: pointData is "";
    var ecPoint: sharedSecretEcPoint is ecPoint.value;
  begin
    # writeln("genClientKeyExchange");
    clientKeyExchange := str(HANDSHAKE) &            # ContentType (index: 1)
                         parameters.tls_version &    # Version: 3.1
                         "\0;\0;" &                  # Length: filled later (index: 4)
                         str(CLIENT_KEY_EXCHANGE) &  # HandshakeType (index: 6)
                         "\0;\0;\0;";                # Length: filled later
    if parameters.key_exchange_algorithm = RSA then
      preMasterSecret :=
          parameters.tls_version &                                 # ProtocolVersion
          bytes(rand(0_, 2_ ** (46 * 8) - 1_), UNSIGNED, BE, 46);  # Random - random_bytes
      encryptedPreMasterSecret := rsaesPkcs1V15Encrypt(parameters.publicRsaCertificateKey,
          preMasterSecret);
      # writeln("encryptedPreMasterSecret: " <& hex(encryptedPreMasterSecret));
      # writeln("length(encryptedPreMasterSecret): " <& length(encryptedPreMasterSecret));
      if parameters.tls_version <> SSL_3_0 then
        clientKeyExchange &:= bytes(length(encryptedPreMasterSecret), UNSIGNED, BE, 2);
      end if;
      clientKeyExchange &:= encryptedPreMasterSecret;
    elsif parameters.key_exchange_algorithm = EC_DIFFIE_HELLMAN then
      parameters.ownEccKeyPair := genEccKeyPair(parameters.curve);
      pointData := ecPointEncode(parameters.curve, parameters.ownEccKeyPair.publicKey);
      clientKeyExchange &:= str(chr(length(pointData))) & pointData;
      sharedSecretEcPoint := multFast(parameters.curve, parameters.publicEccKeyOfServer,
                                      parameters.ownEccKeyPair.privateKey);
      # writeln("sharedSecretEcPoint.x: " <& sharedSecretEcPoint.x radix 16);
      # writeln("length: " <& getSizeInBytes(parameters.curve));
      preMasterSecret := bytes(sharedSecretEcPoint.x, UNSIGNED, BE,
                               getSizeInBytes(parameters.curve));
    end if;
    # writeln("preMasterSecret: " <& hex(preMasterSecret));
    computeMasterSecret(parameters, preMasterSecret);
    # writeln("master_secret: " <& hex(parameters.master_secret));
    storeKeys(parameters);
    length := length(clientKeyExchange);
    clientKeyExchange @:= [4] bytes(length - 5, UNSIGNED, BE, 2);
    clientKeyExchange @:= [8] bytes(length - 9, UNSIGNED, BE, 2);
    parameters.handshake_messages &:= clientKeyExchange[6 ..];
  end func;


const func string: genChangeCipherSpec (in tlsParameters: parameters) is func
  result
    var string: changeCipherSpec is "";
  local
    var integer: length is 0;
  begin
    changeCipherSpec := str(CHANGE_CIPHER_SPEC) &  # ContentType (index: 1)
                        parameters.tls_version &   # Version: 3.1
                        "\0;\0;" &                 # Length: filled later (index: 4)
                        "\1;";                     # change_cipher_spec
    length := length(changeCipherSpec);
    changeCipherSpec @:= [4] bytes(length - 5, UNSIGNED, BE, 2);
  end func;


const func string: genFinished (inout tlsParameters: parameters) is func
  result
    var string: finished is "";
  local
    var integer: length is 0;
    var string: finished_label is "";
    var string: verify_data is "";
  begin
    finished := str(HANDSHAKE) &          # ContentType (index: 1)
                parameters.tls_version &  # Version: 3.1
                "\0;\0;" &                # Length: filled later (index: 4)
                str(FINISHED) &           # HandshakeType (index: 6)
                "\0;\0;\0;";              # Length: filled later
    # writeln("master_secret: " <& hex(parameters.master_secret));
    # writeln("handshake_messages: " <& hex(parameters.handshake_messages));
    if parameters.tls_version = SSL_3_0 then
      if parameters.isClient then
        finished_label := "CLNT";
      else
        finished_label := "SRVR";
      end if;
      # writeln("finished_label: " <& literal(finished_label));
      verify_data := md5(parameters.master_secret & MD5_PAD2 &
                         md5(parameters.handshake_messages & finished_label &
                             parameters.master_secret & MD5_PAD1)) &
                     sha1(parameters.master_secret & SHA_PAD2 &
                          sha1(parameters.handshake_messages & finished_label &
                               parameters.master_secret & SHA_PAD1));
    else
      if parameters.isClient then
        finished_label := "client finished";
      else
        finished_label := "server finished";
      end if;
      # writeln("finished_label: " <& literal(finished_label));
      if parameters.tls_version >= TLS_1_2 then
        verify_data := p_hash(SHA256, parameters.master_secret, finished_label &
                              sha256(parameters.handshake_messages), 12);
      else
        verify_data := pseudoRandomFunction(parameters.master_secret, finished_label,
                                            md5(parameters.handshake_messages) &
                                            sha1(parameters.handshake_messages), 12);
      end if;
    end if;
    # writeln("verify_data: " <& hex(verify_data));
    finished &:= verify_data;
    length := length(finished);
    finished @:= [4] bytes(length - 5, UNSIGNED, BE, 2);
    finished @:= [8] bytes(length - 9, UNSIGNED, BE, 2);
    parameters.handshake_messages &:= finished[6 ..];
  end func;


const func string: genAlert (inout tlsParameters: parameters, in char: description) is func
  result
    var string: alert is "";
  local
    var integer: length is 0;
  begin
    alert := str(ALERT) &              # ContentType (index: 1)
             parameters.tls_version &  # Version: 3.1
             "\0;\0;" &                # Length: filled later (index: 4)
             "\1;" &                   # level: 1
             str(description);         # AlertDescription
    length := length(alert);
    alert @:= [4] bytes(length - 5, UNSIGNED, BE, 2);
  end func;


const func string: tlsEncryptRecord (inout tlsParameters: parameters, in string: plain) is func
  result
    var string: encrypted is "";
  local
    var string: content is "";
    var string: iv is "";
    var string: mac is "";
    var integer: padding_length is 0;
    var string: padding is "";
    var string: encoded is "";
    var integer: length is 0;
  begin
    # writeln("plain: " <& literal(plain));
    # writeln("length(plain): " <& length(plain));
    encrypted := plain[.. 3] &         # Head stays unchanged
                 "\0;\0;";             # Length: filled later (index: 4)
    # writeln("mac secret: " <& hex(parameters.writeMacSecret));
    if parameters.tls_version = SSL_3_0 then
      mac := msgDigest(parameters.mac_algorithm, parameters.writeMacSecret & SHA_PAD2 &
                       msgDigest(parameters.mac_algorithm, parameters.writeMacSecret & SHA_PAD1 &
                                 bytes(parameters.writeSequenceNumber, UNSIGNED, BE, 8) &
                                 plain[1 len 1] & plain[4 ..]));
    else
      # writeln("mac algorithm: " <& ord(parameters.mac_algorithm));
      # writeln("mac secret: " <& hex(parameters.writeMacSecret));
      # writeln("hmac in: " <& hex(bytes(parameters.writeSequenceNumber, UNSIGNED, BE, 8) & plain));
      mac := hmac(parameters.mac_algorithm, parameters.writeMacSecret,
                  bytes(parameters.writeSequenceNumber, UNSIGNED, BE, 8) & plain);
    end if;
    content := plain[6 ..];
    if parameters.block_size <> 0 then
      if parameters.tls_version >= TLS_1_1 then
        iv := bytes(rand(0_, 2_ ** (parameters.block_size * 8) - 1_), UNSIGNED, BE,
                    parameters.block_size);
      end if;
      padding_length := parameters.block_size - 1 -
                        (length(content) + length(mac)) mod parameters.block_size;
      # writeln("padding_length: " <& padding_length);
      padding := str(chr(padding_length)) mult succ(padding_length);
    end if;
    # writeln("bulk_cipher_algorithm: " <& ord(parameters.bulk_cipher_algorithm));
    # writeln("data: " <& hex(content));
    # writeln("mac: " <& hex(mac));
    # writeln("before encode: " <& hex(iv & content & mac & padding));
    initAead(parameters.writeCipherState, plain[.. 3], parameters.writeSequenceNumber);
    encoded := encode(parameters.writeCipherState, iv & content & mac & padding);
    # writeln("encoded: " <& literal(encoded));
    # writeln("length(encoded): " <& length(encoded));
    encrypted &:= encoded;
    length := length(encrypted);
    encrypted @:= [4] bytes(length - 5, UNSIGNED, BE, 2);
    # writeln("encrypted message: " <& hex(encrypted));
    # writeln("length: " <& length(encrypted));
    incr(parameters.writeSequenceNumber);
  end func;


const func boolean: tlsDecryptRecord (inout tlsParameters: parameters, inout tlsParseState: state) is func
  result
    var boolean: decryptOkay is TRUE;
  local
    var string: version is "";
    var string: decoded is "";
    var integer: padding_length is 0;
    var string: content is "";
    var string: mac is "";
    var string: verify is "";
    var string: plain is "";
  begin
    # writeln("tlsDecryptRecord");
    version := state.message[2 len 2];
    # writeln("Version: " <& ord(version[1]) <& "." <& ord(version[2]));
    # writeln("message: " <& literal(state.message));
    initAead(parameters.readCipherState, state.message[.. 3], parameters.readSequenceNumber);
    decoded := decode(parameters.readCipherState, state.message[state.pos len state.length]);
    if parameters.block_size <> 0 then
      padding_length := ord(decoded[length(decoded)]);
      if padding_length < length(decoded) and
          decoded[length(decoded) - padding_length ..] =
          str(chr(padding_length)) mult succ(padding_length) then
        decoded := decoded[.. length(decoded) - succ(padding_length)];
        if version >= TLS_1_1 then
          # writeln("iv: " <& hex(decoded[.. parameters.block_size]));
          decoded := decoded[succ(parameters.block_size) ..]; # Remove iv
        end if;
      else
        decryptOkay := FALSE;
        state.alert := DECRYPTION_FAILED;
      end if;
    end if;
    if decryptOkay then
      content := decoded[.. length(decoded) - digestSize(parameters.mac_algorithm)];
      mac := decoded[length(decoded) - digestSize(parameters.mac_algorithm) + 1 ..];
      plain := state.message[.. 3] &
               bytes(length(content), UNSIGNED, BE, 2) &
               content;
      # writeln("plain: " <& hex(plain));
      # writeln("mac: " <& hex(mac));
      if parameters.bulk_cipher_algorithm = AES_GCM then
        mac := getMac(parameters.readCipherState);
        verify := getComputedMac(parameters.readCipherState);
      else
        if version = SSL_3_0 then
          verify := msgDigest(parameters.mac_algorithm, parameters.readMacSecret & SHA_PAD2 &
                              msgDigest(parameters.mac_algorithm, parameters.readMacSecret & SHA_PAD1 &
                                        bytes(parameters.readSequenceNumber, UNSIGNED, BE, 8) &
                                        plain[1 len 1] & plain[4 ..]));
        else
          verify := hmac(parameters.mac_algorithm, parameters.readMacSecret,
                         bytes(parameters.readSequenceNumber, UNSIGNED, BE, 8) & plain);
        end if;
      end if;
      # writeln("verify: " <& hex(verify));
      if mac = verify then
        state.length := length(content);
        state.message := plain;
      else
        decryptOkay := FALSE;
        state.alert := BAD_RECORD_MAC;
      end if;
    end if;
    incr(parameters.readSequenceNumber);
  end func;


const proc: sendAlertAndClose (inout tlsFile: aFile, in char: alertDescription) is func
  local
    var string: alert is "";
  begin
    alert := genAlert(aFile.parameters, alertDescription);
    # showTlsMsg(alert);
    if aFile.parameters.writeEncryptedRecords then
      alert := tlsEncryptRecord(aFile.parameters, alert);
    end if;
    block
      write(aFile.sock, alert);
    exception
      catch FILE_ERROR: noop;
    end block;
    close(aFile.sock);
    aFile.sock := STD_NULL;
    aFile.parseState.pos := succ(length(aFile.parseState.message));
  end func;


const proc: updateClientCache (in tlsParameters: parameters, in socketAddress: address) is func
  local
    var clientSession: session is clientSession.value;
  begin
    if parameters.session_id <> "" then
      session.session_id            := parameters.session_id;
      session.bulk_cipher_algorithm := parameters.bulk_cipher_algorithm;
      session.master_secret         := parameters.master_secret;
      session.last_use              := time(NOW);
      clientSessionCache @:= [address] session;
    end if;
  end func;


const func file: negotiateSecurityParameters (inout tlsFile: new_file) is func
  result
    var file: tlsSock is STD_NULL;
  local
    var string: clientKeyExchange is "";
    var string: changeCipherSpec is "";
    var string: finished is "";
    var boolean: serverHelloDone is FALSE;
    var boolean: unexpectedMessage is FALSE;
  begin
    repeat
      getTlsMsgRecord(new_file.sock, new_file.parseState);
      # showTlsMsg(new_file.parseState.message);
      if new_file.parseState.contentType = HANDSHAKE then
        loadCompleteHandshakeMsg(new_file.sock, new_file.parseState);
        if new_file.parseState.alert = CLOSE_NOTIFY then
          # showHandshakeMsg(new_file.parseState.message, new_file.parseState.pos);
          if new_file.parseState.message[new_file.parseState.pos] = CERTIFICATE then
            processCertificate(new_file.parameters, new_file.parseState);
          elsif new_file.parseState.message[new_file.parseState.pos] = SERVER_KEY_EXCHANGE then
            processServerKeyExchange(new_file.parameters, new_file.parseState);
          elsif new_file.parseState.message[new_file.parseState.pos] = CERTIFICATE_REQUEST then
            processCertificateRequest(new_file.parameters, new_file.parseState);
          elsif new_file.parseState.message[new_file.parseState.pos] = SERVER_HELLO_DONE then
            processServerHelloDone(new_file.parameters, new_file.parseState);
            serverHelloDone := TRUE;
          else  # Any other handshake
            unexpectedMessage := TRUE;
          end if;
        else
          unexpectedMessage := TRUE;
        end if;
      else
        unexpectedMessage := TRUE;
      end if;
    until serverHelloDone or unexpectedMessage;
    if serverHelloDone then
      clientKeyExchange := genClientKeyExchange(new_file.parameters);
      # showTlsMsg(clientKeyExchange);
      write(new_file.sock, clientKeyExchange);
      changeCipherSpec := genChangeCipherSpec(new_file.parameters);
      # showTlsMsg(changeCipherSpec);
      write(new_file.sock, changeCipherSpec);
      new_file.parameters.writeEncryptedRecords := TRUE;
      finished := genFinished(new_file.parameters);
      # showTlsMsg(finished);
      finished := tlsEncryptRecord(new_file.parameters, finished);
      write(new_file.sock, finished);
      repeat
        getTlsMsgRecord(new_file.sock, new_file.parseState);
        # writeln(literal(new_file.parseState.message));
        # showTlsMsg(new_file.parseState.message);
      until new_file.parseState.contentType = CHANGE_CIPHER_SPEC or
            new_file.parseState.contentType = ALERT or
            new_file.parseState.contentType = NO_MESSAGE;
      if new_file.parseState.contentType = CHANGE_CIPHER_SPEC then
        processChangeCipherSpec(new_file.parameters, new_file.parseState);
        getTlsMsgRecord(new_file.sock, new_file.parseState);
        if new_file.parseState.contentType = HANDSHAKE then  # Handshake with encoded Finished message
          if tlsDecryptRecord(new_file.parameters, new_file.parseState) then
            # showTlsMsg(new_file.parseState.message);
            if new_file.parseState.message[new_file.parseState.pos] = FINISHED then
              processFinished(new_file.parameters, new_file.parseState);
              # writeln("Version: " <& ord(new_file.parameters.tls_version[1]) <& "." <& ord(new_file.parameters.tls_version[2]));
              # writeln("Cipher: " <& ord(new_file.parameters.cipher_suite));
              updateClientCache(new_file.parameters, peerAddress(new_file.sock));
              tlsSock := toInterface(new_file);
            else
              sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
            end if;
          else
            sendAlertAndClose(new_file, new_file.parseState.alert);
          end if;
        else
          sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
        end if;
      else
        sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
      end if;
    else
      if new_file.parseState.alert = CLOSE_NOTIFY then
        sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
      else
        sendAlertAndClose(new_file, new_file.parseState.alert);
      end if;
    end if;
  end func;


const func file: openNewTlsSocket (inout file: sock, in string: hostName) is func
  result
    var file: tlsSock is STD_NULL;
  local
    var tlsFile: new_file is tlsFile.value;
    var string: clientHello is "";
  begin
    new_file.sock := sock;
    new_file.parameters.isClient := TRUE;
    new_file.parameters.hostName := hostName;
    clientHello := genClientHello(new_file.parameters, "");
    # showTlsMsg(clientHello);
    write(sock, clientHello);
    getTlsMsgRecord(sock, new_file.parseState);
    # showTlsMsg(new_file.parseState.message);
    if new_file.parseState.contentType = HANDSHAKE and
        new_file.parseState.message[new_file.parseState.pos] = SERVER_HELLO then
      processServerHello(new_file.parameters, new_file.parseState);
      if new_file.parseState.alert <> CLOSE_NOTIFY then
        sendAlertAndClose(new_file, new_file.parseState.alert);
      else
        tlsSock := negotiateSecurityParameters(new_file);
      end if;
    else
      sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
    end if;
  end func;


const func file: openTlsSocket (inout file: sock, in clientSession: session,
    in string: hostName) is func
  result
    var file: tlsSock is STD_NULL;
  local
    var tlsFile: new_file is tlsFile.value;
    var socketAddress: peerAddress is socketAddress.value;
    var string: sessionId is "";
    var string: clientHello is "";
    var string: changeCipherSpec is "";
    var string: finished is "";
  begin
    if sock <> STD_NULL then
      peerAddress := peerAddress(sock);
      new_file.sock := sock;
      new_file.parameters.isClient := TRUE;
      new_file.parameters.hostName := hostName;
      if session.last_use + clientCacheValid > time(NOW) then
        sessionId := session.session_id;
      end if;
      clientHello := genClientHello(new_file.parameters, sessionId);
      # showTlsMsg(clientHello);
      write(sock, clientHello);
      getTlsMsgRecord(sock, new_file.parseState);
      if new_file.parseState.contentType = HANDSHAKE and
          new_file.parseState.message[new_file.parseState.pos] = SERVER_HELLO then
        # showTlsMsg(new_file.parseState.message);
        processServerHello(new_file.parameters, new_file.parseState);
        if new_file.parseState.alert <> CLOSE_NOTIFY then
          sendAlertAndClose(new_file, new_file.parseState.alert);
        elsif new_file.parameters.session_id <> sessionId or
            new_file.parameters.bulk_cipher_algorithm <> session.bulk_cipher_algorithm then
          tlsSock := negotiateSecurityParameters(new_file);
        else
          getTlsMsgRecord(new_file.sock, new_file.parseState);
          # showTlsMsg(new_file.parseState.message);
          if new_file.parseState.contentType = CHANGE_CIPHER_SPEC then
            processChangeCipherSpec(new_file.parameters, new_file.parseState);
            new_file.parameters.master_secret := session.master_secret;
            storeKeys(new_file.parameters);
            getTlsMsgRecord(new_file.sock, new_file.parseState);
            if new_file.parseState.contentType = HANDSHAKE then  # Handshake with encoded Finished message
              if tlsDecryptRecord(new_file.parameters, new_file.parseState) then
                # showTlsMsg(new_file.parseState.message);
                if new_file.parseState.message[new_file.parseState.pos] = FINISHED then
                  processFinished(new_file.parameters, new_file.parseState);
                  changeCipherSpec := genChangeCipherSpec(new_file.parameters);
                  # showTlsMsg(changeCipherSpec);
                  write(new_file.sock, changeCipherSpec);
                  new_file.parameters.writeEncryptedRecords := TRUE;
                  finished := genFinished(new_file.parameters);
                  # showTlsMsg(finished);
                  finished := tlsEncryptRecord(new_file.parameters, finished);
                  write(new_file.sock, finished);
                  updateClientCache(new_file.parameters, peerAddress);
                  tlsSock := toInterface(new_file);
                else
                  sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
                end if;
              else
                sendAlertAndClose(new_file, new_file.parseState.alert);
              end if;
            else
              sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
            end if;
          else
            sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
          end if;
        end if;
      else
        sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
      end if;
      if tlsSock = STD_NULL then
        excl(clientSessionCache, peerAddress);
        sock := openSocket(peerAddress);
        tlsSock := openNewTlsSocket(sock, hostName);
      end if;
    end if;
  end func;


(**
 *  Return a connected TLS socket file based on the given ''sock''.
 *  @param sock A connected internet socket file (client side).
 *  @param hostName The server host name.
 *  @return an open TLS socket file, or [[null_file#STD_NULL|STD_NULL]]
 *          if it could not be opened.
 *  @exception MEMORY_ERROR An out of memory situation occurred.
 *)
const func file: openTlsSocket (inout file: sock, in string: hostName) is func
  result
    var file: tlsSock is STD_NULL;
  begin
    if sock <> STD_NULL then
      if peerAddress(sock) in clientSessionCache then
        tlsSock := openTlsSocket(sock, clientSessionCache[peerAddress(sock)],
                                 hostName);
      else
        tlsSock := openNewTlsSocket(sock, hostName);
      end if;
    end if;
  end func;


(**
 *  Return a connected TLS socket file based on the given ''sock''.
 *  @param sock A connected internet socket file (client side).
 *  @return an open TLS socket file, or [[null_file#STD_NULL|STD_NULL]]
 *          if it could not be opened.
 *  @exception MEMORY_ERROR An out of memory situation occurred.
 *)
const func file: openTlsSocket (inout file: sock) is
  return openTlsSocket (sock, "");


(**
 *  Return a connected TLS socket file at a port at ''hostName''.
 *  Here ''hostName'' is either a host name (e.g.: "www.example.org"),
 *  or an IPv4 address in standard dot notation (e.g.: "192.0.2.235").
 *  Operating systems supporting IPv6 may also accept an IPv6 address
 *  in colon notation.
 *  @return an open TLS socket file, or [[null_file#STD_NULL|STD_NULL]]
 *          if it could not be opened.
 *  @exception MEMORY_ERROR An out of memory situation occurred.
 *)
const func file: openTlsSocket (in string: hostName, in integer: portNumber) is func
  result
    var file: tlsSock is STD_NULL;
  local
    var file: sock is STD_NULL;
  begin
    sock := openInetSocket(hostName, portNumber);
    tlsSock := openTlsSocket(sock, hostName);
  end func;


(**
 *  Return a connected TLS socket file based on the given ''sock''.
 *  @param sock A connected internet socket file (server side).
 *  @param certificateAndKey Server certificate and corresponding private key.
 *  @return an open TLS socket file, or [[null_file#STD_NULL|STD_NULL]]
 *          if it could not be opened.
 *  @exception MEMORY_ERROR An out of memory situation occurred.
 *)
const func file: openServerTls (inout file: sock, in certAndKey: certificateAndKey) is func
  result
    var file: tlsSock is STD_NULL;
  local
    var tlsFile: new_file is tlsFile.value;
    var string: clientHello is "";
    var string: serverHello is "";
    var string: certificate is "";
    var string: serverKeyExchange is "";
    var string: certificateRequest is "";
    var string: serverHelloDone is "";
    var string: changeCipherSpec is "";
    var string: finished is "";
    var boolean: okay is TRUE;
  begin
    if sock <> STD_NULL then
      new_file.sock := sock;
      new_file.parameters.isClient := FALSE;
      new_file.parameters.privateRsaCertificateKey := certificateAndKey.privateRsaKey;
      new_file.parameters.privateEccCertificateKey := certificateAndKey.privateEccKey;
      # Read and process the request from sock.
      getTlsMsgRecord(sock, new_file.parseState);
      if new_file.parseState.contentType = HANDSHAKE and
          new_file.parseState.message[new_file.parseState.pos] = CLIENT_HELLO then
        # writeln(literal(new_file.parseState.message));
        # showTlsMsg(new_file.parseState.message);
        processClientHello(new_file.parameters, new_file.parseState);
        if new_file.parseState.alert <> CLOSE_NOTIFY then
          sendAlertAndClose(new_file, new_file.parseState.alert);
          okay := FALSE;
        else
          serverHello := genServerHello(new_file.parameters);
          # showTlsMsg(serverHello);
          write(sock, serverHello);
          certificate := genCertificate(new_file.parameters, certificateAndKey.certList);
          # showTlsMsg(certificate);
          block
            write(sock, certificate);
          exception
            catch FILE_ERROR:
              # getTlsMsgRecord(sock, new_file.parseState);
              # showTlsMsg(new_file.parseState.message);
              okay := FALSE;
          end block;
          if okay and new_file.parameters.key_exchange_algorithm = EC_DIFFIE_HELLMAN then
            serverKeyExchange := genServerKeyExchange(new_file.parameters);
            # showTlsMsg(serverKeyExchange);
            write(sock, serverKeyExchange);
          end if;
          # certificateRequest := genCertificateRequest(new_file.parameters);
          # showTlsMsg(certificateRequest);
          # write(sock, certificateRequest);
        end if;
        if okay then
          serverHelloDone := genServerHelloDone(new_file.parameters);
          # showTlsMsg(serverHelloDone);
          write(sock, serverHelloDone);
          repeat
            getTlsMsgRecord(sock, new_file.parseState);
            # showTlsMsg(new_file.parseState.message);
            if new_file.parseState.contentType = HANDSHAKE then
              if new_file.parseState.message[new_file.parseState.pos] = CLIENT_KEY_EXCHANGE then
                processClientKeyExchange(new_file.parameters, new_file.parseState);
              elsif new_file.parseState.message[new_file.parseState.pos] = CERTIFICATE then
                processClientCertificate(new_file.parameters, new_file.parseState);
              elsif new_file.parseState.message[new_file.parseState.pos] = CERTIFICATE_VERIFY then
                processCertificateVerify(new_file.parameters, new_file.parseState);
              end if;
            end if;
          until new_file.parseState.contentType = CHANGE_CIPHER_SPEC or
                new_file.parseState.contentType = ALERT or
                new_file.parseState.contentType = NO_MESSAGE;
          if new_file.parseState.contentType = CHANGE_CIPHER_SPEC then
            processChangeCipherSpec(new_file.parameters, new_file.parseState);
            getTlsMsgRecord(sock, new_file.parseState);
            if new_file.parseState.contentType = HANDSHAKE then  # Handshake with encoded Finished message
              if tlsDecryptRecord(new_file.parameters, new_file.parseState) then
                # showTlsMsg(new_file.parseState.message);
                if new_file.parseState.message[new_file.parseState.pos] = FINISHED then
                  processFinished(new_file.parameters, new_file.parseState);
                  changeCipherSpec := genChangeCipherSpec(new_file.parameters);
                  # showTlsMsg(changeCipherSpec);
                  write(sock, changeCipherSpec);
                  new_file.parameters.writeEncryptedRecords := TRUE;
                  finished := genFinished(new_file.parameters);
                  # showTlsMsg(finished);
                  finished := tlsEncryptRecord(new_file.parameters, finished);
                  block
                    write(sock, finished);
                  exception
                    catch FILE_ERROR:
                      # getTlsMsgRecord(sock, new_file.parseState);
                      # tlsDecryptRecord(new_file.parameters, new_file.parseState);
                      # showTlsMsg(new_file.parseState.message);
                      okay := FALSE;
                  end block;
                  if okay then
                    tlsSock := toInterface(new_file);
                  end if;
                else
                  sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
                end if;
              else
                sendAlertAndClose(new_file, new_file.parseState.alert);
              end if;
            else
              sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
            end if;
          else
            sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
          end if;
        end if;
      else
        sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
      end if;
    end if;
  end func;


(**
 *  Close a tlsFile. This closes also the socket below.
 *  @exception FILE_ERROR A system function returns an error.
 *)
const proc: close (inout tlsFile: aFile) is func
  begin
    sendAlertAndClose(aFile, CLOSE_NOTIFY);
  end func;


(**
 *  Determine the end-of-file indicator.
 *  The end-of-file indicator is set if at least one request to read
 *  from the socket failed. The socket functions ''getc'', ''gets'',
 *  ''getln'' and ''getwd'' indicate the end-of-file situation by
 *  setting ''bufferChar'' to [[char#EOF|EOF]].
 *  @return TRUE if the end-of-file indicator is set, FALSE otherwise.
 *)
const func boolean: eof (in tlsFile: inFile) is
  return inFile.bufferChar = EOF;


const func string: getApplicationData (inout tlsFile: inFile) is func
  result
    var string: applicationData is "";
  begin
    getTlsMsgRecord(inFile.sock, inFile.parseState);
    if inFile.parseState.contentType = APPLICATION_DATA then
      if tlsDecryptRecord(inFile.parameters, inFile.parseState) then
        # showTlsMsg(inFile.parseState.message);
        applicationData := inFile.parseState.message[inFile.parseState.pos ..];
        inFile.parseState.pos +:= inFile.parseState.length;
      else
        sendAlertAndClose(inFile, inFile.parseState.alert);
      end if;
    elsif inFile.parseState.contentType = ALERT then
      if tlsDecryptRecord(inFile.parameters, inFile.parseState) then
        # showTlsMsg(inFile.parseState.message);
        close(inFile);
      else
        sendAlertAndClose(inFile, inFile.parseState.alert);
      end if;
    elsif inFile.parseState.contentType = CLIENT_HELLO then
      sendAlertAndClose(inFile, NO_RENEGOTIATION);
    elsif inFile.parseState.contentType = NO_MESSAGE then
      close(inFile);
    else
      sendAlertAndClose(inFile, UNEXPECTED_MESSAGE);
    end if;
  end func;


(**
 *  Write a [[string]] to a tlsFile.
 *  @exception FILE_ERROR A system function returns an error.
 *  @exception RANGE_ERROR The string contains a character that does
 *             not fit into a byte.
 *)
const proc: write (inout tlsFile: outFile, in string: stri) is func
  local
    const integer: maxStriLen is 2**14 - 1;
    var integer: startIndex is 1;
    var string: plain is "";
    var string: message is "";
  begin
    # writeln("write(" <& literal(stri) <& ")");
    repeat
      plain := str(APPLICATION_DATA) &           # ContentType (index: 1)
               outFile.parameters.tls_version &  # Version: 3.1
               "\0;\0;" &                        # Length: filled later (index: 4)
               stri[startIndex len maxStriLen];
      plain @:= [4] bytes(length(plain) - 5, UNSIGNED, BE, 2);
      # showTlsMsg(plain);
      message := tlsEncryptRecord(outFile.parameters, plain);
      write(outFile.sock, message);
      startIndex +:= maxStriLen;
    until startIndex > length(stri);
  end func;


(**
 *  Write a [[string]] followed by end-of-line to ''outSocket''.
 *  This function assures that string and '\n' are sent together.
 *)
const proc: writeln (inout tlsFile: outFile, in string: stri) is func
  begin
    # writeln("writeln(" <& literal(stri) <& ")");
    write(outFile, stri & "\n");
  end func;


(**
 *  Read a [[string]] with a maximum length from a tlsFile.
 *  @return the string read.
 *  @exception RANGE_ERROR The parameter ''maxLength'' is negative.
 *  @exception MEMORY_ERROR Not enough memory to represent the result.
 *)
const func string: gets (inout tlsFile: inFile, in integer: maxLength) is func
  result
    var string: striRead is "";
  begin
    if maxLength <= 0 then
      if maxLength <> 0 then
        raise RANGE_ERROR;
      end if;
    else
      # writeln("gets(, " <& maxLength <& ") actual length: " <& length(inFile.readBuffer));
      if inFile.readBuffer = "" and not eof(inFile.sock) then
        inFile.readBuffer := getApplicationData(inFile);
        # writeln("gets(, " <& maxLength <& ") actual length: " <& length(inFile.readBuffer));
      end if;
      if length(inFile.readBuffer) > maxLength then
        striRead := inFile.readBuffer[.. maxLength];
        inFile.readBuffer := inFile.readBuffer[succ(maxLength) ..];
      else
        striRead := inFile.readBuffer;
        inFile.readBuffer := "";
      end if;
      if striRead = "" and eof(inFile.sock) then
        inFile.bufferChar := EOF;
      end if;
    end if;
    # writeln("gets --> " <& literal(striRead));
  end func;


(**
 *  Read a line from a tlsFile.
 *  The function accepts lines ending with '\n', "\r\n" or [[char#EOF|EOF]].
 *  The line ending characters are not copied into the string.
 *  That means that the '\r' of a "\r\n" sequence is silently removed.
 *  When the function is left inFile.bufferChar contains '\n' or
 *  [[char#EOF|EOF]].
 *  @return the line read.
 *  @exception MEMORY_ERROR Not enough memory to represent the result.
 *)
const func string: getln (inout tlsFile: inFile) is func
  result
    var string: stri is "";
  local
    var integer: nlPos is 0;
  begin
    nlPos := pos(inFile.readBuffer, '\n');
    while nlPos = 0 and not eof(inFile.sock) do
      inFile.readBuffer &:= getApplicationData(inFile);
      nlPos := pos(inFile.readBuffer, '\n');
    end while;
    if nlPos <> 0 then
      if nlPos <> 1 and inFile.readBuffer[pred(nlPos)] = '\r' then
        stri := inFile.readBuffer[.. nlPos - 2];
      else
        stri := inFile.readBuffer[.. pred(nlPos)];
      end if;
      inFile.readBuffer := inFile.readBuffer[succ(nlPos) ..];
      inFile.bufferChar := '\n';
    else
      stri := inFile.readBuffer;
      inFile.readBuffer := "";
      inFile.bufferChar := EOF;
    end if;
    # writeln("getln --> " <& literal(stri));
  end func;


const func string: getServerCertificate (in file: aFile, in integer: pos) is DYNAMIC;


const func string: getServerCertificate (in tlsFile: aFile, in integer: pos) is
  return aFile.parameters.serverCertificates.certList[pos];