"Fossies" - the Fresh Open Source Software Archive

Member "seed7/lib/tls.s7i" (2 Aug 2020, 90318 Bytes) of package /linux/misc/seed7_05_20210223.tgz:


As a special service "Fossies" has tried to format the requested text file into HTML format (style: standard) with prefixed line numbers. Alternatively you can here view or download the uninterpreted source code file. See also the last Fossies "Diffs" side-by-side code changes report for "tls.s7i": 05_20200727_vs_05_20200830.

    1 
    2 (********************************************************************)
    3 (*                                                                  *)
    4 (*  tls.s7i       Support for Transport Layer Security (TLS/SSL).   *)
    5 (*  Copyright (C) 2013 - 2019  Thomas Mertes                        *)
    6 (*                                                                  *)
    7 (*  This file is part of the Seed7 Runtime Library.                 *)
    8 (*                                                                  *)
    9 (*  The Seed7 Runtime Library is free software; you can             *)
   10 (*  redistribute it and/or modify it under the terms of the GNU     *)
   11 (*  Lesser General Public License as published by the Free Software *)
   12 (*  Foundation; either version 2.1 of the License, or (at your      *)
   13 (*  option) any later version.                                      *)
   14 (*                                                                  *)
   15 (*  The Seed7 Runtime Library is distributed in the hope that it    *)
   16 (*  will be useful, but WITHOUT ANY WARRANTY; without even the      *)
   17 (*  implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR *)
   18 (*  PURPOSE.  See the GNU Lesser General Public License for more    *)
   19 (*  details.                                                        *)
   20 (*                                                                  *)
   21 (*  You should have received a copy of the GNU Lesser General       *)
   22 (*  Public License along with this program; if not, write to the    *)
   23 (*  Free Software Foundation, Inc., 51 Franklin Street,             *)
   24 (*  Fifth Floor, Boston, MA  02110-1301, USA.                       *)
   25 (*                                                                  *)
   26 (********************************************************************)
   27 
   28 
   29 include "socket.s7i";
   30 include "asn1.s7i";
   31 include "x509cert.s7i";
   32 include "hmac.s7i";
   33 include "elliptic.s7i";
   34 include "cipher.s7i";
   35 include "arc4.s7i";
   36 include "des.s7i";
   37 include "tdes.s7i";
   38 include "aes.s7i";
   39 
   40 
   41 const type: cipherSuite is integer;
   42 
   43 const cipherSuite: TLS_NULL_WITH_NULL_NULL               is 16#0000;
   44 const cipherSuite: TLS_RSA_WITH_RC4_128_MD5              is 16#0004;
   45 const cipherSuite: TLS_RSA_WITH_RC4_128_SHA              is 16#0005;
   46 const cipherSuite: TLS_RSA_WITH_DES_CBC_SHA              is 16#0009;
   47 const cipherSuite: TLS_RSA_WITH_3DES_EDE_CBC_SHA         is 16#000a; # Mandatory TLS 1.1 Cipher
   48 const cipherSuite: TLS_RSA_WITH_AES_128_CBC_SHA          is 16#002f; # Mandatory TLS 1.2 Cipher
   49 const cipherSuite: TLS_RSA_WITH_AES_256_CBC_SHA          is 16#0035;
   50 const cipherSuite: TLS_RSA_WITH_AES_128_CBC_SHA256       is 16#003c;
   51 const cipherSuite: TLS_RSA_WITH_AES_256_CBC_SHA256       is 16#003d;
   52 const cipherSuite: TLS_ECDHE_ECDSA_WITH_AES_128_CBC_SHA  is 16#c009;
   53 const cipherSuite: TLS_ECDHE_ECDSA_WITH_AES_256_CBC_SHA  is 16#c00a;
   54 const cipherSuite: TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA    is 16#c013;
   55 const cipherSuite: TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 is 16#c02f;
   56 const cipherSuite: TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 is 16#c030;
   57 
   58 const array cipherSuite: supportedCiphers is [] (
   59     TLS_RSA_WITH_3DES_EDE_CBC_SHA,
   60     TLS_RSA_WITH_RC4_128_SHA,
   61     TLS_RSA_WITH_RC4_128_MD5,
   62     TLS_RSA_WITH_DES_CBC_SHA,
   63     TLS_RSA_WITH_AES_128_CBC_SHA,
   64     TLS_RSA_WITH_AES_256_CBC_SHA,
   65     TLS_RSA_WITH_AES_128_CBC_SHA256,
   66     TLS_RSA_WITH_AES_256_CBC_SHA256,
   67     TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA,
   68     TLS_ECDHE_ECDSA_WITH_AES_128_CBC_SHA
   69   );
   70 
   71 const string: SSL_3_0 is "\3;\0;";
   72 const string: TLS_1_0 is "\3;\1;";
   73 const string: TLS_1_1 is "\3;\2;";
   74 const string: TLS_1_2 is "\3;\3;";
   75 
   76 const type: keyExchangeAlgorithm is new enum
   77     RSA, EC_DIFFIE_HELLMAN
   78   end enum;
   79 
   80 const type: tlsParameters is new struct
   81     var boolean:              isClient                 is TRUE;
   82     var string:               session_id               is "";
   83     var string:               hostName                 is "";
   84     var cipherSuite:          cipher_suite             is TLS_NULL_WITH_NULL_NULL;
   85     var keyExchangeAlgorithm: key_exchange_algorithm   is RSA;
   86     var cipherAlgorithm:      bulk_cipher_algorithm    is NO_CIPHER;
   87     var boolean:              block_cipher             is FALSE;
   88     var integer:              key_size                 is 0;
   89     var integer:              key_material_length      is 0;
   90     var integer:              block_size               is 0;
   91     var boolean:              is_exportable            is FALSE;
   92     var digestAlgorithm:      mac_algorithm            is NO_DIGEST;
   93     var integer:              hash_size                is 0;
   94     var integer:              compression_algorithm    is 0;
   95     var string:               tls_version              is TLS_1_2;  # TLS_1_1;
   96     var string:               master_secret            is ""; # length: 48
   97     var string:               client_random            is ""; # length: 32
   98     var string:               server_random            is ""; # length: 32
   99     var certAndKey:           serverCertificates       is certAndKey.value;
  100     var rsaKey:               publicRsaCertificateKey  is rsaKey.value;
  101     var rsaKey:               privateRsaCertificateKey is rsaKey.value;
  102     var ecPoint:              publicEccCertificateKey  is ecPoint.value;
  103     var bigInteger:           privateEccCertificateKey is 0_;
  104     var ellipticCurve:        curve                    is ellipticCurve.value;
  105     var integer:              signatureScheme          is 0;
  106     var eccKeyPair:           ownEccKeyPair            is eccKeyPair.value;
  107     var ecPoint:              publicEccKeyOfSever      is ecPoint.value;
  108     var string:               readMacSecret            is "";
  109     var string:               writeMacSecret           is "";
  110     var cipherState:          readCipherState          is cipherState.value;
  111     var cipherState:          writeCipherState         is cipherState.value;
  112     var integer:              readSequenceNumber       is 0;
  113     var integer:              writeSequenceNumber      is 0;
  114     var boolean:              writeEncryptedRecords    is FALSE;
  115     var string:               handshake_messages       is "";
  116   end struct;
  117 
  118 const char: NO_MESSAGE         is EOF;
  119 const char: CHANGE_CIPHER_SPEC is '\20;';
  120 const char: ALERT              is '\21;';
  121 const char: HANDSHAKE          is '\22;';
  122 const char: APPLICATION_DATA   is '\23;';
  123 
  124 const char: CLIENT_HELLO        is '\1;';
  125 const char: SERVER_HELLO        is '\2;';
  126 const char: SESSION_TICKET      is '\4;';
  127 const char: CERTIFICATE         is '\11;';
  128 const char: SERVER_KEY_EXCHANGE is '\12;';
  129 const char: CERTIFICATE_REQUEST is '\13;';
  130 const char: SERVER_HELLO_DONE   is '\14;';
  131 const char: CERTIFICATE_VERIFY  is '\15;';
  132 const char: CLIENT_KEY_EXCHANGE is '\16;';
  133 const char: FINISHED            is '\20;';
  134 
  135 const char: CLOSE_NOTIFY        is '\0;';
  136 const char: UNEXPECTED_MESSAGE  is '\10;';
  137 const char: BAD_RECORD_MAC      is '\20;';
  138 const char: DECRYPTION_FAILED   is '\21;';
  139 const char: HANDSHAKE_FAILURE   is '\40;';
  140 const char: ILLEGAL_PARAMETER   is '\47;';
  141 const char: PROCOCOL_VERSION    is '\70;';
  142 const char: NO_RENEGOTIATION    is '\100;';
  143 
  144 # Extensions:
  145 const integer: SERVER_NAME                            is     0;  # RFC6066
  146 const integer: MAX_FRAGMENT_LENGTH                    is     1;  # RFC6066
  147 const integer: CLIENT_CERTIFICATE_URL                 is     2;  # RFC6066
  148 const integer: TRUSTED_CA_KEYS                        is     3;  # RFC6066
  149 const integer: TRUNCATED_HMAC                         is     4;  # RFC6066
  150 const integer: STATUS_REQUEST                         is     5;  # RFC6066
  151 const integer: USER_MAPPING                           is     6;  # RFC4681
  152 const integer: CLIENT_AUTHZ                           is     7;  # RFC5878
  153 const integer: SERVER_AUTHZ                           is     8;  # RFC5878
  154 const integer: CERT_TYPE                              is     9;  # RFC6091
  155 const integer: ELLIPTIC_CURVES                        is    10;  # RFC4492
  156 const integer: EC_POINT_FORMATS                       is    11;  # RFC4492
  157 const integer: SRP                                    is    12;  # RFC5054
  158 const integer: SIGNATURE_ALGORITHMS                   is    13;  # RFC5246
  159 const integer: USE_SRTP                               is    14;  # RFC5764
  160 const integer: HEARTBEAT                              is    15;  # RFC6520
  161 const integer: APPLICATION_LAYER_PROTOCOL_NEGOTIATION is    16;  # RFC7301
  162 const integer: STATUS_REQUEST_V2                      is    17;  # RFC6961
  163 const integer: SIGNED_CERTIFICATE_TIMESTAMP           is    18;  # RFC6962
  164 const integer: CLIENT_CERTIFICATE_TYPE                is    19;  # RFC7250
  165 const integer: SERVER_CERTIFICATE_TYPE                is    20;  # RFC7250
  166 const integer: PADDING                                is    21;  # RFC7685
  167 const integer: ENCRYPT_THEN_MAC                       is    22;  # RFC7366
  168 const integer: EXTENDED_MASTER_SECRET                 is    23;  # RFC7627
  169 const integer: TOKEN_BINDING                          is    24;  # RFC8472
  170 const integer: CACHED_INFO                            is    25;  # RFC7924
  171 const integer: TLS_LTS                                is    26;
  172 const integer: COMPRESS_CERTIFICATE                   is    27;
  173 const integer: RECORD_SIZE_LIMIT                      is    28;  # RFC8449
  174 const integer: PWD_PROTECT                            is    29;  # RFC8492
  175 const integer: PWD_CLEAR                              is    30;  # RFC8492
  176 const integer: PASSWORD_SALT                          is    31;  # RFC8492
  177 const integer: TICKET_PINNING                         is    32;
  178 const integer: SESSION_TICKET_TLS                     is    35;  # RFC4507
  179 const integer: PRE_SHARED_KEY                         is    41;  # RFC8446
  180 const integer: EARLY_DATA                             is    42;  # RFC8446
  181 const integer: SUPPORTED_VERSIONS                     is    43;  # RFC8446
  182 const integer: COOKIE                                 is    44;  # RFC8446
  183 const integer: PSK_KEY_EXCHANGE_MODES                 is    45;  # RFC8446
  184 const integer: CERTIFICATE_AUTHORITIES                is    47;  # RFC8446
  185 const integer: OID_FILTERS                            is    48;  # RFC8446
  186 const integer: POST_HANDSHAKE_AUTH                    is    49;  # RFC8446
  187 const integer: SIGNATURE_ALGORITHMS_CERT              is    50;  # RFC8446
  188 const integer: KEY_SHARE                              is    51;  # RFC8446
  189 const integer: TRANSPARENCY_INFO                      is    52;
  190 const integer: CONNECTION_ID                          is    53;
  191 const integer: EXTERNAL_ID_HASH                       is    55;
  192 const integer: EXTERNAL_SESSION_ID                    is    56;
  193 const integer: NEXT_PROTOCOL_NEGOTIATION              is 13172;
  194 const integer: RENEGOTIATION_INFO                     is 65281;  # RFC5746
  195 
  196 # Elliptic curves:
  197 const integer: SECP192K1 is 18;
  198 const integer: SECP192R1 is 19;
  199 const integer: SECP224K1 is 20;
  200 const integer: SECP224R1 is 21;
  201 const integer: SECP256K1 is 22;
  202 const integer: SECP256R1 is 23;
  203 const integer: SECP384R1 is 24;
  204 const integer: SECP521R1 is 25;
  205 
  206 const array ellipticCurve: curveByNumber is [SECP192K1] (
  207     secp192k1, secp192r1, secp224k1, secp224r1, secp256k1,
  208     secp256r1, secp384r1, secp521r1);
  209 
  210 const char: NAMED_CURVE is '\3;';
  211 
  212 const array digestAlgorithm: signatureHashByNumber is [1] (
  213     MD5, SHA1, SHA224, SHA256, SHA384, SHA512);
  214 
  215 const integer: RSA_PKCS1_MD5_SHA1     is 16#0100;
  216 const integer: RSA_PKCS1_SHA1         is 16#0201;
  217 const integer: RSA_PKCS1_SHA224       is 16#0301;
  218 const integer: RSA_PKCS1_SHA256       is 16#0401;
  219 const integer: RSA_PKCS1_SHA384       is 16#0501;
  220 const integer: RSA_PKCS1_SHA512       is 16#0601;
  221 const integer: ECDSA_SHA1             is 16#0203;
  222 const integer: ECDSA_SECP256R1_SHA256 is 16#0403;
  223 
  224 const array integer: signatureSchemes is [] (
  225     ECDSA_SECP256R1_SHA256, RSA_PKCS1_SHA256, RSA_PKCS1_SHA1, ECDSA_SHA1, RSA_PKCS1_MD5_SHA1);
  226 
  227 const array integer: serverSignatureSchemes is [] (
  228     RSA_PKCS1_SHA512, RSA_PKCS1_SHA384, RSA_PKCS1_SHA256, RSA_PKCS1_SHA1,
  229     RSA_PKCS1_MD5_SHA1);
  230 
  231 const type: tlsParseState is new struct
  232     var char: contentType is NO_MESSAGE;
  233     var integer: length is 0;
  234     var string: message is "";
  235     var integer: pos is 1;
  236     var char: alert is CLOSE_NOTIFY;
  237   end struct;
  238 
  239 const type: tlsFile is sub null_file struct
  240     var file: sock is STD_NULL;
  241     var tlsParseState: parseState is tlsParseState.value;
  242     var tlsParameters: parameters is tlsParameters.value;
  243     var string: readBuffer is "";
  244   end struct;
  245 
  246 const type: clientSession is new struct
  247     var string:              session_id              is "";
  248     var cipherAlgorithm:     bulk_cipher_algorithm   is NO_CIPHER;
  249     var string:              master_secret           is "";
  250     var time:                last_use                is time.value;
  251   end struct;
  252 
  253 const duration: clientCacheValid is 1 . MINUTES;
  254 const type: clientSessionCacheType is hash [socketAddress] clientSession;
  255 
  256 var clientSessionCacheType: clientSessionCache is clientSessionCacheType.value;
  257 
  258 const string: MD5_PAD1 is "\16#36;" mult 48;
  259 const string: MD5_PAD2 is "\16#5c;" mult 48;
  260 const string: SHA_PAD1 is "\16#36;" mult 40;
  261 const string: SHA_PAD2 is "\16#5c;" mult 40;
  262 
  263 
  264 # Showtls defines showTlsMsg(), showTlsMsgType(), showHandshakeMsg() and showX509Cert().
  265 # Activate it, to debug tls.s7i.
  266 # include "showtls.s7i";
  267 
  268 
  269 const func integer: getEllipticCurveNumber (in ellipticCurve: curve) is func
  270   result
  271     var integer: curveNumber is 0;
  272   begin
  273     if curve.name = "secp192k1" then
  274       curveNumber := SECP192K1;
  275     elsif curve.name = "secp192r1" then
  276       curveNumber := SECP192R1;
  277     elsif curve.name = "secp224k1" then
  278       curveNumber := SECP224K1;
  279     elsif curve.name = "secp224r1" then
  280       curveNumber := SECP224R1;
  281     elsif curve.name = "secp256k1" then
  282       curveNumber := SECP256K1;
  283     elsif curve.name = "secp256r1" then
  284       curveNumber := SECP256R1;
  285     elsif curve.name = "secp384r1" then
  286       curveNumber := SECP384R1;
  287     elsif curve.name = "secp512r1" then
  288       curveNumber := SECP521R1;
  289     end if;
  290   end func;
  291 
  292 
  293 const proc: storeCipherSuite (inout tlsParameters: parameters) is func
  294   begin
  295     # writeln("cipher_suite: " <& ord(parameters.cipher_suite) radix 16 lpad0 4);
  296     if parameters.cipher_suite = TLS_NULL_WITH_NULL_NULL then
  297       parameters.bulk_cipher_algorithm := NO_CIPHER;
  298       parameters.key_material_length := 0;
  299       parameters.mac_algorithm := NO_DIGEST;
  300     elsif parameters.cipher_suite = TLS_RSA_WITH_RC4_128_MD5 then
  301       parameters.bulk_cipher_algorithm := RC4;
  302       parameters.key_material_length := 16;
  303       parameters.mac_algorithm := MD5;
  304     elsif parameters.cipher_suite = TLS_RSA_WITH_RC4_128_SHA then
  305       parameters.bulk_cipher_algorithm := RC4;
  306       parameters.key_material_length := 16;
  307       parameters.mac_algorithm := SHA1;
  308     elsif parameters.cipher_suite = TLS_RSA_WITH_3DES_EDE_CBC_SHA then
  309       parameters.bulk_cipher_algorithm := TDES;
  310       parameters.key_material_length := 24;
  311       parameters.mac_algorithm := SHA1;
  312     elsif parameters.cipher_suite = TLS_RSA_WITH_DES_CBC_SHA then
  313       parameters.bulk_cipher_algorithm := DES;
  314       parameters.key_material_length := 8;
  315       parameters.mac_algorithm := SHA1;
  316     elsif parameters.cipher_suite = TLS_RSA_WITH_AES_128_CBC_SHA then
  317       parameters.bulk_cipher_algorithm := AES;
  318       parameters.key_material_length := 16;
  319       parameters.mac_algorithm := SHA1;
  320     elsif parameters.cipher_suite = TLS_RSA_WITH_AES_256_CBC_SHA then
  321       parameters.bulk_cipher_algorithm := AES;
  322       parameters.key_material_length := 32;
  323       parameters.mac_algorithm := SHA1;
  324     elsif parameters.cipher_suite = TLS_RSA_WITH_AES_128_CBC_SHA256 then
  325       parameters.bulk_cipher_algorithm := AES;
  326       parameters.key_material_length := 16;
  327       parameters.mac_algorithm := SHA256;
  328     elsif parameters.cipher_suite = TLS_RSA_WITH_AES_256_CBC_SHA256 then
  329       parameters.bulk_cipher_algorithm := AES;
  330       parameters.key_material_length := 32;
  331       parameters.mac_algorithm := SHA256;
  332     elsif parameters.cipher_suite = TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA then
  333       parameters.key_exchange_algorithm := EC_DIFFIE_HELLMAN;
  334       parameters.bulk_cipher_algorithm := AES;
  335       parameters.key_material_length := 16;
  336       parameters.mac_algorithm := SHA1;
  337     elsif parameters.cipher_suite = TLS_ECDHE_ECDSA_WITH_AES_128_CBC_SHA then
  338       parameters.key_exchange_algorithm := EC_DIFFIE_HELLMAN;
  339       parameters.bulk_cipher_algorithm := AES;
  340       parameters.key_material_length := 16;
  341       parameters.mac_algorithm := SHA1;
  342     else
  343       writeln("Unsupported cipher_suite: " <& ord(parameters.cipher_suite) radix 16 lpad0 4);
  344       # raise RANGE_ERROR;
  345     end if;
  346     parameters.block_size := blockSize(parameters.bulk_cipher_algorithm);
  347     parameters.hash_size := digestSize(parameters.mac_algorithm);
  348   end func;
  349 
  350 
  351 const proc: computeMasterSecret (inout tlsParameters: parameters,
  352     in string: preMasterSecret) is func
  353   begin
  354     # writeln("preMasterSecret: " <& hex(preMasterSecret));
  355     if parameters.tls_version = SSL_3_0 then
  356       parameters.master_secret := keyBlockFunction(preMasterSecret,
  357           parameters.client_random & parameters.server_random, 48);
  358     elsif parameters.tls_version = TLS_1_2 then
  359       parameters.master_secret := p_hash(SHA256, preMasterSecret,
  360           "master secret" & parameters.client_random & parameters.server_random, 48);
  361     else
  362       parameters.master_secret := pseudoRandomFunction(preMasterSecret,
  363           "master secret", parameters.client_random & parameters.server_random, 48);
  364     end if;
  365     # writeln("master_secret: " <& hex(parameters.master_secret));
  366   end func;
  367 
  368 
  369 const proc: storeKeys (inout tlsParameters: parameters) is func
  370   local
  371     var string: key_block is "";
  372     var integer: key_block_pos is 1;
  373     var string: client_write_MAC_secret is "";
  374     var string: server_write_MAC_secret is "";
  375     var string: client_write_key is "";
  376     var string: server_write_key is "";
  377     var string: client_initialization_vector is "";
  378     var string: server_initialization_vector is "";
  379   begin
  380     # writeln("client_random: " <& hex(parameters.client_random));
  381     # writeln("server_random: " <& hex(parameters.server_random));
  382     if parameters.tls_version = SSL_3_0 then
  383       key_block := keyBlockFunction(parameters.master_secret,
  384           parameters.server_random & parameters.client_random,
  385           2 * parameters.hash_size + 2 * parameters.key_material_length + 2 * parameters.block_size);
  386     elsif parameters.tls_version = TLS_1_2 then
  387       key_block := p_hash(SHA256, parameters.master_secret,
  388           "key expansion" & parameters.server_random & parameters.client_random,
  389           2 * parameters.hash_size + 2 * parameters.key_material_length + 2 * parameters.block_size);
  390     else
  391       key_block := pseudoRandomFunction(parameters.master_secret,
  392           "key expansion", parameters.server_random & parameters.client_random,
  393           2 * parameters.hash_size + 2 * parameters.key_material_length + 2 * parameters.block_size);
  394     end if;
  395     # writeln("key_block: " <& hex(key_block));
  396     # writeln("length(key_block): " <& length(key_block));
  397     client_write_MAC_secret := key_block[key_block_pos len parameters.hash_size];
  398     key_block_pos +:= parameters.hash_size;
  399     server_write_MAC_secret := key_block[key_block_pos len parameters.hash_size];
  400     key_block_pos +:= parameters.hash_size;
  401     client_write_key := key_block[key_block_pos len parameters.key_material_length];
  402     key_block_pos +:= parameters.key_material_length;
  403     server_write_key := key_block[key_block_pos len parameters.key_material_length];
  404     key_block_pos +:= parameters.key_material_length;
  405     client_initialization_vector := key_block[key_block_pos len parameters.block_size];
  406     key_block_pos +:= parameters.block_size;
  407     server_initialization_vector := key_block[key_block_pos len parameters.block_size];
  408     # writeln("client_write_MAC_secret: " <& hex(client_write_MAC_secret));
  409     # writeln("server_write_MAC_secret: " <& hex(server_write_MAC_secret));
  410     # writeln("client_write_key: " <& hex(client_write_key));
  411     # writeln("server_write_key: " <& hex(server_write_key));
  412     if parameters.isClient then
  413       parameters.readMacSecret := server_write_MAC_secret;
  414       parameters.writeMacSecret := client_write_MAC_secret;
  415       parameters.readCipherState := setCipherKey(parameters.bulk_cipher_algorithm,
  416           server_write_key, server_initialization_vector);
  417       parameters.writeCipherState := setCipherKey(parameters.bulk_cipher_algorithm,
  418           client_write_key, client_initialization_vector);
  419     else
  420       parameters.readMacSecret := client_write_MAC_secret;
  421       parameters.writeMacSecret := server_write_MAC_secret;
  422       parameters.readCipherState := setCipherKey(parameters.bulk_cipher_algorithm,
  423           client_write_key, client_initialization_vector);
  424       parameters.writeCipherState := setCipherKey(parameters.bulk_cipher_algorithm,
  425           server_write_key, server_initialization_vector);
  426     end if;
  427   end func;
  428 
  429 
  430 const func string: getRsaSignature (in string: signatureStri) is func
  431   result
  432     var string: signature is "";
  433   local
  434     var asn1DataElement: dataElem is asn1DataElement.value;
  435     var integer: pos is 1;
  436     var algorithmIdentifierType: algorithmIdentifier is algorithmIdentifierType.value;
  437   begin
  438     dataElem := getAsn1DataElement(signatureStri, pos);
  439     if dataElem.tagCategory = tagSequence then
  440       algorithmIdentifier := getAlgorithmIdentifier(signatureStri, pos);
  441       dataElem := getAsn1DataElement(signatureStri, pos);
  442       if dataElem.tagCategory = tagOctetString then
  443         signature := getData(signatureStri, pos, dataElem);
  444       end if;
  445     end if;
  446   end func;
  447 
  448 
  449 const func string: genRsaSignature (in string: signature, in digestAlgorithm: digestAlg) is func
  450   result
  451     var string: signatureString is "";
  452   local
  453     var algorithmIdentifierType: algorithmIdentifier is algorithmIdentifierType.value;
  454   begin
  455     case digestAlg of
  456       when {SHA1}:   algorithmIdentifier.algorithm := SHA1_OID;
  457       when {SHA256}: algorithmIdentifier.algorithm := SHA256_OID;
  458       when {SHA384}: algorithmIdentifier.algorithm := SHA384_OID;
  459       when {SHA512}: algorithmIdentifier.algorithm := SHA512_OID;
  460     end case;
  461     signatureString := genAsn1Sequence(
  462             genAlgorithmIdentifier(algorithmIdentifier) &
  463             genAsn1Element(tagOctetString, signature));
  464   end func;
  465 
  466 
  467 const func ecdsaSignature: getEcSignature (in string: signatureStri) is func
  468   result
  469     var ecdsaSignature: signature is ecdsaSignature.value;
  470   local
  471     var asn1DataElement: dataElem is asn1DataElement.value;
  472     var integer: pos is 1;
  473   begin
  474     dataElem := getAsn1DataElement(signatureStri, pos);
  475     if dataElem.tagCategory = tagSequence then
  476       dataElem := getAsn1DataElement(signatureStri, pos);
  477       if dataElem.tagCategory = tagInteger then
  478         signature.r := bytes2BigInt(getData(signatureStri, pos, dataElem), UNSIGNED, BE);
  479         dataElem := getAsn1DataElement(signatureStri, pos);
  480         if dataElem.tagCategory = tagInteger then
  481           signature.s := bytes2BigInt(getData(signatureStri, pos, dataElem), UNSIGNED, BE);
  482         else
  483           signature.r := 0_;
  484         end if;
  485       end if;
  486     end if;
  487   end func;
  488 
  489 
  490 const func boolean: verifySignature (in string: hashParameter, in integer: signatureScheme,
  491     in string: signatureStri, in tlsParameters: parameters, inout tlsParseState: state) is func
  492   result
  493     var boolean: verified is FALSE;
  494   local
  495     var string: signatureHash is "";
  496     var string: decryptedSignature is "";
  497     var ecdsaSignature: signature is ecdsaSignature.value;
  498   begin
  499     case signatureScheme of
  500       when {RSA_PKCS1_MD5_SHA1}:
  501         signatureHash := md5(hashParameter) & sha1(hashParameter);
  502         verified := rsassaPkcs1V15Decrypt(parameters.publicRsaCertificateKey, signatureStri) = signatureHash;
  503       when {RSA_PKCS1_SHA1, RSA_PKCS1_SHA224, RSA_PKCS1_SHA256, RSA_PKCS1_SHA384, RSA_PKCS1_SHA512}:
  504         signatureHash := msgDigest(signatureHashByNumber[signatureScheme mdiv 256],
  505                                    hashParameter);
  506         decryptedSignature := rsassaPkcs1V15Decrypt(parameters.publicRsaCertificateKey, signatureStri);
  507         verified := getRsaSignature(decryptedSignature) = signatureHash;
  508       when {ECDSA_SECP256R1_SHA256}:
  509         signatureHash := sha256(hashParameter);
  510         signature := getEcSignature(signatureStri);
  511         verified := verify(secp256r1, bytes2BigInt(signatureHash, UNSIGNED, BE),
  512                            signature, parameters.publicEccCertificateKey);
  513       when {ECDSA_SHA1}:
  514         signatureHash := sha1(hashParameter);
  515         signature := getEcSignature(signatureStri);
  516         verified := verify(parameters.curve, bytes2BigInt(signatureHash, UNSIGNED, BE),
  517                            signature, parameters.publicEccCertificateKey);
  518     end case;
  519   end func;
  520 
  521 
  522 const func string: genSignature (in string: hashParameter, in tlsParameters: parameters) is func
  523   result
  524     var string: signatureStri is "";
  525   local
  526     var string: signatureHash is "";
  527     var string: rsaSignature is "";
  528     var digestAlgorithm: digestAlg is NO_DIGEST;
  529     var integer: signatureHashNumber is 0;
  530     var ecdsaSignature: signature is ecdsaSignature.value;
  531   begin
  532     case parameters.signatureScheme of
  533       when {RSA_PKCS1_MD5_SHA1}:
  534         signatureHash := md5(hashParameter) & sha1(hashParameter);
  535         signatureStri := rsassaPkcs1V15Encrypt(parameters.privateRsaCertificateKey, signatureHash);
  536       when {RSA_PKCS1_SHA1, RSA_PKCS1_SHA224, RSA_PKCS1_SHA256, RSA_PKCS1_SHA384, RSA_PKCS1_SHA512}:
  537         digestAlg := signatureHashByNumber[parameters.signatureScheme mdiv 256];
  538         signatureHash := msgDigest(digestAlg, hashParameter);
  539         rsaSignature := genRsaSignature(signatureHash, digestAlg);
  540         signatureStri := rsassaPkcs1V15Encrypt(parameters.privateRsaCertificateKey, rsaSignature);
  541       when {ECDSA_SECP256R1_SHA256}:
  542         signatureHash := sha256(hashParameter);
  543         signature := sign(secp256r1, bytes2BigInt(signatureHash, UNSIGNED, BE),
  544                           parameters.privateEccCertificateKey);
  545         signatureStri := genAsn1Sequence(
  546             genAsn1Element(tagInteger, bytes(signature.r, SIGNED, BE)) &
  547             genAsn1Element(tagInteger, bytes(signature.s, SIGNED, BE)));
  548 (*
  549         signatureHash := sha1(parameters.client_random & parameters.server_random &
  550                               serverParams);
  551         signature := sign(parameters.curve, bytes2BigInt(signatureHash, UNSIGNED, BE),
  552                           parameters.privateEccCertificateKey);
  553         signatureStri := genAsn1Sequence(
  554             genAsn1Element(tagInteger, bytes(signature.r, SIGNED, BE)) &
  555             genAsn1Element(tagInteger, bytes(signature.s, SIGNED, BE)));
  556         signatureStri := bytes(length(signatureStri), UNSIGNED, BE) & signatureStri;
  557 *)
  558     end case;
  559     signatureStri := int16AsTwoBytesBe(parameters.signatureScheme) &
  560                      int16AsTwoBytesBe(length(signatureStri)) &
  561                      signatureStri;
  562   end func;
  563 
  564 
  565 const proc: processCertificate (inout tlsParameters: parameters, inout tlsParseState: state) is func
  566   local
  567     var integer: startPos is 0;
  568     var integer: sequenceLen is 0;
  569     var integer: certLen is 0;
  570     var integer: index is 1;
  571     var x509cert: cert is x509cert.value;
  572   begin
  573     # writeln("certificate");
  574     startPos := state.pos;
  575     state.pos +:= 4;
  576     sequenceLen := bytes2Int(state.message[state.pos len 3], UNSIGNED, BE);
  577     state.pos +:= 3;
  578     while state.pos <= 3 + sequenceLen do
  579       certLen := bytes2Int(state.message[state.pos len 3], UNSIGNED, BE);
  580       state.pos +:= 3;
  581       parameters.serverCertificates.certList &:= [] (state.message[state.pos len certLen]);
  582       state.pos +:= certLen;
  583     end while;
  584     cert := getX509Cert(parameters.serverCertificates.certList[1]);
  585     # showX509Cert(cert);
  586     parameters.publicRsaCertificateKey := cert.tbsCertificate.subjectPublicKeyInfo.publicRsaKey;
  587     parameters.publicEccCertificateKey := cert.tbsCertificate.subjectPublicKeyInfo.publicEccKey;
  588     parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  589   end func;
  590 
  591 
  592 const proc: processEllipticCurvesExtension (inout tlsParameters: parameters,
  593     in string: extensionData) is func
  594   local
  595     var integer: pos is 1;
  596     var integer: length is 0;
  597     var integer: curveNumber is 0;
  598   begin
  599     length := bytes2Int(extensionData[pos len 2], UNSIGNED, BE);
  600     pos +:= 2;
  601     while pos < length(extensionData) and parameters.curve.bits = 0 do
  602       curveNumber := bytes2Int(extensionData[pos len 2], UNSIGNED, BE);
  603       # writeln("curveNumber: " <& curveNumber);
  604       pos +:= 2;
  605       if curveNumber >= minIdx(curveByNumber) and curveNumber <= maxIdx(curveByNumber) then
  606         parameters.curve := curveByNumber[curveNumber];
  607       end if;
  608     end while;
  609     # writeln("curve.name: " <& parameters.curve.name);
  610   end func;
  611 
  612 
  613 const proc: processSignatureAlgorithmsExtension (inout tlsParameters: parameters,
  614     in string: extensionData) is func
  615   local
  616     var integer: pos is 1;
  617     var integer: length is 0;
  618     var integer: signatureScheme is 0;
  619     var integer: schemeFromList is 0;
  620   begin
  621     length := bytes2Int(extensionData[pos len 2], UNSIGNED, BE);
  622     pos +:= 2;
  623     while pos < length(extensionData) and parameters.signatureScheme = 0 do
  624       signatureScheme := bytes2Int(extensionData[pos len 2], UNSIGNED, BE);
  625       # writeln("signatureScheme: " <& signatureScheme radix 16 lpad0 4);
  626       pos +:= 2;
  627       for schemeFromList range serverSignatureSchemes until parameters.signatureScheme <> 0 do
  628         if schemeFromList = signatureScheme then
  629           parameters.signatureScheme := signatureScheme;
  630         end if;
  631       end for;
  632     end while;
  633     # writeln("signatureScheme: " <& parameters.signatureScheme radix 16 lpad0 4);
  634   end func;
  635 
  636 
  637 const proc: processClientExtensions (inout tlsParameters: parameters, in string: extensions) is func
  638   local
  639     var integer: pos is 1;
  640     var integer: extensionType is 0;
  641     var integer: dataSize is 0;
  642     var string: data is "";
  643   begin
  644     while pos < length(extensions) do
  645       extensionType := bytes2Int(extensions[pos len 2], UNSIGNED, BE);
  646       pos +:= 2;
  647       dataSize := bytes2Int(extensions[pos len 2], UNSIGNED, BE);
  648       pos +:= 2;
  649       data := extensions[pos len dataSize];
  650       pos +:= dataSize;
  651       case extensionType of
  652         when {ELLIPTIC_CURVES}:
  653           processEllipticCurvesExtension(parameters, data);
  654         when {SIGNATURE_ALGORITHMS}:
  655           processSignatureAlgorithmsExtension(parameters, data);
  656       end case;
  657     end while;
  658   end func;
  659 
  660 
  661 const proc: processClientHello (inout tlsParameters: parameters, inout tlsParseState: state) is func
  662   local
  663     var integer: startPos is 0;
  664     var integer: length is 0;
  665     var integer: beyond is 0;
  666     var integer: sessionIdLen is 0;
  667     var integer: numCipherSuites is 0;
  668     var integer: numCompressionMethods is 0;
  669     var integer: extensionBytes is 0;
  670     var integer: index is 0;
  671     var integer: cipher_suite_number is ord(TLS_NULL_WITH_NULL_NULL);
  672     var integer: searchIndex is 0;
  673     var integer: minIndex is succ(length(supportedCiphers));
  674   begin
  675     # writeln("client_hello");
  676     startPos := state.pos;
  677     incr(state.pos);
  678     length := bytes2Int(state.message[state.pos len 3], UNSIGNED, BE);
  679     state.pos +:= 3;
  680     beyond := state.pos + length;
  681     if state.message[state.pos len 2] >= SSL_3_0 and
  682         state.message[state.pos len 2] <= TLS_1_2 then
  683       if state.message[state.pos len 2] < parameters.tls_version then
  684         parameters.tls_version := state.message[state.pos len 2];
  685       end if;
  686       state.pos +:= 2;
  687       parameters.client_random := state.message[state.pos len 32];
  688       state.pos +:= 32;
  689       sessionIdLen := ord(state.message[state.pos]);
  690       incr(state.pos);
  691       # writeln("SessionId: " <& hex(state.message[state.pos len sessionIdLen]));
  692       state.pos +:= sessionIdLen;
  693       numCipherSuites := bytes2Int(state.message[state.pos len 2], UNSIGNED, BE) div 2;
  694       state.pos +:= 2;
  695       for index range 1 to numCipherSuites do
  696         cipher_suite_number := bytes2Int(state.message[state.pos len 2], UNSIGNED, BE);
  697         for key searchIndex range supportedCiphers do
  698           if ord(supportedCiphers[searchIndex]) = cipher_suite_number and
  699               searchIndex < minIndex then
  700             minIndex := searchIndex;
  701           end if;
  702         end for;
  703         state.pos +:= 2;
  704       end for;
  705       if minIndex <= length(supportedCiphers) then
  706         parameters.cipher_suite := supportedCiphers[minIndex];
  707         # writeln("cipher_suite: " <& parameters.cipher_suite radix 16 lpad0 4);
  708         storeCipherSuite(parameters);
  709       else
  710         state.alert := HANDSHAKE_FAILURE;
  711       end if;
  712       numCompressionMethods := ord(state.message[state.pos]);
  713       state.pos +:= 1 + numCompressionMethods;
  714       if state.pos <= beyond - 2 then
  715         extensionBytes := bytes2Int(state.message[state.pos len 2], UNSIGNED, BE);
  716         state.pos +:= 2;
  717         processClientExtensions(parameters, state.message[state.pos len extensionBytes]);
  718         state.pos +:= extensionBytes;
  719       end if;
  720     else
  721       state.alert := PROCOCOL_VERSION;
  722     end if;
  723     parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  724   end func;
  725 
  726 
  727 const proc: processServerHello (inout tlsParameters: parameters, inout tlsParseState: state) is func
  728   local
  729     var integer: startPos is 0;
  730     var integer: length is 0;
  731     var integer: beyond is 0;
  732     var integer: sessionIdLen is 0;
  733     var integer: extensionBytes is 0;
  734   begin
  735     # writeln("server_hello");
  736     startPos := state.pos;
  737     incr(state.pos);
  738     length := bytes2Int(state.message[state.pos len 3], UNSIGNED, BE);
  739     state.pos +:= 3;
  740     beyond := state.pos + length;
  741     if state.message[state.pos len 2] >= SSL_3_0 and
  742         state.message[state.pos len 2] <= parameters.tls_version then
  743       parameters.tls_version := state.message[state.pos len 2];
  744       state.pos +:= 2;
  745       parameters.server_random := state.message[state.pos len 32];
  746       state.pos +:= 32;
  747       sessionIdLen := ord(state.message[state.pos]);
  748       incr(state.pos);
  749       parameters.session_id := state.message[state.pos len sessionIdLen];
  750       state.pos +:= sessionIdLen;
  751       parameters.cipher_suite := cipherSuite conv bytes2Int(state.message[state.pos len 2], UNSIGNED, BE);
  752       # writeln("Cipher: " <& ord(parameters.cipher_suite));
  753       storeCipherSuite(parameters);
  754       state.pos +:= 2;
  755       parameters.compression_algorithm := ord(state.message[state.pos]);
  756       incr(state.pos);
  757       if state.pos <= beyond - 2 then
  758         extensionBytes := bytes2Int(state.message[state.pos len 2], UNSIGNED, BE);
  759         state.pos +:= 2 + extensionBytes;
  760       end if;
  761     else
  762       state.alert := PROCOCOL_VERSION;
  763     end if;
  764     parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  765   end func;
  766 
  767 
  768 const proc: processServerKeyExchange (inout tlsParameters: parameters, inout tlsParseState: state) is func
  769   local
  770     var integer: startPos is 0;
  771     var integer: length is 0;
  772     var integer: beyond is 0;
  773     var integer: paramsStartPos is 0;
  774     var integer: curveNumber is 0;
  775     var integer: pointLength is 0;
  776     var string: pointData is "";
  777     var string: serverParams is "";
  778     var integer: signatureScheme is 0;
  779     var integer: signatureLength is 0;
  780     var string: signatureStri is "";
  781     var boolean: verified is FALSE;
  782   begin
  783     # writeln("server_key_exchange");
  784     startPos := state.pos;
  785     incr(state.pos);
  786     length := bytes2Int(state.message[state.pos len 3], UNSIGNED, BE);
  787     state.pos +:= 3;
  788     beyond := state.pos + length;
  789     if parameters.key_exchange_algorithm = EC_DIFFIE_HELLMAN then
  790       if state.message[state.pos] = NAMED_CURVE then
  791         paramsStartPos := state.pos;
  792         incr(state.pos);
  793         curveNumber := bytes2Int(state.message[state.pos len 2], UNSIGNED, BE);
  794         state.pos +:= 2;
  795         if curveNumber < minIdx(curveByNumber) or curveNumber > maxIdx(curveByNumber) then
  796           state.alert := ILLEGAL_PARAMETER;
  797         else
  798           parameters.curve := curveByNumber[curveNumber];
  799           pointLength := ord(state.message[state.pos]);
  800           incr(state.pos);
  801           pointData := state.message[state.pos len pointLength];
  802           parameters.publicEccKeyOfSever := ecPointDecode(parameters.curve, pointData);
  803           state.pos +:= pointLength;
  804           serverParams := state.message[paramsStartPos .. pred(state.pos)];
  805           signatureScheme := bytes2Int(state.message[state.pos len 2], UNSIGNED, BE);
  806           state.pos +:= 2;
  807           if parameters.tls_version >= TLS_1_2 then
  808             signatureLength := bytes2Int(state.message[state.pos len 2], UNSIGNED, BE);
  809             state.pos +:= 2;
  810           else
  811             signatureLength := beyond - state.pos;
  812           end if;
  813           signatureStri := state.message[state.pos len signatureLength];
  814           state.pos +:= signatureLength;
  815           verified := verifySignature(parameters.client_random &
  816                                       parameters.server_random &
  817                                       serverParams, signatureScheme, signatureStri,
  818                                       parameters, state);
  819         end if;
  820       else
  821         state.alert := ILLEGAL_PARAMETER;
  822       end if;
  823     end if;
  824     parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  825   end func;
  826 
  827 
  828 const proc: processCertificateRequest (inout tlsParameters: parameters, inout tlsParseState: state) is func
  829   local
  830     var integer: startPos is 0;
  831     var integer: length is 0;
  832   begin
  833     # writeln("certificate_request");
  834     startPos := state.pos;
  835     incr(state.pos);
  836     length := bytes2Int(state.message[state.pos len 3], UNSIGNED, BE);
  837     state.pos +:= 3;
  838     state.pos +:= length;
  839     parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  840   end func;
  841 
  842 
  843 const proc: processServerHelloDone (inout tlsParameters: parameters, inout tlsParseState: state) is func
  844   local
  845     var integer: startPos is 0;
  846     var integer: length is 0;
  847   begin
  848     # writeln("server_hello_done");
  849     startPos := state.pos;
  850     incr(state.pos);
  851     length := bytes2Int(state.message[state.pos len 3], UNSIGNED, BE);
  852     state.pos +:= 3;
  853     parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  854   end func;
  855 
  856 
  857 const proc: processClientKeyExchange (inout tlsParameters: parameters, inout tlsParseState: state) is func
  858   local
  859     var integer: startPos is 0;
  860     var integer: length is 0;
  861     var integer: encryptedSecretLength is 0;
  862     var string: encryptedPreMasterSecret is "";
  863     var string: preMasterSecret is "";
  864     var integer: pointLength is 0;
  865     var string: pointData is "";
  866     var ecPoint: publicEccKeyOfClient is ecPoint.value;
  867     var ecPoint: sharedSecretEcPoint is ecPoint.value;
  868   begin
  869     # writeln("client_key_exchange");
  870     startPos := state.pos;
  871     incr(state.pos);
  872     length := bytes2Int(state.message[state.pos len 3], UNSIGNED, BE);
  873     state.pos +:= 3;
  874     if parameters.key_exchange_algorithm = RSA then
  875       if parameters.tls_version = SSL_3_0 then
  876         encryptedSecretLength := length;
  877       else
  878         encryptedSecretLength := bytes2Int(state.message[state.pos len 2], UNSIGNED, BE);
  879         state.pos +:= 2;
  880       end if;
  881       encryptedPreMasterSecret := state.message[state.pos len encryptedSecretLength];
  882       state.pos +:= encryptedSecretLength;
  883       # writeln("encryptedPreMasterSecret: " <& hex(encryptedPreMasterSecret));
  884       # writeln("length(encryptedPreMasterSecret): " <& length(encryptedPreMasterSecret));
  885       preMasterSecret := rsaesPkcs1V15Decrypt(parameters.privateRsaCertificateKey,
  886           encryptedPreMasterSecret);
  887     elsif parameters.key_exchange_algorithm = EC_DIFFIE_HELLMAN then
  888       pointLength := ord(state.message[state.pos]);
  889       incr(state.pos);
  890       pointData := state.message[state.pos len pointLength];
  891       publicEccKeyOfClient := ecPointDecode(parameters.curve, pointData);
  892       state.pos +:= pointLength;
  893       sharedSecretEcPoint := multFast(parameters.curve, publicEccKeyOfClient,
  894                                       parameters.ownEccKeyPair.privateKey);
  895       # writeln("sharedSecretEcPoint.x: " <& sharedSecretEcPoint.x radix 16);
  896       # writeln("length: " <& getSizeInBytes(parameters.curve));
  897       preMasterSecret := int2Octets(sharedSecretEcPoint.x,
  898                                     getSizeInBytes(parameters.curve));
  899     end if;
  900     # writeln("preMasterSecret: " <& hex(preMasterSecret));
  901     computeMasterSecret(parameters, preMasterSecret);
  902     # writeln("master_secret: " <& hex(parameters.master_secret));
  903     storeKeys(parameters);
  904     parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  905   end func;
  906 
  907 
  908 const proc: processChangeCipherSpec (inout tlsParameters: parameters, inout tlsParseState: state) is func
  909   local
  910     var integer: startPos is 0;
  911     var integer: length is 0;
  912   begin
  913     # writeln("change_cipher_spec");
  914     startPos := state.pos;
  915     incr(state.pos);
  916     length := bytes2Int(state.message[state.pos len 3], UNSIGNED, BE);
  917     state.pos +:= 4;
  918   end func;
  919 
  920 
  921 const proc: processFinished (inout tlsParameters: parameters, inout tlsParseState: state) is func
  922   local
  923     var integer: startPos is 0;
  924     var integer: length is 0;
  925     var string: finished_label is "";
  926     var string: verify_data is "";
  927     var string: handshake_hash is "";
  928     var string: computed_verify_data is "";
  929   begin
  930     # writeln("finished");
  931     startPos := state.pos;
  932     incr(state.pos);
  933     length := bytes2Int(state.message[state.pos len 3], UNSIGNED, BE);
  934     state.pos +:= 3;
  935     verify_data := state.message[state.pos len length];
  936     state.pos +:= length;
  937     # writeln("verify_data: " <& hex(verify_data));
  938     # writeln("master_secret: " <& hex(parameters.master_secret));
  939     # writeln("handshake_messages: " <& hex(parameters.handshake_messages));
  940     # writeln("tls_version: " <& literal(parameters.tls_version));
  941     if parameters.tls_version = SSL_3_0 then
  942       if parameters.isClient then
  943         finished_label := "SRVR";  # The sender is a server.
  944       else
  945         finished_label := "CLNT";  # The sender is a client.
  946       end if;
  947       # writeln("finished_label: " <& literal(finished_label));
  948       computed_verify_data := md5(parameters.master_secret & MD5_PAD2 &
  949                                   md5(parameters.handshake_messages & finished_label &
  950                                       parameters.master_secret & MD5_PAD1)) &
  951                               sha1(parameters.master_secret & SHA_PAD2 &
  952                                    sha1(parameters.handshake_messages & finished_label &
  953                                         parameters.master_secret & SHA_PAD1));
  954     else
  955       if parameters.isClient then
  956         finished_label := "server finished";  # The sender is a server.
  957       else
  958         finished_label := "client finished";  # The sender is a client.
  959       end if;
  960       # writeln("finished_label: " <& literal(finished_label));
  961       if parameters.tls_version = TLS_1_2 then
  962         computed_verify_data := p_hash(SHA256, parameters.master_secret, finished_label &
  963                                        sha256(parameters.handshake_messages), 12);
  964       else
  965         handshake_hash := md5(parameters.handshake_messages) &
  966                           sha1(parameters.handshake_messages);
  967         # writeln("handshake_hash: " <& hex(handshake_hash));
  968         # writeln("handshake_hash size: " <& length(handshake_hash));
  969         computed_verify_data := pseudoRandomFunction(parameters.master_secret, finished_label,
  970                                                      handshake_hash, 12);
  971       end if;
  972     end if;
  973     # writeln("computed_verify_data: " <& hex(computed_verify_data));
  974     if verify_data <> computed_verify_data then
  975       writeln(" ***** Handshake not verified");
  976       raise RANGE_ERROR;
  977     end if;
  978     parameters.handshake_messages &:= state.message[startPos .. pred(state.pos)];
  979   end func;
  980 
  981 
  982 const proc: getTlsMsgRecord (inout file: sock, inout tlsParseState: state) is func
  983   local
  984     var integer: missing is 0;
  985     var string: msg2 is "";
  986   begin
  987     # writeln("in getTlsMsgRecord");
  988     if state.pos > length(state.message) then
  989       state.message := gets(sock, 5);
  990       if length(state.message) = 5 and
  991           state.message[1] >= CHANGE_CIPHER_SPEC and state.message[1] <= APPLICATION_DATA then
  992         state.contentType := state.message[1];
  993         state.length := bytes2Int(state.message[4 len 2], UNSIGNED, BE);
  994         missing := state.length;
  995         repeat
  996           msg2 := gets(sock, missing);
  997           state.message &:= msg2;
  998           missing -:= length(msg2);
  999         until missing = 0 or eof(sock);
 1000         if missing = 0 then
 1001           state.pos := 6;
 1002         else
 1003           state.contentType := NO_MESSAGE;
 1004           state.length := 0;
 1005         end if;
 1006       else
 1007         state.contentType := NO_MESSAGE;
 1008         state.length := 0;
 1009         # writeln("EOF = " <& eof(sock));
 1010         # writeln("length(message) = " <& length(state.message));
 1011         # writeln("message = " <& literal(state.message));
 1012         # raise RANGE_ERROR;
 1013       end if;
 1014     end if;
 1015     # writeln("getTlsMsgRecord -> " <& length(state.message) <& " " <& literal(state.message));
 1016     # showTlsMsgType(state.message);
 1017     # showTlsMsg(state.message);
 1018   end func;
 1019 
 1020 
 1021 const proc: loadCompleteHandshakeMsg (inout file: sock, inout tlsParseState: state) is func
 1022   local
 1023     var integer: lengthOfHandshakeMsg is 0;
 1024     var integer: remainingBytesInMsgRecord is 0;
 1025     var integer: totallyMissing is 0;
 1026     var string: stri is "";
 1027     var integer: recordLength is 0;
 1028     var integer: missing is 0;
 1029     var string: msg2 is "";
 1030   begin
 1031     if length(state.message) >= state.pos + 3 then
 1032       # Determine the length of the handshake message.
 1033       lengthOfHandshakeMsg := bytes2Int(state.message[state.pos + 1 len 3], UNSIGNED, BE);
 1034       remainingBytesInMsgRecord := length(state.message) - state.pos - 3;
 1035       if lengthOfHandshakeMsg > remainingBytesInMsgRecord then
 1036         # In the current TLS message record are not enough characters.
 1037         totallyMissing := lengthOfHandshakeMsg - remainingBytesInMsgRecord;
 1038         # writeln("totallyMissing: " <& totallyMissing);
 1039         repeat
 1040           # Get the next TLS message record.
 1041           stri := gets(sock, 5);
 1042           if length(stri) = 5 and stri[1] = HANDSHAKE then
 1043             # We are reading additional data for a handshake message.
 1044             recordLength := bytes2Int(stri[4 len 2], UNSIGNED, BE);
 1045             missing := recordLength;
 1046             repeat
 1047               msg2 := gets(sock, missing);
 1048               state.message &:= msg2;
 1049               missing -:= length(msg2);
 1050             until missing = 0 or eof(sock);
 1051             totallyMissing -:= recordLength;
 1052           else
 1053             state.alert := UNEXPECTED_MESSAGE;
 1054           end if;
 1055         until totallyMissing <= 0 or eof(sock);
 1056       end if;
 1057     end if;
 1058   end func;
 1059 
 1060 
 1061 const func string: genExtension (in integer: extensionType, in string: data) is
 1062   return int16AsTwoBytesBe(extensionType) &
 1063       int16AsTwoBytesBe(length(data)) & data;
 1064 
 1065 
 1066 const func string: serverNameExtension (in string: serverName) is
 1067   return int16AsTwoBytesBe(length(serverName) + 3) &
 1068          "\0;" & int16AsTwoBytesBe(length(serverName)) & serverName;
 1069 
 1070 
 1071 const func string: genEllipticCurvesExtension (in array ellipticCurve: curves) is func
 1072   result
 1073     var string: extensionBytes is "";
 1074   local
 1075     var integer: curveNumber is 0;
 1076   begin
 1077     extensionBytes := int16AsTwoBytesBe(length(curves) * 2);
 1078     for key curveNumber range curves do
 1079       extensionBytes &:= int16AsTwoBytesBe(curveNumber);
 1080     end for;
 1081   end func;
 1082 
 1083 
 1084 const func string: int16BeArrayExtension (in array integer: intArray) is func
 1085   result
 1086     var string: extensionBytes is "";
 1087   local
 1088     var integer: intValue is 0;
 1089   begin
 1090     extensionBytes := int16AsTwoBytesBe(length(intArray) * 2);
 1091     for intValue range intArray do
 1092       extensionBytes &:= int16AsTwoBytesBe(intValue);
 1093     end for;
 1094   end func;
 1095 
 1096 
 1097 const func string: genClientExtensions (in tlsParameters: parameters) is func
 1098   result
 1099     var string: extensionBytes is "";
 1100   begin
 1101     if parameters.hostName <> "" then
 1102       extensionBytes &:= genExtension(SERVER_NAME, serverNameExtension(parameters.hostName));
 1103     end if;
 1104     extensionBytes &:= genExtension(ELLIPTIC_CURVES, genEllipticCurvesExtension(curveByNumber));
 1105     extensionBytes &:= genExtension(SIGNATURE_ALGORITHMS, int16BeArrayExtension(signatureSchemes));
 1106     if extensionBytes <> "" then
 1107       extensionBytes := int16AsTwoBytesBe(length(extensionBytes)) & extensionBytes;
 1108     end if;
 1109   end func;
 1110 
 1111 
 1112 const func string: genClientHello (inout tlsParameters: parameters, in string: sessionId) is func
 1113   result
 1114     var string: clientHello is "";
 1115   local
 1116     var integer: length is 0;
 1117     var integer: count is 0;
 1118     var cipherSuite: cipher is TLS_NULL_WITH_NULL_NULL;
 1119   begin
 1120     parameters.client_random := int32AsFourBytesBe(timestamp1970(time(NOW)));   # Random - gmt_unix_time
 1121     parameters.client_random &:= int2Octets(rand(0_, 2_ ** (28 * 8) - 1_), 28); # Random - random_bytes
 1122     clientHello := str(HANDSHAKE) &               # ContentType (index: 1)
 1123                    parameters.tls_version &       # Version: 3.1
 1124                    "\0;\0;" &                     # Length: filled later (index: 4)
 1125                    str(CLIENT_HELLO) &            # HandshakeType (index: 6)
 1126                    "\0;\0;\0;" &                  # Length: filled later
 1127                    parameters.tls_version &       # Version: 3.1
 1128                    parameters.client_random &     # Random - random_bytes
 1129                    str(chr(length(sessionId))) &  # SessionId length
 1130                    sessionId &                    # SessionId
 1131                    int16AsTwoBytesBe(2 * length(supportedCiphers));  # Number of Ciphers in bytes
 1132     for cipher range supportedCiphers do
 1133       clientHello &:= int16AsTwoBytesBe(ord(cipher));
 1134     end for;
 1135     clientHello &:= "\1;" &                       # Number of CompressionMethods: 1 (1 byte)
 1136                     "\0;";                        # CompressionMethod-1: 0
 1137     clientHello &:= genClientExtensions(parameters);
 1138     length := length(clientHello);
 1139     clientHello @:= [4] int16AsTwoBytesBe(length - 5);
 1140     clientHello @:= [8] int16AsTwoBytesBe(length - 9);
 1141     parameters.handshake_messages &:= clientHello[6 ..];
 1142   end func;
 1143 
 1144 
 1145 const func string: genServerHello (inout tlsParameters: parameters) is func
 1146   result
 1147     var string: serverHello is "";
 1148   local
 1149     const integer: SESSION_ID_LEN is 32;
 1150     var integer: length is 0;
 1151     var integer: count is 0;
 1152   begin
 1153     parameters.server_random := int32AsFourBytesBe(timestamp1970(time(NOW)));   # Random - gmt_unix_time
 1154     parameters.server_random &:= int2Octets(rand(0_, 2_ ** (28 * 8) - 1_), 28); # Random - random_bytes
 1155     parameters.session_id :=
 1156         int2Octets(rand(0_, 2_ ** (SESSION_ID_LEN * 8) - 1_), SESSION_ID_LEN);  # SessionId
 1157     serverHello := str(HANDSHAKE) &            # ContentType (index: 1)
 1158                    parameters.tls_version &    # Version: take version from client_hello.
 1159                    "\0;\0;" &                  # Length: filled later (index: 4)
 1160                    str(SERVER_HELLO) &         # HandshakeType (index: 6)
 1161                    "\0;\0;\0;" &               # Length: filled later
 1162                    parameters.tls_version &    # Version: take version from client_hello.
 1163                    parameters.server_random &  # Random
 1164                    str(chr(SESSION_ID_LEN)) &  # SessionId length
 1165                    parameters.session_id &     # SessionId
 1166                    int16AsTwoBytesBe(ord(parameters.cipher_suite)) &
 1167                    "\0;";                      # CompressionMethod: 0
 1168     length := length(serverHello);
 1169     serverHello @:= [4] int16AsTwoBytesBe(length - 5);
 1170     serverHello @:= [8] int16AsTwoBytesBe(length - 9);
 1171     parameters.handshake_messages &:= serverHello[6 ..];
 1172   end func;
 1173 
 1174 
 1175 const func string: genCertificate (inout tlsParameters: parameters, in array string: certList) is func
 1176   result
 1177     var string: certificate is "";
 1178   local
 1179     var integer: length is 0;
 1180     var integer: index is 0;
 1181   begin
 1182     certificate := str(HANDSHAKE) &          # ContentType (index: 1)
 1183                    parameters.tls_version &  # Version: take version from client_hello.
 1184                    "\0;\0;" &                # Length: filled later (index: 4)
 1185                    str(CERTIFICATE) &        # HandshakeType (index: 6)
 1186                    "\0;\0;\0;" &             # Length: filled later
 1187                    "\0;\0;\0;";              # Sequence length: filled later
 1188     for key index range certList do
 1189       certificate &:= "\0;" & int16AsTwoBytesBe(length(certList[index])) &
 1190                       certList[index];
 1191     end for;
 1192     length := length(certificate);
 1193     certificate @:= [4] int16AsTwoBytesBe(length - 5);
 1194     certificate @:= [8] int16AsTwoBytesBe(length - 9);
 1195     certificate @:= [11] int16AsTwoBytesBe(length - 12);
 1196     parameters.handshake_messages &:= certificate[6 ..];
 1197   end func;
 1198 
 1199 
 1200 const func string: genServerKeyExchange (inout tlsParameters: parameters) is func
 1201   result
 1202     var string: serverKeyExchange is "";
 1203   local
 1204     var integer: length is 0;
 1205     var string: serverParams is "";
 1206     var string: pointData is "";
 1207     var string: signatureHash is "";
 1208     var ecdsaSignature: signature is ecdsaSignature.value;
 1209     var string: signatureStri is "";
 1210   begin
 1211     # writeln("genServerKeyExchange");
 1212     serverKeyExchange := str(HANDSHAKE) &            # ContentType (index: 1)
 1213                          parameters.tls_version &    # Version: 3.1
 1214                          "\0;\0;" &                  # Length: filled later (index: 4)
 1215                          str(SERVER_KEY_EXCHANGE) &  # HandshakeType (index: 6)
 1216                          "\0;\0;\0;";                # Length: filled later
 1217     if parameters.key_exchange_algorithm = EC_DIFFIE_HELLMAN then
 1218       # writeln("curve.name: " <& parameters.curve.name);
 1219       parameters.ownEccKeyPair := genEccKeyPair(parameters.curve);
 1220       # writeln("curve number: " <& getEllipticCurveNumber(parameters.curve));
 1221       pointData := ecPointEncode(parameters.curve, parameters.ownEccKeyPair.publicKey);
 1222       serverParams &:= str(NAMED_CURVE) &
 1223                        int16AsTwoBytesBe(getEllipticCurveNumber(parameters.curve)) &
 1224                        str(chr(length(pointData))) & pointData;
 1225       signatureStri := genSignature(parameters.client_random &
 1226                                     parameters.server_random &
 1227                                     serverParams, parameters);
 1228       serverKeyExchange &:= serverParams & signatureStri;
 1229     end if;
 1230     length := length(serverKeyExchange);
 1231     serverKeyExchange @:= [4] int16AsTwoBytesBe(length - 5);
 1232     serverKeyExchange @:= [8] int16AsTwoBytesBe(length - 9);
 1233     parameters.handshake_messages &:= serverKeyExchange[6 ..];
 1234   end func;
 1235 
 1236 
 1237 const func string: genServerHelloDone (inout tlsParameters: parameters) is func
 1238   result
 1239     var string: serverHelloDone is "";
 1240   local
 1241     var integer: length is 0;
 1242   begin
 1243     serverHelloDone := str(HANDSHAKE) &          # ContentType (index: 1)
 1244                        parameters.tls_version &  # Version: take version from client_hello.
 1245                        "\0;\0;" &                # Length: filled later (index: 4)
 1246                        str(SERVER_HELLO_DONE) &  # HandshakeType (index: 6)
 1247                        "\0;\0;\0;";              # Length: 0
 1248     length := length(serverHelloDone);
 1249     serverHelloDone @:= [4] int16AsTwoBytesBe(length - 5);
 1250     parameters.handshake_messages &:= serverHelloDone[6 ..];
 1251   end func;
 1252 
 1253 
 1254 const func string: genClientKeyExchange (inout tlsParameters: parameters) is func
 1255   result
 1256     var string: clientKeyExchange is "";
 1257   local
 1258     var integer: length is 0;
 1259     var string: preMasterSecret is "";
 1260     var string: encryptedPreMasterSecret is "";
 1261     var string: pointData is "";
 1262     var ecPoint: sharedSecretEcPoint is ecPoint.value;
 1263   begin
 1264     # writeln("genClientKeyExchange");
 1265     clientKeyExchange := str(HANDSHAKE) &            # ContentType (index: 1)
 1266                          parameters.tls_version &    # Version: 3.1
 1267                          "\0;\0;" &                  # Length: filled later (index: 4)
 1268                          str(CLIENT_KEY_EXCHANGE) &  # HandshakeType (index: 6)
 1269                          "\0;\0;\0;";                # Length: filled later
 1270     if parameters.key_exchange_algorithm = RSA then
 1271       preMasterSecret := parameters.tls_version;                          # ProtocolVersion
 1272       preMasterSecret &:= int2Octets(rand(0_, 2_ ** (46 * 8) - 1_), 46);  # Random - random_bytes
 1273       encryptedPreMasterSecret := rsaesPkcs1V15Encrypt(parameters.publicRsaCertificateKey,
 1274           preMasterSecret);
 1275       # writeln("encryptedPreMasterSecret: " <& hex(encryptedPreMasterSecret));
 1276       # writeln("length(encryptedPreMasterSecret): " <& length(encryptedPreMasterSecret));
 1277       if parameters.tls_version <> SSL_3_0 then
 1278         clientKeyExchange &:= int16AsTwoBytesBe(length(encryptedPreMasterSecret));
 1279       end if;
 1280       clientKeyExchange &:= encryptedPreMasterSecret;
 1281     elsif parameters.key_exchange_algorithm = EC_DIFFIE_HELLMAN then
 1282       parameters.ownEccKeyPair := genEccKeyPair(parameters.curve);
 1283       pointData := ecPointEncode(parameters.curve, parameters.ownEccKeyPair.publicKey);
 1284       clientKeyExchange &:= str(chr(length(pointData))) & pointData;
 1285       sharedSecretEcPoint := multFast(parameters.curve, parameters.publicEccKeyOfSever,
 1286                                       parameters.ownEccKeyPair.privateKey);
 1287       # writeln("sharedSecretEcPoint.x: " <& sharedSecretEcPoint.x radix 16);
 1288       # writeln("length: " <& getSizeInBytes(parameters.curve));
 1289       preMasterSecret := int2Octets(sharedSecretEcPoint.x,
 1290                                     getSizeInBytes(parameters.curve));
 1291     end if;
 1292     # writeln("preMasterSecret: " <& hex(preMasterSecret));
 1293     computeMasterSecret(parameters, preMasterSecret);
 1294     # writeln("master_secret: " <& hex(parameters.master_secret));
 1295     storeKeys(parameters);
 1296     length := length(clientKeyExchange);
 1297     clientKeyExchange @:= [4] int16AsTwoBytesBe(length - 5);
 1298     clientKeyExchange @:= [8] int16AsTwoBytesBe(length - 9);
 1299     parameters.handshake_messages &:= clientKeyExchange[6 ..];
 1300   end func;
 1301 
 1302 
 1303 const func string: genChangeCipherSpec (in tlsParameters: parameters) is func
 1304   result
 1305     var string: changeCipherSpec is "";
 1306   local
 1307     var integer: length is 0;
 1308   begin
 1309     changeCipherSpec := str(CHANGE_CIPHER_SPEC) &  # ContentType (index: 1)
 1310                         parameters.tls_version &   # Version: 3.1
 1311                         "\0;\0;" &                 # Length: filled later (index: 4)
 1312                         "\1;";                     # change_cipher_spec
 1313     length := length(changeCipherSpec);
 1314     changeCipherSpec @:= [4] int16AsTwoBytesBe(length - 5);
 1315   end func;
 1316 
 1317 
 1318 const func string: genFinished (inout tlsParameters: parameters) is func
 1319   result
 1320     var string: finished is "";
 1321   local
 1322     var integer: length is 0;
 1323     var string: finished_label is "";
 1324     var string: verify_data is "";
 1325   begin
 1326     finished := str(HANDSHAKE) &          # ContentType (index: 1)
 1327                 parameters.tls_version &  # Version: 3.1
 1328                 "\0;\0;" &                # Length: filled later (index: 4)
 1329                 str(FINISHED) &           # HandshakeType (index: 6)
 1330                 "\0;\0;\0;";              # Length: filled later
 1331     # writeln("master_secret: " <& hex(parameters.master_secret));
 1332     # writeln("handshake_messages: " <& hex(parameters.handshake_messages));
 1333     if parameters.tls_version = SSL_3_0 then
 1334       if parameters.isClient then
 1335         finished_label := "CLNT";
 1336       else
 1337         finished_label := "SRVR";
 1338       end if;
 1339       # writeln("finished_label: " <& literal(finished_label));
 1340       verify_data := md5(parameters.master_secret & MD5_PAD2 &
 1341                          md5(parameters.handshake_messages & finished_label &
 1342                              parameters.master_secret & MD5_PAD1)) &
 1343                      sha1(parameters.master_secret & SHA_PAD2 &
 1344                           sha1(parameters.handshake_messages & finished_label &
 1345                                parameters.master_secret & SHA_PAD1));
 1346     else
 1347       if parameters.isClient then
 1348         finished_label := "client finished";
 1349       else
 1350         finished_label := "server finished";
 1351       end if;
 1352       # writeln("finished_label: " <& literal(finished_label));
 1353       if parameters.tls_version = TLS_1_2 then
 1354         verify_data := p_hash(SHA256, parameters.master_secret, finished_label &
 1355                               sha256(parameters.handshake_messages), 12);
 1356       else
 1357         verify_data := pseudoRandomFunction(parameters.master_secret, finished_label,
 1358                                             md5(parameters.handshake_messages) &
 1359                                             sha1(parameters.handshake_messages), 12);
 1360       end if;
 1361     end if;
 1362     # writeln("verify_data: " <& hex(verify_data));
 1363     finished &:= verify_data;
 1364     length := length(finished);
 1365     finished @:= [4] int16AsTwoBytesBe(length - 5);
 1366     finished @:= [8] int16AsTwoBytesBe(length - 9);
 1367     parameters.handshake_messages &:= finished[6 ..];
 1368   end func;
 1369 
 1370 
 1371 const func string: genAlert (inout tlsParameters: parameters, in char: description) is func
 1372   result
 1373     var string: alert is "";
 1374   local
 1375     var integer: length is 0;
 1376   begin
 1377     alert := str(ALERT) &              # ContentType (index: 1)
 1378              parameters.tls_version &  # Version: 3.1
 1379              "\0;\0;" &                # Length: filled later (index: 4)
 1380              "\1;" &                   # level: 1
 1381              str(description);         # AlertDescription
 1382     length := length(alert);
 1383     alert @:= [4] int16AsTwoBytesBe(length - 5);
 1384   end func;
 1385 
 1386 
 1387 const func string: tlsEncryptRecord (inout tlsParameters: parameters, in string: plain) is func
 1388   result
 1389     var string: encrypted is "";
 1390   local
 1391     var string: content is "";
 1392     var string: iv is "";
 1393     var string: mac is "";
 1394     var integer: padding_length is 0;
 1395     var string: padding is "";
 1396     var string: encoded is "";
 1397     var integer: length is 0;
 1398   begin
 1399     # writeln("plain: " <& literal(plain));
 1400     # writeln("length(plain): " <& length(plain));
 1401     encrypted := plain[.. 3] &         # Head stays unchanged
 1402                  "\0;\0;";             # Length: filled later (index: 4)
 1403     # writeln("mac secret: " <& hex(parameters.writeMacSecret));
 1404     if parameters.tls_version = SSL_3_0 then
 1405       mac := msgDigest(parameters.mac_algorithm, parameters.writeMacSecret & SHA_PAD2 &
 1406                        msgDigest(parameters.mac_algorithm, parameters.writeMacSecret & SHA_PAD1 &
 1407                                  int64AsEightBytesBe(parameters.writeSequenceNumber) &
 1408                                  plain[1 len 1] & plain[4 ..]));
 1409     else
 1410       # writeln("mac algorithm: " <& ord(parameters.mac_algorithm));
 1411       # writeln("mac secret: " <& hex(parameters.writeMacSecret));
 1412       # writeln("hmac in: " <& hex(int64AsEightBytesBe(parameters.writeSequenceNumber) & plain));
 1413       mac := hmac(parameters.mac_algorithm, parameters.writeMacSecret,
 1414                   int64AsEightBytesBe(parameters.writeSequenceNumber) & plain);
 1415     end if;
 1416     content := plain[6 ..];
 1417     if parameters.block_size <> 0 then
 1418       if parameters.tls_version >= TLS_1_1 then
 1419         iv := int2Octets(rand(0_, 2_ ** (parameters.block_size * 8) - 1_), parameters.block_size);
 1420       end if;
 1421       padding_length := parameters.block_size - 1 -
 1422                         (length(content) + length(mac)) mod parameters.block_size;
 1423       # writeln("padding_length: " <& padding_length);
 1424       padding := str(chr(padding_length)) mult succ(padding_length);
 1425     end if;
 1426     # writeln("bulk_cipher_algorithm: " <& ord(parameters.bulk_cipher_algorithm));
 1427     # writeln("data: " <& hex(content));
 1428     # writeln("mac: " <& hex(mac));
 1429     # writeln("before encode: " <& hex(iv & content & mac & padding));
 1430     encoded := encode(parameters.writeCipherState, iv & content & mac & padding);
 1431     # writeln("encoded: " <& literal(encoded));
 1432     # writeln("length(encoded): " <& length(encoded));
 1433     encrypted &:= encoded;
 1434     length := length(encrypted);
 1435     encrypted @:= [4] int16AsTwoBytesBe(length - 5);
 1436     # writeln("encrypted message: " <& hex(encrypted));
 1437     # writeln("length: " <& length(encrypted));
 1438     incr(parameters.writeSequenceNumber);
 1439   end func;
 1440 
 1441 
 1442 const func boolean: tlsDecryptRecord (inout tlsParameters: parameters, inout tlsParseState: state) is func
 1443   result
 1444     var boolean: decryptOkay is TRUE;
 1445   local
 1446     var string: version is "";
 1447     var string: decoded is "";
 1448     var integer: padding_length is 0;
 1449     var string: content is "";
 1450     var string: mac is "";
 1451     var string: verify is "";
 1452     var string: plain is "";
 1453   begin
 1454     # writeln("tlsDecryptRecord");
 1455     version := state.message[2 len 2];
 1456     # writeln("Version: " <& ord(version[1]) <& "." <& ord(version[2]));
 1457     # writeln("message: " <& literal(state.message));
 1458     decoded := decode(parameters.readCipherState, state.message[state.pos len state.length]);
 1459     if parameters.block_size <> 0 then
 1460       padding_length := ord(decoded[length(decoded)]);
 1461       if decoded[length(decoded) - padding_length ..] =
 1462           str(chr(padding_length)) mult succ(padding_length) then
 1463         decoded := decoded[.. length(decoded) - succ(padding_length)];
 1464         if version >= TLS_1_1 then
 1465           # writeln("iv: " <& hex(decoded[.. parameters.block_size]));
 1466           decoded := decoded[succ(parameters.block_size) ..]; # Remove iv
 1467         end if;
 1468       else
 1469         decryptOkay := FALSE;
 1470         state.alert := DECRYPTION_FAILED;
 1471       end if;
 1472     end if;
 1473     if decryptOkay then
 1474       content := decoded[.. length(decoded) - digestSize(parameters.mac_algorithm)];
 1475       mac := decoded[length(decoded) - digestSize(parameters.mac_algorithm) + 1 ..];
 1476       plain := state.message[.. 3] &
 1477                int16AsTwoBytesBe(length(content)) &
 1478                content;
 1479       # writeln("plain: " <& hex(plain));
 1480       # writeln("mac: " <& hex(mac));
 1481       if version = SSL_3_0 then
 1482         verify := msgDigest(parameters.mac_algorithm, parameters.readMacSecret & SHA_PAD2 &
 1483                             msgDigest(parameters.mac_algorithm, parameters.readMacSecret & SHA_PAD1 &
 1484                                       int64AsEightBytesBe(parameters.readSequenceNumber) &
 1485                                       plain[1 len 1] & plain[4 ..]));
 1486       else
 1487         verify := hmac(parameters.mac_algorithm, parameters.readMacSecret,
 1488                        int64AsEightBytesBe(parameters.readSequenceNumber) & plain);
 1489       end if;
 1490       # writeln("verify: " <& hex(verify));
 1491       if mac = verify then
 1492         state.length := length(content);
 1493         state.message := plain;
 1494       else
 1495         decryptOkay := FALSE;
 1496         state.alert := BAD_RECORD_MAC;
 1497       end if;
 1498     end if;
 1499     incr(parameters.readSequenceNumber);
 1500   end func;
 1501 
 1502 
 1503 const proc: sendAlertAndClose (inout tlsFile: aFile, in char: alertDescription) is func
 1504   local
 1505     var string: alert is "";
 1506   begin
 1507     alert := genAlert(aFile.parameters, alertDescription);
 1508     # showTlsMsg(alert);
 1509     if aFile.parameters.writeEncryptedRecords then
 1510       alert := tlsEncryptRecord(aFile.parameters, alert);
 1511     end if;
 1512     block
 1513       write(aFile.sock, alert);
 1514     exception
 1515       catch FILE_ERROR: noop;
 1516     end block;
 1517     close(aFile.sock);
 1518     aFile.sock := STD_NULL;
 1519     aFile.parseState.pos := succ(length(aFile.parseState.message));
 1520   end func;
 1521 
 1522 
 1523 const proc: updateClientCache (in tlsParameters: parameters, in socketAddress: address) is func
 1524   local
 1525     var clientSession: session is clientSession.value;
 1526   begin
 1527     if parameters.session_id <> "" then
 1528       session.session_id            := parameters.session_id;
 1529       session.bulk_cipher_algorithm := parameters.bulk_cipher_algorithm;
 1530       session.master_secret         := parameters.master_secret;
 1531       session.last_use              := time(NOW);
 1532       clientSessionCache @:= [address] session;
 1533     end if;
 1534   end func;
 1535 
 1536 
 1537 const func file: negotiateSecurityParameters (inout tlsFile: new_file) is func
 1538   result
 1539     var file: tlsSock is STD_NULL;
 1540   local
 1541     var string: clientKeyExchange is "";
 1542     var string: changeCipherSpec is "";
 1543     var string: finished is "";
 1544     var boolean: serverHelloDone is FALSE;
 1545     var boolean: unexpectedMessage is FALSE;
 1546   begin
 1547     repeat
 1548       getTlsMsgRecord(new_file.sock, new_file.parseState);
 1549       # showTlsMsg(new_file.parseState.message);
 1550       if new_file.parseState.contentType = HANDSHAKE then
 1551         loadCompleteHandshakeMsg(new_file.sock, new_file.parseState);
 1552         if new_file.parseState.alert = CLOSE_NOTIFY then
 1553           # showHandshakeMsg(new_file.parseState.message, new_file.parseState.pos);
 1554           if new_file.parseState.message[new_file.parseState.pos] = CERTIFICATE then
 1555             processCertificate(new_file.parameters, new_file.parseState);
 1556           elsif new_file.parseState.message[new_file.parseState.pos] = SERVER_KEY_EXCHANGE then
 1557             processServerKeyExchange(new_file.parameters, new_file.parseState);
 1558           elsif new_file.parseState.message[new_file.parseState.pos] = CERTIFICATE_REQUEST then
 1559             processCertificateRequest(new_file.parameters, new_file.parseState);
 1560           elsif new_file.parseState.message[new_file.parseState.pos] = SERVER_HELLO_DONE then
 1561             processServerHelloDone(new_file.parameters, new_file.parseState);
 1562             serverHelloDone := TRUE;
 1563           else  # Any other handshake
 1564             unexpectedMessage := TRUE;
 1565           end if;
 1566         else
 1567           unexpectedMessage := TRUE;
 1568         end if;
 1569       else
 1570         unexpectedMessage := TRUE;
 1571       end if;
 1572     until serverHelloDone or unexpectedMessage;
 1573     if serverHelloDone then
 1574       clientKeyExchange := genClientKeyExchange(new_file.parameters);
 1575       # showTlsMsg(clientKeyExchange);
 1576       write(new_file.sock, clientKeyExchange);
 1577       changeCipherSpec := genChangeCipherSpec(new_file.parameters);
 1578       # showTlsMsg(changeCipherSpec);
 1579       write(new_file.sock, changeCipherSpec);
 1580       new_file.parameters.writeEncryptedRecords := TRUE;
 1581       finished := genFinished(new_file.parameters);
 1582       # showTlsMsg(finished);
 1583       finished := tlsEncryptRecord(new_file.parameters, finished);
 1584       write(new_file.sock, finished);
 1585       repeat
 1586         getTlsMsgRecord(new_file.sock, new_file.parseState);
 1587         # writeln(literal(new_file.parseState.message));
 1588         # showTlsMsg(new_file.parseState.message);
 1589       until new_file.parseState.contentType = CHANGE_CIPHER_SPEC or
 1590             new_file.parseState.contentType = ALERT or
 1591             new_file.parseState.contentType = NO_MESSAGE;
 1592       if new_file.parseState.contentType = CHANGE_CIPHER_SPEC then
 1593         processChangeCipherSpec(new_file.parameters, new_file.parseState);
 1594         getTlsMsgRecord(new_file.sock, new_file.parseState);
 1595         if new_file.parseState.contentType = HANDSHAKE then  # Handshake with encoded Finished message
 1596           if tlsDecryptRecord(new_file.parameters, new_file.parseState) then
 1597             # showTlsMsg(new_file.parseState.message);
 1598             if new_file.parseState.message[new_file.parseState.pos] = FINISHED then
 1599               processFinished(new_file.parameters, new_file.parseState);
 1600               # writeln("Version: " <& ord(new_file.parameters.tls_version[1]) <& "." <& ord(new_file.parameters.tls_version[2]));
 1601               # writeln("Cipher: " <& ord(new_file.parameters.cipher_suite));
 1602               updateClientCache(new_file.parameters, peerAddress(new_file.sock));
 1603               tlsSock := toInterface(new_file);
 1604             else
 1605               sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
 1606             end if;
 1607           else
 1608             sendAlertAndClose(new_file, new_file.parseState.alert);
 1609           end if;
 1610         else
 1611           sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
 1612         end if;
 1613       else
 1614         sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
 1615       end if;
 1616     else
 1617       sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
 1618     end if;
 1619   end func;
 1620 
 1621 
 1622 const func file: openTlsSocket (inout file: sock, in clientSession: session) is func
 1623   result
 1624     var file: tlsSock is STD_NULL;
 1625   local
 1626     var tlsFile: new_file is tlsFile.value;
 1627     var socketAddress: peerAddress is socketAddress.value;
 1628     var string: sessionId is "";
 1629     var string: clientHello is "";
 1630     var string: changeCipherSpec is "";
 1631     var string: finished is "";
 1632   begin
 1633     if sock <> STD_NULL then
 1634       peerAddress := peerAddress(sock);
 1635       new_file.sock := sock;
 1636       new_file.parameters.isClient := TRUE;
 1637       if session.last_use + clientCacheValid > time(NOW) then
 1638         sessionId := session.session_id;
 1639       end if;
 1640       clientHello := genClientHello(new_file.parameters, sessionId);
 1641       # showTlsMsg(clientHello);
 1642       write(sock, clientHello);
 1643       getTlsMsgRecord(sock, new_file.parseState);
 1644       if new_file.parseState.contentType = HANDSHAKE and
 1645           new_file.parseState.message[new_file.parseState.pos] = SERVER_HELLO then
 1646         # showTlsMsg(new_file.parseState.message);
 1647         processServerHello(new_file.parameters, new_file.parseState);
 1648         if new_file.parseState.alert <> CLOSE_NOTIFY then
 1649           sendAlertAndClose(new_file, new_file.parseState.alert);
 1650         elsif new_file.parameters.session_id <> sessionId or
 1651             new_file.parameters.bulk_cipher_algorithm <> session.bulk_cipher_algorithm then
 1652           tlsSock := negotiateSecurityParameters(new_file);
 1653         else
 1654           getTlsMsgRecord(new_file.sock, new_file.parseState);
 1655           # showTlsMsg(new_file.parseState.message);
 1656           if new_file.parseState.contentType = CHANGE_CIPHER_SPEC then
 1657             processChangeCipherSpec(new_file.parameters, new_file.parseState);
 1658             new_file.parameters.master_secret := session.master_secret;
 1659             storeKeys(new_file.parameters);
 1660             getTlsMsgRecord(new_file.sock, new_file.parseState);
 1661             if new_file.parseState.contentType = HANDSHAKE then  # Handshake with encoded Finished message
 1662               if tlsDecryptRecord(new_file.parameters, new_file.parseState) then
 1663                 # showTlsMsg(new_file.parseState.message);
 1664                 if new_file.parseState.message[new_file.parseState.pos] = FINISHED then
 1665                   processFinished(new_file.parameters, new_file.parseState);
 1666                   changeCipherSpec := genChangeCipherSpec(new_file.parameters);
 1667                   # showTlsMsg(changeCipherSpec);
 1668                   write(new_file.sock, changeCipherSpec);
 1669                   new_file.parameters.writeEncryptedRecords := TRUE;
 1670                   finished := genFinished(new_file.parameters);
 1671                   # showTlsMsg(finished);
 1672                   finished := tlsEncryptRecord(new_file.parameters, finished);
 1673                   write(new_file.sock, finished);
 1674                   updateClientCache(new_file.parameters, peerAddress);
 1675                   tlsSock := toInterface(new_file);
 1676                 else
 1677                   sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
 1678                 end if;
 1679               else
 1680                 sendAlertAndClose(new_file, new_file.parseState.alert);
 1681               end if;
 1682             else
 1683               sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
 1684             end if;
 1685           else
 1686             sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
 1687           end if;
 1688         end if;
 1689       else
 1690         sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
 1691       end if;
 1692       if tlsSock = STD_NULL then
 1693         excl(clientSessionCache, peerAddress);
 1694       end if;
 1695     end if;
 1696   end func;
 1697 
 1698 
 1699 (**
 1700  *  Return a connected TLS socket file based on the given ''sock''.
 1701  *  @param sock A connected internet socket file (client side).
 1702  *  @param hostName The server host name.
 1703  *  @return an open TLS socket file, or [[null_file#STD_NULL|STD_NULL]]
 1704  *          if it could not be opened.
 1705  *  @exception MEMORY_ERROR An out of memory situation occurred.
 1706  *)
 1707 const func file: openTlsSocket (inout file: sock, in string: hostName) is func
 1708   result
 1709     var file: tlsSock is STD_NULL;
 1710   local
 1711     var tlsFile: new_file is tlsFile.value;
 1712     var string: clientHello is "";
 1713   begin
 1714     if sock <> STD_NULL then
 1715       if peerAddress(sock) in clientSessionCache then
 1716         tlsSock := openTlsSocket(sock, clientSessionCache[peerAddress(sock)]);
 1717       else
 1718         new_file.sock := sock;
 1719         new_file.parameters.isClient := TRUE;
 1720         new_file.parameters.hostName := hostName;
 1721         clientHello := genClientHello(new_file.parameters, "");
 1722         # showTlsMsg(clientHello);
 1723         write(sock, clientHello);
 1724         getTlsMsgRecord(sock, new_file.parseState);
 1725         # showTlsMsg(new_file.parseState.message);
 1726         if new_file.parseState.contentType = HANDSHAKE and
 1727             new_file.parseState.message[new_file.parseState.pos] = SERVER_HELLO then
 1728           processServerHello(new_file.parameters, new_file.parseState);
 1729           if new_file.parseState.alert <> CLOSE_NOTIFY then
 1730             sendAlertAndClose(new_file, new_file.parseState.alert);
 1731           else
 1732             tlsSock := negotiateSecurityParameters(new_file);
 1733           end if;
 1734         else
 1735           sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
 1736         end if;
 1737       end if;
 1738     end if;
 1739   end func;
 1740 
 1741 
 1742 (**
 1743  *  Return a connected TLS socket file based on the given ''sock''.
 1744  *  @param sock A connected internet socket file (client side).
 1745  *  @return an open TLS socket file, or [[null_file#STD_NULL|STD_NULL]]
 1746  *          if it could not be opened.
 1747  *  @exception MEMORY_ERROR An out of memory situation occurred.
 1748  *)
 1749 const func file: openTlsSocket (inout file: sock) is
 1750   return openTlsSocket (sock, "");
 1751 
 1752 
 1753 (**
 1754  *  Return a connected TLS socket file at a port at ''hostName''.
 1755  *  Here ''hostName'' is either a host name (e.g.: "www.example.org"),
 1756  *  or an IPv4 address in standard dot notation (e.g.: "192.0.2.235").
 1757  *  Operating systems supporting IPv6 may also accept an IPv6 address
 1758  *  in colon notation.
 1759  *  @return an open TLS socket file, or [[null_file#STD_NULL|STD_NULL]]
 1760  *          if it could not be opened.
 1761  *  @exception MEMORY_ERROR An out of memory situation occurred.
 1762  *)
 1763 const func file: openTlsSocket (in string: hostName, in integer: portNumber) is func
 1764   result
 1765     var file: tlsSock is STD_NULL;
 1766   local
 1767     var file: sock is STD_NULL;
 1768   begin
 1769     sock := openInetSocket(hostName, portNumber);
 1770     tlsSock := openTlsSocket(sock, hostName);
 1771   end func;
 1772 
 1773 
 1774 (**
 1775  *  Return a connected TLS socket file based on the given ''sock''.
 1776  *  @param sock A connected internet socket file (server side).
 1777  *  @param certificateAndKey Server certificate and corresponding private key.
 1778  *  @return an open TLS socket file, or [[null_file#STD_NULL|STD_NULL]]
 1779  *          if it could not be opened.
 1780  *  @exception MEMORY_ERROR An out of memory situation occurred.
 1781  *)
 1782 const func file: openServerTls (inout file: sock, in certAndKey: certificateAndKey) is func
 1783   result
 1784     var file: tlsSock is STD_NULL;
 1785   local
 1786     var tlsFile: new_file is tlsFile.value;
 1787     var string: clientHello is "";
 1788     var string: serverHello is "";
 1789     var string: certificate is "";
 1790     var string: serverKeyExchange is "";
 1791     var string: serverHelloDone is "";
 1792     var string: changeCipherSpec is "";
 1793     var string: finished is "";
 1794     var boolean: okay is TRUE;
 1795   begin
 1796     if sock <> STD_NULL then
 1797       new_file.sock := sock;
 1798       new_file.parameters.isClient := FALSE;
 1799       new_file.parameters.privateRsaCertificateKey := certificateAndKey.privateRsaKey;
 1800       new_file.parameters.privateEccCertificateKey := certificateAndKey.privateEccKey;
 1801       # Read and process the request from sock.
 1802       getTlsMsgRecord(sock, new_file.parseState);
 1803       if new_file.parseState.contentType = HANDSHAKE and
 1804           new_file.parseState.message[new_file.parseState.pos] = CLIENT_HELLO then
 1805         # writeln(literal(new_file.parseState.message));
 1806         # showTlsMsg(new_file.parseState.message);
 1807         processClientHello(new_file.parameters, new_file.parseState);
 1808         if new_file.parseState.alert <> CLOSE_NOTIFY then
 1809           sendAlertAndClose(new_file, new_file.parseState.alert);
 1810           okay := FALSE;
 1811         else
 1812           serverHello := genServerHello(new_file.parameters);
 1813           # showTlsMsg(serverHello);
 1814           write(sock, serverHello);
 1815           certificate := genCertificate(new_file.parameters, certificateAndKey.certList);
 1816           # showTlsMsg(certificate);
 1817           block
 1818             write(sock, certificate);
 1819           exception
 1820             catch FILE_ERROR:
 1821               # getTlsMsgRecord(sock, new_file.parseState);
 1822               # showTlsMsg(new_file.parseState.message);
 1823               okay := FALSE;
 1824           end block;
 1825           if okay and new_file.parameters.key_exchange_algorithm = EC_DIFFIE_HELLMAN then
 1826             serverKeyExchange := genServerKeyExchange(new_file.parameters);
 1827             # showTlsMsg(serverKeyExchange);
 1828             write(sock, serverKeyExchange);
 1829           end if;
 1830         end if;
 1831         if okay then
 1832           serverHelloDone := genServerHelloDone(new_file.parameters);
 1833           # showTlsMsg(serverHelloDone);
 1834           write(sock, serverHelloDone);
 1835           repeat
 1836             getTlsMsgRecord(sock, new_file.parseState);
 1837             # showTlsMsg(new_file.parseState.message);
 1838             if new_file.parseState.contentType = HANDSHAKE and
 1839                 new_file.parseState.message[new_file.parseState.pos] = CLIENT_KEY_EXCHANGE then
 1840               processClientKeyExchange(new_file.parameters, new_file.parseState);
 1841             end if;
 1842           until new_file.parseState.contentType = CHANGE_CIPHER_SPEC or
 1843                 new_file.parseState.contentType = ALERT or
 1844                 new_file.parseState.contentType = NO_MESSAGE;
 1845           if new_file.parseState.contentType = CHANGE_CIPHER_SPEC then
 1846             processChangeCipherSpec(new_file.parameters, new_file.parseState);
 1847             getTlsMsgRecord(sock, new_file.parseState);
 1848             if new_file.parseState.contentType = HANDSHAKE then  # Handshake with encoded Finished message
 1849               if tlsDecryptRecord(new_file.parameters, new_file.parseState) then
 1850                 # showTlsMsg(new_file.parseState.message);
 1851                 if new_file.parseState.message[new_file.parseState.pos] = FINISHED then
 1852                   processFinished(new_file.parameters, new_file.parseState);
 1853                   changeCipherSpec := genChangeCipherSpec(new_file.parameters);
 1854                   # showTlsMsg(changeCipherSpec);
 1855                   write(sock, changeCipherSpec);
 1856                   new_file.parameters.writeEncryptedRecords := TRUE;
 1857                   finished := genFinished(new_file.parameters);
 1858                   # showTlsMsg(finished);
 1859                   finished := tlsEncryptRecord(new_file.parameters, finished);
 1860                   block
 1861                     write(sock, finished);
 1862                   exception
 1863                     catch FILE_ERROR:
 1864                       # getTlsMsgRecord(sock, new_file.parseState);
 1865                       # tlsDecryptRecord(new_file.parameters, new_file.parseState);
 1866                       # showTlsMsg(new_file.parseState.message);
 1867                       okay := FALSE;
 1868                   end block;
 1869                   if okay then
 1870                     tlsSock := toInterface(new_file);
 1871                   end if;
 1872                 else
 1873                   sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
 1874                 end if;
 1875               else
 1876                 sendAlertAndClose(new_file, new_file.parseState.alert);
 1877               end if;
 1878             else
 1879               sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
 1880             end if;
 1881           else
 1882             sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
 1883           end if;
 1884         end if;
 1885       else
 1886         sendAlertAndClose(new_file, UNEXPECTED_MESSAGE);
 1887       end if;
 1888     end if;
 1889   end func;
 1890 
 1891 
 1892 (**
 1893  *  Close a tlsFile.
 1894  *  @exception FILE_ERROR A system function returns an error.
 1895  *)
 1896 const proc: close (inout tlsFile: aFile) is func
 1897   begin
 1898     sendAlertAndClose(aFile, CLOSE_NOTIFY);
 1899   end func;
 1900 
 1901 
 1902 (**
 1903  *  Determine the end-of-file indicator.
 1904  *  The end-of-file indicator is set if at least one request to read
 1905  *  from the socket failed. The socket functions ''getc'', ''gets'',
 1906  *  ''getln'' and ''getwd'' indicate the end-of-file situation by
 1907  *  setting ''bufferChar'' to [[char#EOF|EOF]].
 1908  *  @return TRUE if the end-of-file indicator is set, FALSE otherwise.
 1909  *)
 1910 const func boolean: eof (in tlsFile: inFile) is
 1911   return inFile.bufferChar = EOF;
 1912 
 1913 
 1914 const func string: getApplicationData (inout tlsFile: inFile) is func
 1915   result
 1916     var string: applicationData is "";
 1917   begin
 1918     getTlsMsgRecord(inFile.sock, inFile.parseState);
 1919     if inFile.parseState.contentType = APPLICATION_DATA then
 1920       if tlsDecryptRecord(inFile.parameters, inFile.parseState) then
 1921         # showTlsMsg(inFile.parseState.message);
 1922         applicationData := inFile.parseState.message[inFile.parseState.pos ..];
 1923         inFile.parseState.pos +:= inFile.parseState.length;
 1924       else
 1925         sendAlertAndClose(inFile, inFile.parseState.alert);
 1926       end if;
 1927     elsif inFile.parseState.contentType = ALERT then
 1928       if tlsDecryptRecord(inFile.parameters, inFile.parseState) then
 1929         # showTlsMsg(inFile.parseState.message);
 1930         close(inFile);
 1931       else
 1932         sendAlertAndClose(inFile, inFile.parseState.alert);
 1933       end if;
 1934     elsif inFile.parseState.contentType = CLIENT_HELLO then
 1935       sendAlertAndClose(inFile, NO_RENEGOTIATION);
 1936     elsif inFile.parseState.contentType = NO_MESSAGE then
 1937       close(inFile);
 1938     else
 1939       sendAlertAndClose(inFile, UNEXPECTED_MESSAGE);
 1940     end if;
 1941   end func;
 1942 
 1943 
 1944 (**
 1945  *  Write a [[string]] to a tlsFile.
 1946  *  @exception FILE_ERROR A system function returns an error.
 1947  *  @exception RANGE_ERROR The string contains a character that does
 1948  *             not fit into a byte.
 1949  *)
 1950 const proc: write (inout tlsFile: outFile, in string: stri) is func
 1951   local
 1952     const integer: maxStriLen is 2**14 - 1;
 1953     var integer: startIndex is 1;
 1954     var string: plain is "";
 1955     var string: message is "";
 1956   begin
 1957     # writeln("write(" <& literal(stri) <& ")");
 1958     repeat
 1959       plain := str(APPLICATION_DATA) &           # ContentType (index: 1)
 1960                outFile.parameters.tls_version &  # Version: 3.1
 1961                "\0;\0;" &                        # Length: filled later (index: 4)
 1962                stri[startIndex len maxStriLen];
 1963       plain @:= [4] int16AsTwoBytesBe(length(plain) - 5);
 1964       # showTlsMsg(plain);
 1965       message := tlsEncryptRecord(outFile.parameters, plain);
 1966       write(outFile.sock, message);
 1967       startIndex +:= maxStriLen;
 1968     until startIndex > length(stri);
 1969   end func;
 1970 
 1971 
 1972 (**
 1973  *  Write a [[string]] followed by end-of-line to ''outSocket''.
 1974  *  This function assures that string and '\n' are sent together.
 1975  *)
 1976 const proc: writeln (inout tlsFile: outFile, in string: stri) is func
 1977   begin
 1978     # writeln("writeln(" <& literal(stri) <& ")");
 1979     write(outFile, stri & "\n");
 1980   end func;
 1981 
 1982 
 1983 (**
 1984  *  Read a [[string]] with a maximum length from a tlsFile.
 1985  *  @return the string read.
 1986  *  @exception RANGE_ERROR The length is negative.
 1987  *  @exception MEMORY_ERROR Not enough memory to represent the result.
 1988  *)
 1989 const func string: gets (inout tlsFile: inFile, in integer: maxLength) is func
 1990   result
 1991     var string: striRead is "";
 1992   begin
 1993     if maxLength <= 0 then
 1994       if maxLength <> 0 then
 1995         raise RANGE_ERROR;
 1996       end if;
 1997     else
 1998       # writeln("gets(, " <& maxLength <& ") actual length: " <& length(inFile.readBuffer));
 1999       if inFile.readBuffer = "" and not eof(inFile.sock) then
 2000         inFile.readBuffer := getApplicationData(inFile);
 2001         # writeln("gets(, " <& maxLength <& ") actual length: " <& length(inFile.readBuffer));
 2002       end if;
 2003       if length(inFile.readBuffer) > maxLength then
 2004         striRead := inFile.readBuffer[.. maxLength];
 2005         inFile.readBuffer := inFile.readBuffer[succ(maxLength) ..];
 2006       else
 2007         striRead := inFile.readBuffer;
 2008         inFile.readBuffer := "";
 2009       end if;
 2010       if maxLength > 0 and striRead = "" and eof(inFile.sock) then
 2011         inFile.bufferChar := EOF;
 2012       end if;
 2013     end if;
 2014     # writeln("gets --> " <& literal(striRead));
 2015   end func;
 2016 
 2017 
 2018 (**
 2019  *  Read a line from a tlsFile.
 2020  *  The function accepts lines ending with '\n', "\r\n" or [[char#EOF|EOF]].
 2021  *  The line ending characters are not copied into the string.
 2022  *  That means that the '\r' of a "\r\n" sequence is silently removed.
 2023  *  When the function is left inFile.bufferChar contains '\n' or
 2024  *  [[char#EOF|EOF]].
 2025  *  @return the line read.
 2026  *  @exception MEMORY_ERROR Not enough memory to represent the result.
 2027  *)
 2028 const func string: getln (inout tlsFile: inFile) is func
 2029   result
 2030     var string: stri is "";
 2031   local
 2032     var integer: nlPos is 0;
 2033   begin
 2034     nlPos := pos(inFile.readBuffer, '\n');
 2035     while nlPos = 0 and not eof(inFile.sock) do
 2036       inFile.readBuffer &:= getApplicationData(inFile);
 2037       nlPos := pos(inFile.readBuffer, '\n');
 2038     end while;
 2039     if nlPos <> 0 then
 2040       if nlPos <> 1 and inFile.readBuffer[pred(nlPos)] = '\r' then
 2041         stri := inFile.readBuffer[.. nlPos - 2];
 2042       else
 2043         stri := inFile.readBuffer[.. pred(nlPos)];
 2044       end if;
 2045       inFile.readBuffer := inFile.readBuffer[succ(nlPos) ..];
 2046       inFile.bufferChar := '\n';
 2047     else
 2048       stri := inFile.readBuffer;
 2049       inFile.readBuffer := "";
 2050       inFile.bufferChar := EOF;
 2051     end if;
 2052     # writeln("getln --> " <& literal(stri));
 2053   end func;
 2054 
 2055 
 2056 const func string: getServerCertificate (in file: aFile, in integer: pos) is DYNAMIC;
 2057 
 2058 
 2059 const func string: getServerCertificate (in tlsFile: aFile, in integer: pos) is
 2060   return aFile.parameters.serverCertificates.certList[pos];