Верификация криптографических протоколов на основе понятия наблюдаемой эквивалентности

В работе излагается модель криптографических протоколов, основанная на теории процессов с передачей сообщений. Показано, как можно использовать данную модель для решения задач верификации криптографических протоколов (то есть построения математических доказательств утверждений о том, что криптографические протоколы обладают заданными свойствами). В качестве примера таких свойств рассматриваются свойства целостности и секретности. Данные свойства определяются формально, как некоторые соотношения, выражаемые в терминах наблюдаемой эквивалентности процессов с передачей сообщений. Показаны примеры верификации данных свойств для некоторых криптографических протоколов.