ИСТИНА

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