From b623d869ddae1a0825c7093ec887db1b25bc75d3 Mon Sep 17 00:00:00 2001 From: Nyeogmi Date: Sun, 6 Apr 2025 21:37:49 -0700 Subject: [PATCH] Horrifying prolog crypto, implementation 1 --- binchunking.pl | 47 ++++++++++++++ chacha20.pl | 145 ++++++++++++++++++++++++++++++++++++++++++ chacha20_poly1305.pl | 110 ++++++++++++++++++++++++++++++++ chacha20_prim.pl | 33 ++++++++++ ciphertext.json | 6 ++ input.json | 4 ++ key.json | 1 + main.pl | 74 +++++++++++++++++++++ poly1305.pl | 69 ++++++++++++++++++++ roundtrip.json | 1 + start.bat | 2 + types.pl | 49 ++++++++++++++ xchacha20_poly1305.pl | 106 ++++++++++++++++++++++++++++++ 13 files changed, 647 insertions(+) create mode 100644 binchunking.pl create mode 100644 chacha20.pl create mode 100644 chacha20_poly1305.pl create mode 100644 chacha20_prim.pl create mode 100644 ciphertext.json create mode 100644 input.json create mode 100644 key.json create mode 100644 main.pl create mode 100644 poly1305.pl create mode 100644 roundtrip.json create mode 100644 start.bat create mode 100644 types.pl create mode 100644 xchacha20_poly1305.pl diff --git a/binchunking.pl b/binchunking.pl new file mode 100644 index 0000000..df83808 --- /dev/null +++ b/binchunking.pl @@ -0,0 +1,47 @@ +:- module(binchunking, [as_int_be/3, as_int_le/3, append_chunk/4, test_binchunking/0]). + +as_int_be(W, Bytes, V1) :- + ground(Bytes), reverse(RevBytes, Bytes), as_int_le(W, RevBytes, V1). +as_int_be(W, Bytes, V1) :- + ground(V1), as_int_le(W, RevBytes, V1), reverse(RevBytes, Bytes). + +as_int_le(0, [], 0) :- !. +as_int_le(W1, [B | Bytes], V1) :- + ground(W1), W1 > 0, succ(W0, W1), + ground(B), !, + as_int_le(W0, Bytes, V0), V1 is V0 * 256 + B. +as_int_le(W1, [B | Bytes], V1) :- + ground(W1), W1 > 0, succ(W0, W1), + ground(V1), !, + B is V1 mod 256, V0 is V1 div 256, as_int_le(W0, Bytes, V0). +as_int_le(W, Bytes, V) :- throw(invalid_as_int(W, Bytes, V)). + +append_chunk(Size, Chunk, Remaining, Total) :- + length(Chunk, Size), append(Chunk, Remaining, Total). +append_chunk(Size, Total, [], Total) :- + length(Total, L), 0 < L, L < Size. + +test_as_int :- + forall( + member(L/W = N, [ + []/0 = 0, + [0, 0]/2 = 0, + [255, 1]/2 = 511, + [255, 128]/2 = 33023 + ]), + ( + assertion( (as_int_le(W, L, N1), N1 = N) ), + assertion( (as_int_le(W, L1, N), L1 = L) ), + reverse(L, Q), + assertion( (as_int_be(W, Q, N1), N1 = N) ), + assertion( (as_int_be(W, Q1, N), Q1 = Q) ) + ) + ). + +test_append_chunk :- + assertion( (append_chunk(2, C, Rem, [a, b, c]), C = [a, b], Rem= [c]) ), + assertion( (append_chunk(3, C, Rem, [a, b, c]), C = [a, b, c], Rem= []) ). + +test_binchunking :- + test_as_int, + test_append_chunk. \ No newline at end of file diff --git a/chacha20.pl b/chacha20.pl new file mode 100644 index 0000000..6e663ed --- /dev/null +++ b/chacha20.pl @@ -0,0 +1,145 @@ +:- module(chacha20, [chacha20_block/5, chacha20_cipher/5, test_chacha20/0]). +:- use_module(chacha20_prim). +:- use_module(types). + +chacha20_block(Key, Nonce, Counter, State, Mixed) :- + assertion(is_chacha20_key(Key)), + assertion(is_chacha20_nonce(Nonce)), + assertion(is_chacha20_counter(Counter)), + u8s_to_u32s_le(Key, [K0, K1, K2, K3, K4, K5, K6, K7]), + expand_counter(Counter, [C0, C1]), + u8s_to_u32s_le(Nonce, [N0, N1]), + BlockStart = [ + % specified here: https://datatracker.ietf.org/doc/html/rfc7539 + 0x61707865, 0x3320646e, 0x79622d32, 0x6b206574, + K0, K1, K2, K3, + K4, K5, K6, K7, + C0, C1, N0, N1 + ], + % format("\n"), + % format("start block: "), print_hexlist(BlockStart), format("\n"), + chacha20_prim_u32(BlockStart, State), + % format("state block: "), print_hexlist(State), format("\n"), + maplist(mix_term, BlockStart, State, Mixed). + % format("mixed block: "), print_hexlist(Mixed), format("\n"), + % format("\n"). + +mix_term(X, Y, Z) :- Z is (X + Y) /\ 0xFFFFFFFF. + +chacha20_cipher(Key, Nonce, Counter, Text, Result) :- + assertion(is_chacha20_key(Key)), + assertion(is_chacha20_nonce(Nonce)), + assertion(is_chacha20_counter(Counter)), + assertion(is_u8s(Text)), + chacha20_cipher_impl(Key, Nonce, Counter, Text, Result). + +chacha20_cipher_impl(_, _, _, [],[]). +chacha20_cipher_impl(Key, Nonce, Counter, Text, Result) :- + append_chunk(64, TextPrefix, TextRemaining, Text), + compute_keystream(Key, Nonce, Counter, Keystream), + mix_keystream(Keystream, TextPrefix, ResultPrefix), + assertion(length(Keystream, 64)), + chacha20_cipher_impl(Key, Nonce, Counter + 1, TextRemaining, ResultRemaining), + append(ResultPrefix, ResultRemaining, Result). + +compute_keystream(Key, Nonce, Counter, Keystream) :- + chacha20_block(Key, Nonce, Counter, _, Mixed), + u8s_to_u32s_le(Keystream, Mixed). + +expand_counter(Counter, [C1, C2]) :- + C1 is Counter mod (1 << 32), + C2 is Counter div (1 << 32). + +mix_keystream(_, [], []). +mix_keystream([K|Key], [T|Text], [O|Out]) :- + O is K xor T, + mix_keystream(Key, Text, Out). +mix_keystream([], [_|_], _) :- throw(ran_out_of_keystream). + +test_chacha20 :- + test_compute_keystream, + test_mix_keystream, + test_e2e_short, + test_e2e_long. + +test_compute_keystream :- + % test vectors from here: https://datatracker.ietf.org/doc/html/rfc7539#appendix-A.1 + ZeroKey = [ + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 + ], + OneKey = [ + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1 + ], + HighKey = [ + 0, 0xff, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0 , 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 + ], + ZeroNonce = [0, 0, 0, 0, 0, 0, 0, 0], + TwoNonce = [0, 0, 0, 0, 0, 0, 0, 2], + forall( + member(example(K, N, Ctr) = Ks, [ + example(ZeroKey, ZeroNonce, 0) = [0x76, 0xb8, 0xe0, 0xad], + example(ZeroKey, ZeroNonce, 1) = [0x9f, 0x07, 0xe7, 0xbe], + example(OneKey, ZeroNonce, 1) = [0x3a, 0xeb, 0x52, 0x24], + example(HighKey, ZeroNonce, 2) = [0x72, 0xd5, 0x4d, 0xfb], + example(ZeroKey, TwoNonce, 0) = [0xc2, 0xc6, 0x4d, 0x37] + ]), + assertion(( + compute_keystream(K, N, Ctr, Ks2), + prefix(Ks, Ks2) + )) + ). + +test_mix_keystream :- + forall( + member(mix(Ks, Tx) = Result, [ + mix([0, 0, 0], []) = [], + mix([0, 0, 0], [0, 0, 0]) = [0, 0, 0], + mix([1, 2, 3], [8, 8, 8]) = [9, 10, 11], + mix([1, 2, 3], [9, 10, 11]) = [8, 8, 8] + ]), + assertion( mix_keystream(Ks, Tx, Result) ) + ). + +test_e2e_short :- + length(PlaintextBytes, 64), maplist(=(0), PlaintextBytes), + Ciphertext="76b8e0ada0f13d90405d6ae55386bd28bdd219b8a08ded1aa836efcc8b770dc7da41597c5157488d7724e03fb8d84a376a43b8f41518a11cc387b669b2ee6586", + hex_bytes(Ciphertext, CiphertextBytes), + zeros(32, Key), zeros(8, Nonce), + chacha20_cipher( + Key, Nonce, 0, + PlaintextBytes, + CiphertextCandidateBytes + ), + assertion(CiphertextBytes = CiphertextCandidateBytes), + chacha20_cipher( + Key, Nonce, 0, + CiphertextBytes, + PlaintextCandidateBytes + ), + assertion(PlaintextBytes = PlaintextCandidateBytes). + +test_e2e_long :- + Plaintext = "Any submission to the IETF intended by the Contributor for publication as all or part of an IETF Internet-Draft or RFC and any statement made within the context of an IETF activity is considered an \"IETF Contribution\". Such statements include oral statements in IETF sessions, as well as written and electronic communications made at any time or place, which are addressed to", + Ciphertext = "a3fbf07df3fa2fde4f376ca23e82737041605d9f4f4f57bd8cff2c1d4b7955ec2a97948bd3722915c8f3d337f7d370050e9e96d647b7c39f56e031ca5eb6250d4042e02785ececfa4b4bb5e8ead0440e20b6e8db09d881a7c6132f420e52795042bdfa7773d8a9051447b3291ce1411c680465552aa6c405b7764d5e87bea85ad00f8449ed8f72d0d662ab052691ca66424bc86d2df80ea41f43abf937d3259dc4b2d0dfb48a6c9139ddd7f76966e928e635553ba76c5c879d7b35d49eb2e62b0871cdac638939e25e8a1e0ef9d5280fa8ca328b351c3c765989cbcf3daa8b6ccc3aaf9f3979c92b3720fc88dc95ed84a1be059c6499b9fda236e7e818b04b0bc39c1e876b193bfe5569753f88128cc08aaa9b63d1a16f80ef2554d7189c411f5869ca52c5b83fa36ff216b9c1d30062bebcfd2dc5bce0911934fda79a86f6e698ced759c3ff9b6477338f3da4f9cd8514ea9982ccafb341b2384dd902f3d1ab7ac61dd29c6f21ba5b862f3730e37cfdc4fd806c22f221", + string_bytes(Plaintext, PlaintextBytes, utf8), + hex_bytes(Ciphertext, CiphertextBytes), + Key = [ + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, + 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1 + ], + Nonce = [0, 0, 0, 0, 0, 0, 0, 2], + chacha20_cipher( + Key, Nonce, 1, + PlaintextBytes, + CiphertextCandidateBytes + ), + assertion(CiphertextBytes = CiphertextCandidateBytes), + chacha20_cipher( + Key, Nonce, 1, + CiphertextBytes, + PlaintextCandidateBytes + ), + assertion(PlaintextBytes = PlaintextCandidateBytes). \ No newline at end of file diff --git a/chacha20_poly1305.pl b/chacha20_poly1305.pl new file mode 100644 index 0000000..4968cd6 --- /dev/null +++ b/chacha20_poly1305.pl @@ -0,0 +1,110 @@ +:- module(chacha20_poly1305, [ + chacha20_poly1305_encrypt/7, + chacha20_poly1305_decrypt/7, + test_chacha20_poly1305/0 +]). +:- use_module(poly1305). + +% mostly from https://datatracker.ietf.org/doc/html/rfc8439#section-2.8 +chacha20_poly1305_encrypt(Aad, Key, Nonce, CounterOffset, Text, Ciphertext, Tag) :- + assertion(is_u8s(Aad)), + assertion(is_chacha20_key(Key)), + assertion(is_chacha20_nonce(Nonce)), + assertion(is_u8s(Text)), + + poly1305_generate_key(Key, Nonce, CounterOffset, Poly1305Key), + + Counter is CounterOffset + 1, + chacha20_cipher(Key, Nonce, Counter, Text, Ciphertext), + + create_mac_data(Aad, Ciphertext, MacData), + poly1305(Poly1305Key, MacData, Tag), + + assertion(is_u8s(Ciphertext)), + assertion(is_poly1305_tag(Tag)). + +chacha20_poly1305_decrypt(Aad, Key, Nonce, CounterOffset, Text, Ciphertext, Tag) :- + assertion(is_u8s(Aad)), + assertion(is_chacha20_key(Key)), + assertion(is_chacha20_nonce(Nonce)), + assertion(is_u8s(Ciphertext)), + assertion(is_poly1305_tag(Tag)), + + poly1305_generate_key(Key, Nonce, CounterOffset, Poly1305Key), + + create_mac_data(Aad, Ciphertext, MacData), + poly1305(Poly1305Key, MacData, ExpectedTag), + + assertion(ExpectedTag = Tag), + Counter is CounterOffset + 1, + chacha20_cipher(Key, Nonce, Counter, Ciphertext, Text), + + assertion(is_u8s(Text)). + +create_mac_data(Aad, Ciphertext, MacData) :- + pad16(Aad, Aad16), + pad16(Ciphertext, Ciphertext16), + length(Aad, AadLength), + length(Ciphertext, CiphertextLength), + as_int_le(8, AadLengthBytes, AadLength), + as_int_le(8, CiphertextLengthBytes, CiphertextLength), + append([ + Aad, Aad16, + Ciphertext, Ciphertext16, + AadLengthBytes, CiphertextLengthBytes + ], MacData). + +pad16(X, Padding) :- + length(X, Len), + PaddingNeeded is (16 - Len mod 16) mod 16, + zeros(PaddingNeeded, Padding). + +poly1305_generate_key(Key, Nonce, CounterOffset, Poly1305Key) :- + chacha20_block(Key, Nonce, CounterOffset, _, Mixed), + u8s_to_u32s_le(Bytes, Mixed), + assertion(length(Bytes, 64)), + length(Poly1305Key, 32), + prefix(Poly1305Key, Bytes). + +test_chacha20_poly1305 :- + test_pad16, + test_poly1305_generate_key, + test_e2e. + +test_pad16 :- + assertion( pad16([], []) ), + assertion( pad16([1], [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]) ). + +test_poly1305_generate_key :- + hex_bytes("808182838485868788898a8b8c8d8e8f909192939495969798999a9b9c9d9e9f", Key), + hex_bytes("0001020304050607", Nonce), + hex_bytes("8ad5a08b905f81cc815040274ab29471a833b637e3fd0da508dbb8e2fdd1a646", ExpectedPolyKey), + poly1305_generate_key(Key, Nonce, 0, PolyKey), + assertion(PolyKey = ExpectedPolyKey). + + +test_e2e :- + hex_bytes("50515253c0c1c2c3c4c5c6c7", Aad), + hex_bytes("808182838485868788898a8b8c8d8e8f909192939495969798999a9b9c9d9e9f", Key), + hex_bytes("4041424344454647", Nonce), + string_bytes( + "Ladies and Gentlemen of the class of \x27\99: If I could offer you only one tip for the future, sunscreen would be it.", + Text, utf8 + ), + CounterOffset is 7 << 32, % rfc8439 expects a 3 byte nonce, so we sneak it into the counter like this so we can reuse the test vector + poly1305_generate_key(Key, Nonce, CounterOffset, PolyKey), + chacha20_poly1305_encrypt(Aad, Key, Nonce, CounterOffset, Text, Ciphertext, Tag), + + hex_bytes("7bac2b252db447af09b67a55a4e955840ae1d6731075d9eb2a9375783ed553ff", ExpectedPolyKey), + + hex_bytes("d31a8d34648e60db7b86afbc53ef7ec2a4aded51296e08fea9e2b5a736ee62d63dbea45e8ca9671282fafb69da92728b1a71de0a9e060b2905d6a5b67ecd3b3692ddbd7f2d778b8c9803aee328091b58fab324e4fad675945585808b4831d7bc3ff4def08e4b7a9de576d26586cec64b6116", ExpectedCiphertext), + hex_bytes("1ae10b594f09e26a7e902ecbd0600691", ExpectedTag), + + assertion(PolyKey = ExpectedPolyKey), + assertion(Ciphertext = ExpectedCiphertext), + assertion(Tag = ExpectedTag), + + chacha20_poly1305_decrypt( + Aad, Key, Nonce, CounterOffset, Plaintext, ExpectedCiphertext, ExpectedTag + ), + assertion(Plaintext = Text). \ No newline at end of file diff --git a/chacha20_prim.pl b/chacha20_prim.pl new file mode 100644 index 0000000..742590f --- /dev/null +++ b/chacha20_prim.pl @@ -0,0 +1,33 @@ +:- module(chacha20_prim, [chacha20_prim_u32/2]). + +chacha20_prim_u32(B0, B1) :- + assertion(is_chacha20_block(B0)), + chacha(10, B0, B1). + +chacha(0, D, D). +chacha(N1) --> {N1 > 0, succ(N0, N1)}, round, chacha(N0). + +round --> + qround([0, 4, 8, 12]), qround([1, 5, 9, 13]), + qround([2, 6, 10, 14]), qround([3, 7, 11, 15]), + qround([0, 5, 10, 15]), qround([1, 6, 11, 12]), + qround([2, 7, 8, 13]), qround([3, 4, 9, 14]). + +qround([A, B, C, D]) --> + at([A, B], qadd), at([D, A], qxor), at([D], rot_l32(16)), + at([C, D], qadd), at([B, C], qxor), at([B], rot_l32(12)), + at([A, B], qadd), at([D, A], qxor), at([D], rot_l32(8)), + at([C, D], qadd), at([B, C], qxor), at([B], rot_l32(7)). + +at([IxA], Pred, L0, LN) :- + nth0(IxA, L0, A0, LRem), + call(Pred, A0, A1), trunc_32(A1, A2), + nth0(IxA, LN, A2, LRem), !. + +at([IxA, IxB], Pred, L0, LN) :- + nth0(IxB, L0, B), + at([IxA], call(Pred, B), L0, LN). + +qadd(B, A0, A1) :- A1 is A0 + B. +qxor(B, A0, A1) :- A1 is A0 xor B. +rot_l32(Amt, A0, A1) :- A1 is (A0 << Amt) \/ (A0 >> (32 - Amt)). \ No newline at end of file diff --git a/ciphertext.json b/ciphertext.json new file mode 100644 index 0000000..d23d22a --- /dev/null +++ b/ciphertext.json @@ -0,0 +1,6 @@ +{ + "aad":"hello", + "ciphertext":"cf27fda2d96899900d62a13cee78eebc741f545d8f7f9413c9c3d30c1f068e3a21401a6e0c", + "nonce":"c229d14ee30af88070a708657c09f699f75e6d69c757cf4c", + "tag":"94219fa2d6078bbdf10ac258c8232746" +} \ No newline at end of file diff --git a/input.json b/input.json new file mode 100644 index 0000000..d63b8e4 --- /dev/null +++ b/input.json @@ -0,0 +1,4 @@ +{ + "aad": "hello", + "message": "BEEP BOOP! I'm a bat. How about that?" +} \ No newline at end of file diff --git a/key.json b/key.json new file mode 100644 index 0000000..df2f2ac --- /dev/null +++ b/key.json @@ -0,0 +1 @@ +{"key":"bats are neat (32 byte demo str)"} \ No newline at end of file diff --git a/main.pl b/main.pl new file mode 100644 index 0000000..3fa3d96 --- /dev/null +++ b/main.pl @@ -0,0 +1,74 @@ +:- initialization(main, main). +:- use_module(library(http/json)). +:- use_module(binchunking). +:- use_module(chacha20). +:- use_module(chacha20_poly1305). +:- use_module(poly1305). +:- use_module(types). +:- use_module(xchacha20_poly1305). + +test :- + test_binchunking, + test_chacha20, + test_chacha20_poly1305, + test_poly1305, + test_xchacha20_poly1305. + +main([Key, Command, Input, Output]) :- + processor(Command, Processor), !, + test, + json_read_file(Key, KeyValue), + json_read_file(Input, InputValue), + + call(Processor, KeyValue, InputValue, OutputValue), !, + + json_write_file(Output, OutputValue). + +json_read_file(Fname, Value) :- + open(Fname, read, Stream), + json_read_dict(Stream, Value), + close(Stream). + +json_write_file(Fname, Value) :- + open(Fname, write, Stream), + json_write_dict(Stream, Value), + close(Stream). + + +processor('-e', encrypt). +processor('-d', decrypt). + +nonce(Nonce) :- crypto_n_random_bytes(24, Nonce). + +encrypt(_{key: Key}, _{aad: Aad, message: Plaintext}, Out) :- + nonce(NonceBytes), + string_bytes(Key, KeyBytes, utf8), assertion(is_xchacha20_key(KeyBytes)), + string_bytes(Aad, AadBytes, utf8), + string_bytes(Plaintext, PlaintextBytes, utf8), + xchacha20_poly1305_encrypt( + AadBytes, KeyBytes, NonceBytes, PlaintextBytes, CiphertextBytes, TagBytes + ), + hex_bytes(Nonce, NonceBytes), + hex_bytes(Ciphertext, CiphertextBytes), + hex_bytes(Tag, TagBytes), + Out = _{ + nonce: Nonce, + aad: Aad, + ciphertext: Ciphertext, + tag: Tag + }. + +decrypt(_{key: Key}, _{nonce: Nonce, aad: Aad, ciphertext: Ciphertext, tag: Tag}, Out) :- + string_bytes(Key, KeyBytes, utf8), assertion(is_chacha20_key(KeyBytes)), + string_bytes(Aad, AadBytes, utf8), + hex_bytes(Nonce, NonceBytes), + hex_bytes(Ciphertext, CiphertextBytes), + hex_bytes(Tag, TagBytes), + xchacha20_poly1305_decrypt( + AadBytes, KeyBytes, NonceBytes, PlaintextBytes, CiphertextBytes, TagBytes + ), + string_bytes(Plaintext, PlaintextBytes, utf8), + Out = _{ + aad: Aad, + message: Plaintext + }. \ No newline at end of file diff --git a/poly1305.pl b/poly1305.pl new file mode 100644 index 0000000..56e7d6d --- /dev/null +++ b/poly1305.pl @@ -0,0 +1,69 @@ +:- module(poly1305, [poly1305/3, test_poly1305/0]). +:- use_module(binchunking). +:- use_module(types). + +% docs: https://www.rfc-editor.org/rfc/rfc7539.html#section-2.5.2 + +poly1305(Key, Text, Tag) :- + assertion(is_poly1305_key(Key)), + assertion(is_u8s(Text)), + parse_key(Key, R, Pad), + + poly1305_impl(R, Pad, 0, TagInt, Text), + as_int_le(16, Tag, TagInt), + assertion(is_poly1305_tag(Tag)). + +parse_key(Key, R, Pad) :- + length(RBytes, 16), + length(PadBytes, 16), + append(RBytes, PadBytes, Key), + as_int_le(16, RBytes, R0), + as_int_le(16, PadBytes, Pad), + R is R0 /\ 0x0FFFFFFC0FFFFFFC0FFFFFFC0FFFFFFF. + +prime(P) :- P is 2^130-5. +poly1305_impl(_, Pad, Acc, Result, []) :- + Result is (Acc + Pad) /\ (1<<128 - 1). +poly1305_impl(R, Pad, Acc, Result, Text) :- + prime(Prime), + append_chunk(16, BytesTrunc, Remaining, Text), + append(BytesTrunc, [1], Bytes), + length(Bytes, W), + as_int_le(W, Bytes, Block), + Acc2 is ((Acc + Block) * R) mod Prime, !, + poly1305_impl(R, Pad, Acc2, Result, Remaining). + +test_poly1305 :- + test_parse_key, + test_main. + +test_parse_key :- + parse_key( + [ + 0x85, 0xd6, 0xbe, 0x78, 0x57, 0x55, 0x6d, 0x33, + 0x7f, 0x44, 0x52, 0xfe, 0x42, 0xd5, 0x06, 0xa8, + 0x01, 0x03, 0x80, 0x8a, 0xfb, 0x0d, 0xb2, 0xfd, + 0x4a, 0xbf, 0xf6, 0xaf, 0x41, 0x49, 0xf5, 0x1b + ], + R, + Pad + ), + assertion(Pad = 0x1bf54941aff6bf4afdb20dfb8a800301), + assertion(R = 0x806d5400e52447c036d555408bed685). + +test_main :- + string_bytes("Cryptographic Forum Research Group", Bytes, utf8), + poly1305( + [ + 0x85, 0xd6, 0xbe, 0x78, 0x57, 0x55, 0x6d, 0x33, + 0x7f, 0x44, 0x52, 0xfe, 0x42, 0xd5, 0x06, 0xa8, + 0x01, 0x03, 0x80, 0x8a, 0xfb, 0x0d, 0xb2, 0xfd, + 0x4a, 0xbf, 0xf6, 0xaf, 0x41, 0x49, 0xf5, 0x1b + ], + Bytes, + Tag + ), + assertion(Tag = [ + 0xa8, 0x06, 0x1d, 0xc1, 0x30, 0x51, 0x36, 0xc6, + 0xc2, 0x2b, 0x8b, 0xaf, 0x0c, 0x01, 0x27, 0xa9 + ]). \ No newline at end of file diff --git a/roundtrip.json b/roundtrip.json new file mode 100644 index 0000000..38db9ef --- /dev/null +++ b/roundtrip.json @@ -0,0 +1 @@ +{"aad":"hello","message":"BEEP BOOP! I'm a bat. How about that?"} \ No newline at end of file diff --git a/start.bat b/start.bat new file mode 100644 index 0000000..1d32c08 --- /dev/null +++ b/start.bat @@ -0,0 +1,2 @@ +swipl main.pl key.json -e input.json ciphertext.json +swipl main.pl key.json -d ciphertext.json roundtrip.json \ No newline at end of file diff --git a/types.pl b/types.pl new file mode 100644 index 0000000..7d31e64 --- /dev/null +++ b/types.pl @@ -0,0 +1,49 @@ +:- module(types, [ + is_xchacha20_key/1, is_xchacha20_nonce/1, is_xchacha20_counter/1, + is_chacha20_key/1, is_chacha20_nonce/1, is_chacha20_counter/1, + is_hchacha20_hash/1, + is_chacha20_block/1, + is_poly1305_key/1, is_poly1305_tag/1, + is_u8s/1, is_u32s/1, + is_u8/1, is_u32/1, + trunc_8/2, trunc_32/2, + zeros/2, + u8s_to_u32s_le/2, + print_hexlist/1 +]). + +is_xchacha_poly1305_key(K) :- is_xchacha20_key(K). +is_xchacha_poly1305_iv(K) :- is_xchacha20_key(K). + +is_xchacha20_key(K) :- is_chacha20_key(K). +is_xchacha20_nonce(N) :- is_u8s(N), length(N, 24). +is_xchacha20_counter(C) :- is_chacha20_counter(C). + +is_chacha20_key(K) :- is_u8s(K), length(K, 32). +is_chacha20_nonce(N) :- is_u8s(N), length(N, 8). +is_chacha20_counter(C) :- ground(C), Top is 1<<64, 0 =< C, C < Top. + +is_hchacha20_hash(H) :- is_u8s(H), length(H, 32). +is_chacha20_block(B) :- is_u32s(B), length(B, 16). + +is_poly1305_key(K) :- is_u8s(K), length(K, 32). +is_poly1305_tag(T) :- is_u8s(T), length(T, 16). + +is_u8s(Xs) :- ground(Xs), is_list(Xs), forall(member(X, Xs), is_u8(X)). +is_u32s(Xs) :- ground(Xs), is_list(Xs), forall(member(X, Xs), is_u32(X)). + +is_u8(X) :- trunc_8(X, X). +is_u32(X) :- trunc_32(X, X). + +trunc_8(A, X) :- A >= 0, X is A /\ 0xFF. +trunc_32(A, X) :- A >= 0, X is A /\ 0xFFFFFFFF. + +zeros(N, Lst) :- length(Lst, N), maplist(=(0), Lst). + +u8s_to_u32s_le([], []). +u8s_to_u32s_le([A, B, C, D|U8s], [ABCD|U32s]) :- + as_int_le(4, [A, B, C, D], ABCD), + u8s_to_u32s_le(U8s, U32s). + + +print_hexlist(Xs) :- forall(member(X, Xs), format("~16r ", X)). \ No newline at end of file diff --git a/xchacha20_poly1305.pl b/xchacha20_poly1305.pl new file mode 100644 index 0000000..9abd1df --- /dev/null +++ b/xchacha20_poly1305.pl @@ -0,0 +1,106 @@ +:- module(xchacha20_poly1305, [ + test_xchacha20_poly1305/0, + xchacha20_poly1305_encrypt/6, + xchacha20_poly1305_decrypt/6 +]). +:- use_module(chacha20_poly1305). +:- use_module(chacha20_prim). + + +xchacha20_poly1305_encrypt(Aad, Key, Nonce, Text, Ciphertext, Tag) :- + assertion(is_u8s(Aad)), + assertion(is_xchacha20_key(Key)), + assertion(is_xchacha20_nonce(Nonce)), + assertion(is_u8s(Text)), + + split_nonce(N0, N1, Nonce), + hchacha20(Key, N0, Subkey), + chacha20_poly1305_encrypt(Aad, Subkey, N1, 0, Text, Ciphertext, Tag), + + assertion(is_u8s(Ciphertext)), + assertion(is_poly1305_tag(Tag)). + +xchacha20_poly1305_decrypt(Aad, Key, Nonce, Text, Ciphertext, Tag) :- + assertion(is_u8s(Aad)), + assertion(is_xchacha20_key(Key)), + assertion(is_xchacha20_nonce(Nonce)), + assertion(is_u8s(Ciphertext)), + assertion(is_u8s(Tag)), + + split_nonce(N0, N1, Nonce), + hchacha20(Key, N0, Subkey), + chacha20_poly1305_decrypt(Aad, Subkey, N1, 0, Text, Ciphertext, Tag), + + assertion(is_u8s(Text)). + +split_nonce(N0, N1, Nonce) :- + length(N0, 16), + length(N1, 8), + append(N0, N1, Nonce). + +hchacha20(Key, Nonce, Hash) :- + assertion(is_chacha20_key(Key)), + assertion(is_u8s(Nonce)), length(Nonce, 16), + u8s_to_u32s_le(Key, K), + u8s_to_u32s_le(Nonce, N), + hchacha20_impl(K, N, H), + u8s_to_u32s_le(Hash, H), + assertion(is_hchacha20_hash(Hash)). + +hchacha20_impl(Key, Nonce, Hash) :- + hchacha20_block(Key, Nonce, [ + H0, H1, H2, H3, + _, _, _, _, + _, _, _, _, + H4, H5, H6, H7 + ]), + Hash = [H0, H1, H2, H3, H4, H5, H6, H7]. + +hchacha20_block(Key, Nonce, Output) :- + Key = [K0, K1, K2, K3, K4, K5, K6, K7], + Nonce = [N0, N1, N2, N3], + Input = [ + 0x61707865, 0x3320646e, 0x79622d32, 0x6b206574, + K0, K1, K2, K3, + K4, K5, K6, K7, + N0, N1, N2, N3 + ], + chacha20_prim_u32(Input, Output). + +test_xchacha20_poly1305 :- + test_hchacha20, + test_e2e. + +test_hchacha20 :- + hchacha20_block( + [ + 0x03020100, 0x07060504, 0x0b0a0908, 0x0f0e0d0c, + 0x13121110, 0x17161514, 0x1b1a1918, 0x1f1e1d1c + ], + [0x09000000, 0x4a000000, 0x00000000, 0x27594131], + Output + ), + assertion( + Output = [ + 0x423b4182, 0xfe7bb227, 0x50420ed3, 0x737d878a, + 0x0aa76448, 0x7954cdf3, 0x846acd37, 0x7b3c58ad, + 0x77e35583, 0x83e77c12, 0xe0076a2d, 0xbc6cd0e5, + 0xd5e4f9a0, 0x53a8748a, 0x13c42ec1, 0xdcecd326 + ] + ). + +test_e2e :- + hex_bytes("50515253c0c1c2c3c4c5c6c7", Aad), + hex_bytes("808182838485868788898a8b8c8d8e8f909192939495969798999a9b9c9d9e9f", Key), + hex_bytes("404142434445464748494a4b4c4d4e4f5051525354555657", Nonce), + string_bytes( + "Ladies and Gentlemen of the class of \x27\99: If I could offer you only one tip for the future, sunscreen would be it.", + Text, utf8 + ), + hex_bytes("bd6d179d3e83d43b9576579493c0e939572a1700252bfaccbed2902c21396cbb731c7f1b0b4aa6440bf3a82f4eda7e39ae64c6708c54c216cb96b72e1213b4522f8c9ba40db5d945b11b69b982c1bb9e3f3fac2bc369488f76b2383565d3fff921f9664c97637da9768812f615c68b13b52e", ExpectedCiphertext), + hex_bytes("c0875924c1c7987947deafd8780acf49", ExpectedTag), + + xchacha20_poly1305_encrypt(Aad, Key, Nonce, Text, Ciphertext, Tag), + + assertion(Ciphertext = ExpectedCiphertext), + assertion(Tag = ExpectedTag).