'// OTRv3 Authenticated Key Exchange (AKE)' Comment.Single '\n' Text.Whitespace '// https://otr.cypherpunks.ca/Protocol-v3-4.1.1.html' Comment.Single '\n\n' Text.Whitespace 'attacker' Name.Builtin '[' Punctuation 'passive' Literal.String ']' Punctuation '\n\n' Text.Whitespace '// Setup' Comment.Single '\n' Text.Whitespace 'principal' Name.Builtin ' ' Text.Whitespace 'Bob' Literal.String '[' Punctuation '\n ' Text.Whitespace 'knows' Name.Builtin ' ' Text.Whitespace 'private' Keyword.Constant ' ' Text.Whitespace 'priv_b' Name.Variable '\n ' Text.Whitespace 'pub_b' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'G' Name.Function '^' Punctuation 'priv_b' Name.Variable '\n' Text.Whitespace ']' Punctuation '\n' Text.Whitespace 'Bob' Literal.String ' ' Text.Whitespace '→' Punctuation ' ' Text.Whitespace 'Alice' Literal.String ':' Punctuation ' ' Text.Whitespace '[' Punctuation 'pub_b' Name.Variable ']' Punctuation '\n' Text.Whitespace 'principal' Name.Builtin ' ' Text.Whitespace 'Alice' Literal.String '[' Punctuation '\n ' Text.Whitespace 'knows' Name.Builtin ' ' Text.Whitespace 'private' Keyword.Constant ' ' Text.Whitespace 'priv_a' Name.Variable '\n ' Text.Whitespace 'pub_a' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'G' Name.Function '^' Punctuation 'priv_a' Name.Variable '\n' Text.Whitespace ']' Punctuation '\n' Text.Whitespace 'Alice' Literal.String ' ' Text.Whitespace '→' Punctuation ' ' Text.Whitespace 'Bob' Literal.String ':' Punctuation ' ' Text.Whitespace '[' Punctuation 'pub_a' Name.Variable ']' Punctuation '\n\n' Text.Whitespace '// Go!' Comment.Single '\n' Text.Whitespace 'principal' Name.Builtin ' ' Text.Whitespace 'Bob' Literal.String '[' Punctuation '\n ' Text.Whitespace 'generates' Name.Builtin ' ' Text.Whitespace 'r' Name.Variable ',' Punctuation ' ' Text.Whitespace 'x' Name.Variable '\n ' Text.Whitespace 'g_x' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'G' Name.Function '^' Punctuation 'x' Name.Variable '\n ' Text.Whitespace 'enc_gx' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'ENC' Name.Function '(' Punctuation 'r' Name.Variable ',' Punctuation ' ' Text.Whitespace 'g_x' Name.Variable ')' Punctuation '\n ' Text.Whitespace 'hash_gx' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'HASH' Name.Function '(' Punctuation 'g_x' Name.Variable ')' Punctuation '\n' Text.Whitespace ']' Punctuation '\n\n' Text.Whitespace 'Bob' Literal.String ' ' Text.Whitespace '→' Punctuation ' ' Text.Whitespace 'Alice' Literal.String ':' Punctuation ' ' Text.Whitespace 'enc_gx' Name.Variable ',' Punctuation ' ' Text.Whitespace 'hash_gx' Name.Variable '\n\n' Text.Whitespace 'principal' Name.Builtin ' ' Text.Whitespace 'Alice' Literal.String '[' Punctuation '\n ' Text.Whitespace 'generates' Name.Builtin ' ' Text.Whitespace 'y' Name.Variable '\n ' Text.Whitespace 'g_y' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'G' Name.Function '^' Punctuation 'y' Name.Variable '\n' Text.Whitespace ']' Punctuation '\n\n' Text.Whitespace 'Alice' Literal.String ' ' Text.Whitespace '→' Punctuation ' ' Text.Whitespace 'Bob' Literal.String ':' Punctuation ' ' Text.Whitespace 'g_y' Name.Variable '\n\n' Text.Whitespace 'principal' Name.Builtin ' ' Text.Whitespace 'Bob' Literal.String ' ' Text.Whitespace '[' Punctuation '\n ' Text.Whitespace 's' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'g_y' Name.Variable '^' Punctuation 'x' Name.Variable '\n ' Text.Whitespace 'c' Name.Variable ',' Punctuation ' ' Text.Whitespace 'c_' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'HKDF' Name.Function '(' Punctuation 's' Name.Variable ',' Punctuation ' ' Text.Whitespace 'nil' Name.Function ',' Punctuation ' ' Text.Whitespace 'nil' Name.Function ')' Punctuation '\n ' Text.Whitespace 'm1' Name.Variable ',' Punctuation ' ' Text.Whitespace 'm2' Name.Variable ',' Punctuation ' ' Text.Whitespace 'm1_' Name.Variable ',' Punctuation ' ' Text.Whitespace 'm2_' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'HKDF' Name.Function '(' Punctuation 'nil' Name.Function ',' Punctuation ' ' Text.Whitespace 's' Name.Variable ',' Punctuation ' ' Text.Whitespace 'nil' Name.Function ')' Punctuation '\n ' Text.Whitespace 'generates' Name.Builtin ' ' Text.Whitespace 'keyid_b' Name.Variable '\n ' Text.Whitespace 'Mb' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'MAC' Name.Function '(' Punctuation 'm1' Name.Variable ',' Punctuation ' ' Text.Whitespace 'CONCAT' Name.Function '(' Punctuation 'g_x' Name.Variable ',' Punctuation ' ' Text.Whitespace 'g_y' Name.Variable ',' Punctuation ' ' Text.Whitespace 'pub_b' Name.Variable ',' Punctuation ' ' Text.Whitespace 'keyid_b' Name.Variable ')' Punctuation ')' Punctuation '\n ' Text.Whitespace 'Xb' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'CONCAT' Name.Function '(' Punctuation 'pub_b' Name.Variable ',' Punctuation ' ' Text.Whitespace 'keyid_b' Name.Variable ',' Punctuation ' ' Text.Whitespace 'SIGN' Name.Function '(' Punctuation 'priv_b' Name.Variable ',' Punctuation ' ' Text.Whitespace 'Mb' Name.Variable ')' Punctuation ')' Punctuation '\n ' Text.Whitespace 'enc_c_x_b' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'ENC' Name.Function '(' Punctuation 'c' Name.Variable ',' Punctuation ' ' Text.Whitespace 'Xb' Name.Variable ')' Punctuation '\n ' Text.Whitespace 'mac_mc2_enc_c_x_b' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'MAC' Name.Function '(' Punctuation 'm2' Name.Variable ',' Punctuation ' ' Text.Whitespace 'ENC' Name.Function '(' Punctuation 'c' Name.Variable ',' Punctuation ' ' Text.Whitespace 'Xb' Name.Variable ')' Punctuation ')' Punctuation '\n' Text.Whitespace ']' Punctuation '\n\n' Text.Whitespace 'Bob' Literal.String ' ' Text.Whitespace '→' Punctuation ' ' Text.Whitespace 'Alice' Literal.String ':' Punctuation ' ' Text.Whitespace 'r' Name.Variable ',' Punctuation ' ' Text.Whitespace 'enc_c_x_b' Name.Variable ',' Punctuation ' ' Text.Whitespace 'mac_mc2_enc_c_x_b' Name.Variable '\n\n' Text.Whitespace 'principal' Name.Builtin ' ' Text.Whitespace 'Alice' Literal.String '[' Punctuation '\n ' Text.Whitespace 'dec_gx' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'DEC' Name.Function '(' Punctuation 'r' Name.Variable ',' Punctuation ' ' Text.Whitespace 'enc_gx' Name.Variable ')' Punctuation '\n ' Text.Whitespace '_' Name.Function ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'ASSERT' Name.Function '(' Punctuation 'HASH' Name.Function '(' Punctuation 'dec_gx' Name.Variable ')' Punctuation ',' Punctuation ' ' Text.Whitespace 'hash_gx' Name.Variable ')' Punctuation '?' Punctuation '\n ' Text.Whitespace 's_' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'dec_gx' Name.Variable '^' Punctuation 'y' Name.Variable '\n ' Text.Whitespace 'c_alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'c__alice' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'HKDF' Name.Function '(' Punctuation 's_' Name.Variable ',' Punctuation ' ' Text.Whitespace 'nil' Name.Function ',' Punctuation ' ' Text.Whitespace 'nil' Name.Function ')' Punctuation '\n ' Text.Whitespace 'm1_alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'm2_alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'm1__alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'm2__alice' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'HKDF' Name.Function '(' Punctuation 'nil' Name.Function ',' Punctuation ' ' Text.Whitespace 's_' Name.Variable ',' Punctuation ' ' Text.Whitespace 'nil' Name.Function ')' Punctuation '\n ' Text.Whitespace '_' Name.Function ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'ASSERT' Name.Function '(' Punctuation 'mac_mc2_enc_c_x_b' Name.Variable ',' Punctuation ' ' Text.Whitespace 'MAC' Name.Function '(' Punctuation 'm2_alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'enc_c_x_b' Name.Variable ')' Punctuation ')' Punctuation '?' Punctuation '\n ' Text.Whitespace 'xb_alice' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'DEC' Name.Function '(' Punctuation 'c_alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'enc_c_x_b' Name.Variable ')' Punctuation '\n ' Text.Whitespace 'pub_b_alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'keyd_b_alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'sig_b_mb_alice' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'SPLIT' Name.Function '(' Punctuation 'xb_alice' Name.Variable ')' Punctuation '\n ' Text.Whitespace 'mb_alice' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'MAC' Name.Function '(' Punctuation 'm1_alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'CONCAT' Name.Function '(' Punctuation 'dec_gx' Name.Variable ',' Punctuation ' ' Text.Whitespace 'g_y' Name.Variable ',' Punctuation ' ' Text.Whitespace 'pub_b_alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'keyd_b_alice' Name.Variable ')' Punctuation ')' Punctuation '\n ' Text.Whitespace '_' Name.Function ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'SIGNVERIF' Name.Function '(' Punctuation 'pub_b_alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'mb_alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'sig_b_mb_alice' Name.Variable ')' Punctuation '?' Punctuation '\n ' Text.Whitespace 'generates' Name.Builtin ' ' Text.Whitespace 'keyid_a' Name.Variable '\n ' Text.Whitespace 'ma' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'MAC' Name.Function '(' Punctuation 'm1__alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'CONCAT' Name.Function '(' Punctuation 'g_y' Name.Variable ',' Punctuation ' ' Text.Whitespace 'dec_gx' Name.Variable ',' Punctuation ' ' Text.Whitespace 'pub_a' Name.Variable ',' Punctuation ' ' Text.Whitespace 'keyid_a' Name.Variable ')' Punctuation ')' Punctuation '\n ' Text.Whitespace 'xa' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'CONCAT' Name.Function '(' Punctuation 'pub_a' Name.Variable ',' Punctuation ' ' Text.Whitespace 'keyid_a' Name.Variable ',' Punctuation ' ' Text.Whitespace 'SIGN' Name.Function '(' Punctuation 'priv_a' Name.Variable ',' Punctuation ' ' Text.Whitespace 'ma' Name.Variable ')' Punctuation ')' Punctuation '\n ' Text.Whitespace 'enc_c__x_a' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'ENC' Name.Function '(' Punctuation 'c__alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'xa' Name.Variable ')' Punctuation '\n ' Text.Whitespace 'mac_m2_enc_c__xa' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'MAC' Name.Function '(' Punctuation 'm2__alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'ENC' Name.Function '(' Punctuation 'c__alice' Name.Variable ',' Punctuation ' ' Text.Whitespace 'xa' Name.Variable ')' Punctuation ')' Punctuation '\n' Text.Whitespace ']' Punctuation '\n\n' Text.Whitespace 'Alice' Literal.String ' ' Text.Whitespace '→' Punctuation ' ' Text.Whitespace 'Bob' Literal.String ':' Punctuation ' ' Text.Whitespace 'enc_c__x_a' Name.Variable ',' Punctuation ' ' Text.Whitespace 'mac_m2_enc_c__xa' Name.Variable '\n\n' Text.Whitespace 'principal' Name.Builtin ' ' Text.Whitespace 'Bob' Literal.String '[' Punctuation '\n ' Text.Whitespace '_' Name.Function ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'ASSERT' Name.Function '(' Punctuation 'mac_m2_enc_c__xa' Name.Variable ',' Punctuation ' ' Text.Whitespace 'MAC' Name.Function '(' Punctuation 'm2_' Name.Variable ',' Punctuation ' ' Text.Whitespace 'enc_c__x_a' Name.Variable ')' Punctuation ')' Punctuation '?' Punctuation '\n ' Text.Whitespace 'xa_bob' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'DEC' Name.Function '(' Punctuation 'c_' Name.Variable ',' Punctuation ' ' Text.Whitespace 'enc_c__x_a' Name.Variable ')' Punctuation '\n ' Text.Whitespace 'pub_a_bob' Name.Variable ',' Punctuation ' ' Text.Whitespace 'keyid_a_bob' Name.Variable ',' Punctuation ' ' Text.Whitespace 'sig_a_ma_bob' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'SPLIT' Name.Function '(' Punctuation 'xa_bob' Name.Variable ')' Punctuation '\n ' Text.Whitespace 'ma_bob' Name.Variable ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'MAC' Name.Function '(' Punctuation 'm1_' Name.Variable ',' Punctuation ' ' Text.Whitespace 'CONCAT' Name.Function '(' Punctuation 'g_y' Name.Variable ',' Punctuation ' ' Text.Whitespace 'g_x' Name.Variable ',' Punctuation ' ' Text.Whitespace 'pub_a_bob' Name.Variable ',' Punctuation ' ' Text.Whitespace 'keyid_a_bob' Name.Variable ')' Punctuation ')' Punctuation '\n ' Text.Whitespace '_' Name.Function ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'SIGNVERIF' Name.Function '(' Punctuation 'pub_a_bob' Name.Variable ',' Punctuation ' ' Text.Whitespace 'ma_bob' Name.Variable ',' Punctuation ' ' Text.Whitespace 'sig_a_ma_bob' Name.Variable ')' Punctuation '?' Punctuation '\n ' Text.Whitespace '_' Name.Function ' ' Text.Whitespace '=' Punctuation ' ' Text.Whitespace 'ASSERT' Name.Function '(' Punctuation 'pub_a_bob' Name.Variable ',' Punctuation ' ' Text.Whitespace 'pub_a' Name.Variable ')' Punctuation '?' Punctuation '\n' Text.Whitespace ']' Punctuation '\n\n' Text.Whitespace 'queries' Name.Builtin ' ' Text.Whitespace '[' Punctuation '\n ' Name.Variable 'equivalence?' Keyword.Pseudo ' ' Text.Whitespace 's' Name.Variable ',' Punctuation ' ' Text.Whitespace 's_' Name.Variable '\n ' Name.Variable 'confidentiality?' Keyword.Pseudo ' ' Text.Whitespace 's' Name.Variable '\n ' Name.Variable 'freshness?' Keyword.Pseudo ' ' Text.Whitespace 's' Name.Variable '\n\n ' Name.Variable 'equivalence?' Keyword.Pseudo ' ' Text.Whitespace 'pub_b' Name.Variable ',' Punctuation ' ' Text.Whitespace 'pub_b_alice' Name.Variable '\n ' Name.Variable 'equivalence?' Keyword.Pseudo ' ' Text.Whitespace 'pub_a' Name.Variable ',' Punctuation ' ' Text.Whitespace 'pub_a_bob' Name.Variable '\n' Name.Variable ']' Punctuation '\n' Text.Whitespace