Practice description

AlgorithmsComplexityPractice.txt

Transalg
    https://gitlab.com/transalg/transalg/-/tree/master/bin%2Fwin32
    Файл Transalg.exe (727 KB)

Minisat
    https://yadi.sk/mail?hash=EG3Zg4JxooK0wVez3O2In5Ok7lE5yzDIg1OEF94fY03uNjj3pzXgWhxDUYKbznMeq%2FJ6bpmRyOJonT3VoXnDag%3D%3D

CriptoMiniSat
    https://github.com/msoos/cryptominisat/releases
    Файл cryptominisat5-win-amd64-nogauss.exe (1.54 MB)

Задание и таблица вариантов
    https://docs.google.com/spreadsheets/d/1NOkm183J26NC1ybnQI07fmfwwBarQ0ek474F4AQFI9Y/edit?usp=sharing
    Проверены результаты по генератору Геффе
    * Добавлено семестровое задание по генератору переменного шага (ASG). Вкладка ASG64.

Остальные материалы
    Добавлен файл Geffe.alg с примером TA-программы для генератора Геффе
    Добавлен файл InversionProblemSolutionInstruction.txt, содержащий инструкцию по решению задачи обращения фрагмента ключевого потока

Geffe.alg

define len 100;

__in bit regA[19];
__in bit regB[22];
__in bit regC[23];

__out bit result[100];


bit func(bit x, bit y, bit z) {
	return x & y ^ (y ^ 1) & z;
}

bit shift_regA() {
	bit x = regA[9] ^ regA[15] ^ regA[17] ^ regA[18];
	bit y = regA[18];
	int i;
	for (i = 18; i >= 1; i = i - 1)
		regA[i] = regA[i - 1];
	regA[0] = x;
	return y;
}

bit shift_regB() {
	bit x = regB[12] ^ regB[16] ^ regB[20] ^ regB[21];
	bit y = regB[21];
	int i;
	for (i = 21; i >= 1; i = i - 1)
		regB[i] = regB[i - 1];
	regB[0] = x;
	return y;
}

bit shift_regC() {
	bit x = regC[15] ^ regC[19] ^ regC[21] ^ regC[22];
	bit y = regC[22];
	int i;
	for (i = 22; i >= 1; i = i - 1)
		regC[i] = regC[i - 1];
	regC[0] = x;
	return y;
}

void main()
{

	int i;
	for (i = 0; i < len; i = i + 1)
		result[i] = func(shift_regA(), shift_regB(), shift_regC());

}

InversionProblemSolutionInstruction.txt

Дано описание генератора ключевого потока и некоторое число битов ключевого потока. Найти вход генератора.
Работаем в папке C:\SAT\.

1. По данному описанию генератора ключевого потока написать TA-программу (файл generator.alg)
2. Построить по данной программе КНФ в формате DIMACS с помощью Transalg (файл generator.cnf)
    2.1. Скачать файл Transalg.exe по ссылке из файла описания практики
    2.2. В командной строке вызвать комманду:
        C:\SAT> Transalg.exe  -i generator.alg  -o generator.cnf
