Институт системного программирования им. В.П. Иванникова РАН
О формальной верификации криптографических протоколов с использованием spi-исчисления.
Авторы
Аннотация
Spi-исчисление было введено как расширение pi-исчисления Р. Милнера за счет обогащения последнего специальными термами и действиями, соответствующими выполнению криптографических операций. Одна из главных особенностей, отличающих spi-исчисление от традиционных алгебр процессов, состоит в том, что каналы связи между процессами могут являться переменными величинами, и их имена могут передаваться в ходе обменов сообщениями между процессами. Другую особенность составляет операция сокрытия имени, позволяющая вводить новые свободные имена, отличные от всех ранее использованных имен, и операция репликации P, позволяющая многократно воспроизводить процесс P. spi-исчисление позволяет достаточно точно описывать значительное число криптографических протоколов.
Вместе с тем, наличие простой операционной семантики делает spi-исчисление весьма удачной математической моделью для формального анализа сложных протоколов. Предложен новый подход к символьному представлению знаний противника для решения задачи проверки тестовой эквивалентности процессов spi-исчисления, а также алгоритм проверки тестовой эквивалентности для процессов без операции репликации. Предложенный алгоритм позволяет проверить отличимость знаний противника за линейное время и существенно упрощает проверку тестовой эквивалентности процессов spi исчисления при верификации протоколов.
Издание
Труды второй всероссийской конференции «Методы и средства обработки информации», 2005, Изд-во ф-та ВМК МГУ Москва, с. 373-379.
Научная группа
Все публикации за 2005 год
Все публикации