commit b623d869ddae1a0825c7093ec887db1b25bc75d3 Author: Nyeogmi Date: Sun Apr 6 21:37:49 2025 -0700 Horrifying prolog crypto, implementation 1 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).