pyrex/xchacha20_pl
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Horrifying prolog crypto, implementation 1

Browse Source
This commit is contained in:
Pyrex 2025-04-06 21:37:49 -07:00
commit b623d869dd
13 changed files with 647 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

47
binchunking.pl Normal file
View File

@ -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.

145
chacha20.pl Normal file
View File

@ -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).

110
chacha20_poly1305.pl Normal file
View File

@ -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).

33
chacha20_prim.pl Normal file
View File

@ -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)).

6
ciphertext.json Normal file
View File

@ -0,0 +1,6 @@
{
"aad":"hello",
"ciphertext":"cf27fda2d96899900d62a13cee78eebc741f545d8f7f9413c9c3d30c1f068e3a21401a6e0c",
"nonce":"c229d14ee30af88070a708657c09f699f75e6d69c757cf4c",
"tag":"94219fa2d6078bbdf10ac258c8232746"
}

4
input.json Normal file
View File

@ -0,0 +1,4 @@
{
"aad": "hello",
"message": "BEEP BOOP! I'm a bat. How about that?"
}

1
key.json Normal file
View File

@ -0,0 +1 @@
{"key":"bats are neat (32 byte demo str)"}

74
main.pl Normal file
View File

@ -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
}.

69
poly1305.pl Normal file
View File

@ -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
]).

1
roundtrip.json Normal file
View File

@ -0,0 +1 @@
{"aad":"hello","message":"BEEP BOOP! I'm a bat. How about that?"}

2
start.bat Normal file
View File

@ -0,0 +1,2 @@
swipl main.pl key.json -e input.json ciphertext.json
swipl main.pl key.json -d ciphertext.json roundtrip.json

49
types.pl Normal file
View File

@ -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)).

106
xchacha20_poly1305.pl Normal file
View File

@ -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).