3. Сделать копию файла generator.cnf (файл generator_out.cnf).
   Добавить в него значения известных битов ключевого потока в виде однолитеральных дизъюнктов.
   Дизъюнкты можно получить по двоичной последовательности, например, с помощью программы на C++ (https://ideone.com/8m60Lp).
4. Запустить решатель на полученной КНФ
    4.1. Скачать решатель (файл Minisat2.2.exe или cryptominisat5-win-amd64-nogauss.exe по ссылке из файла описания практики).
    4.2. Запустить решатель из командной строки
         Для Minisat (результат записывается в файл out.cnf):
         C:\SAT> Minisat2.2.exe  generator_out.cnf  out.cnf
         Для CryptoMiniSat (результат записывается в консоль):
         C:\SAT> cryptominisat5-win-amd64-nogauss.exe  generator_out.cnf
5. Выделить в результате множество дизъюнктов, отвечающих значениям переменных входа (первые несколько переменных).
   Получить по описанию дизъюнктов двоичную последовательность, например, с помощью программы на C++. (https://ideone.com/KMRtW4)

SemesterTask.txt

РЕШЕНИЕ ЗАДАЧИ ОБРАЩЕНИЯ ФРАГМЕНТА КЛЮЧЕВОГО ПОТОКА ГЕНЕРАТОРА ПЕРЕМЕННОГО ШАГА (ALTERNATING STEP GENERATOR, ASG)

Описание генератора можно прочитать на странице Википедии: ru.wikipedia.org/wiki/Потоковый_шифр#Генератор_переменного_шага
В данном задании требуется использовать генератор с длиной ключа 64 бита и выходную последовательность (ключевой поток) длиной 100 битов.
Кратко генератор можно описать следующим образом.

Генератор состоит из трёх регистров сдвига с линейной обратной связью (РСЛОС). Назовём их LFSR1, LFSR2 и LFSR3. Длины регистров 19, 22 и 23 бита соответственно.
Секретный ключ длины 64 бита составлен из битов начальных состояний LFSR1, LFSR2 и LFSR3 соответственно.
Процесс шифрования состоит из 100 итераций. Каждая итерация содержит следующие шаги.
1. Сдвиг регистра LFSR1;
2. Если последний бит LFSR1 равен 1, то сдвигается LFSR2, иначе сдвигается LFSR3;
3. xor последних битов LFSR2 и LFSR3 добавляется к выходной последовательности (ключевому потоку).
Новое значение первого бита каждого регистра после сдвига определяется соответствующим полиномом обратной связи.

Биты фрагмента ключевого потока и полиномы обратной связи для каждого РСЛОС указаны в таблице (docs.google.com/spreadsheets/d/1NOkm183J26NC1ybnQI07fmfwwBarQ0ek474F4AQFI9Y/edit?usp=sharing).

Решение задачи обращения генератора ключевого потока подразумевает нахождение секретного ключа по известному фрагменту ключевого потока.
Алгоритм выполнения данной семестровой работы во многом повторяет алгоритм решения задачи обращения для генератора Геффе (файл InversionProblemSolutionInstruction.txt).

Сначала необходимо выбрать вариант, не выбранный ещё никем из одногруппников.
Для этого в таблице во вкладке ASG64 надо в виде комментария оставить свои данные в столбце ФИО в строке с выбранным вариантом.

Далее описано выполнение задания в ОС семейства Windows (для других ОС см. комментарий в конце файла).
Работаем в папке C:\SAT\.
1. По данному описанию генератора ключевого потока (см. выше) написать TA-программу (файл generator.alg)
2. Построить по данной программе КНФ в формате DIMACS с помощью Transalg (файл generator.cnf)
    2.1. Скачать файл Transalg.exe по ссылке (gitlab.com/transalg/transalg/-/tree/master/bin%2Fwin32)
    2.2. В командной строке вызвать комманду:
        C:\SAT> Transalg.exe  -i generator.alg  -o generator.cnf
3. Сделать копию файла generator.cnf (файл generator_out.cnf).
   Добавить в него значения известных битов ключевого потока в виде однолитеральных дизъюнктов (последние 100 переменных).
   Дизъюнкты можно получить по двоичной последовательности, например, с помощью программы на C++ (ideone.com/8m60Lp).
4. Запустить решатель на полученной КНФ
    4.1. Скачать решатель: файл Minisat2.2.exe (yadi.sk/mail?hash=EG3Zg4JxooK0wVez3O2In5Ok7lE5yzDIg1OEF94fY03uNjj3pzXgWhxDUYKbznMeq%2FJ6bpmRyOJonT3VoXnDag%3D%3D) или cryptominisat5-win-amd64-nogauss.exe (github.com/msoos/cryptominisat/releases)
    4.2. Запустить решатель из командной строки
         Для Minisat (результат записывается в файл out.cnf):
         C:\SAT> Minisat2.2.exe  generator_out.cnf  out.cnf
         Для CryptoMiniSat (результат выводится в консоль):
         C:\SAT> cryptominisat5-win-amd64-nogauss.exe  generator_out.cnf
   Если на этом шаге был получен UNSAT, то причин может быть несколько:
    1) неправильно подставлены значения битов выхода в шаблонную КНФ, например, неверно указаны номера переменных выхода.
       В этом случае решатель обычно завершает выполнение достаточно быстро.
    2) неправильно написана программа (generator.alg) и, как следствие, неправильно составлена шаблонная КНФ.
       В этом случае, если значения битов выхода были подставлены верно, решатель обычно выполняется долго, прежде чем вывести ответ.

5. Выделить в результате множество дизъюнктов, отвечающих значениям переменных входа (первые 64 переменных).
   Получить по описанию дизъюнктов двоичную последовательность, например, с помощью программы на C++ (ideone.com/KMRtW4)
6. Написать отчёт в свободной форме о выполнении семестрового задания

Полученную в результате двоичную строку для проверки необходимо вставить в таблицу, в столбец для ответа в строку с выбранным вариантом.
Ответ так же надо оставить в виде комментария.

Комментарий для студентов, у которых нет возможности выполнить работу на Windows.
При выполнении работы от ОС может зависить только файл SAT решателя и файл собранной утилиты Transalg.

1) Где взять подходящий SAT решатель?
Для Linux есть версии уже собранных бинарных файлов Minisat (например, по ссылке файл MiniSat_v1.14_linux на странице minisat.se/MiniSat.html). На Ubuntu и Debian можно установить через apt (onstartup.ru/nauka/minisat-2).
Вообще на любой ОС можно использовать CryptoMiniSat из браузера (msoos.org/2013/09/minisat-in-your-browser).

2) Как запустить Transalg?
Для Linux есть собранный вариант утилиты (x64 или x86) по ссылке (gitlab.com/transalg/transalg/-/tree/master/bin).
Для остальных ОС можно использовать эмулятор Linux в браузере (cocalc.com/doc/terminal.html).
Для этого необходимо загрузить туда Transalg x64 (ссылка выше) и файл .alg программы из локального хранилища.
После загрузки файлов Transalg и asg64.alg выполнить в терминале две строки:
chmod u+x Transalg                   # настройка прав для запуска программы
./Transalg -i asg64.alg -o asg64.cnf # создание КНФ 
После успешного завершения программы можно скачать файл asg64.cnf, содержащий необходимую КНФ.

Можно также установить эмулятор Linux или Windows на компьютер.
В крайнем случае придётся просить запустить Transalg у одногруппников.