Формализация свойств безопасности криптографических протоколов с помощью логики линейного времени

Abstract

Представлены основные свойства безопасности криптографических протоколов с помощью аппарата логики линейного времени LTL, а также приведен пример автомата Бюхи, построенного на основе формулы LTL.

Conducted theoretical research of applying instruments of linear temporal logic to formalize the security properties of cryptographic protocols and developing the Buchi automata based on LTL-formulas.