Image

Доведення коректності алгоритму шифрування RSA засобами The Coq Proof Assistant

Навчальний заклад: Комунальний заклад «Харківський науковий ліцей-інтернат «Обдарованість» Харківської обласної ради

Автор: Панов Максим Ігорович

Відділення: Математика

Секція: Прикладна математика

Область: Харківська

Опис:

Мета роботи – довести коректність алгоритму RSA, використовуючи The COQ Proof Assistant. Для досягнення мети дослідження були поставлені такі задачі: дати визначення криптографії, показати роботу алгоритму RSA, його особливості; розглянути зв’язок між математичними доведеннями і програмами – відповідність Карі-Говарда; ознайомитися зі створеними на основі цієї відповідності інструментами інтерактивного доведення теорем, зокрема з The COQ Proof Assistant; сформулювати засобами COQ алгоритм RSA та довести його коректність.