Научная литература
booksshare.net -> Добавить материал -> Криптография -> Венбо Мао -> "Современная криптография" -> 256

Современная криптография - Венбо Мао

Венбо Мао Современная криптография. Под редакцией Клюшиной Д.А. — М. : Издательский дом Вильямс, 2005. — 768 c.
ISBN 5-8459-0847-7
Скачать (прямая ссылка): sovremennaya_kriptografiya.djvu
Предыдущая << 1 .. 250 251 252 253 254 255 < 256 > 257 258 259 260 261 262 .. 311 >> Следующая

вмешательство человека, хотя в некоторых случаях они имеют более широкое применение. Этот подход развивается двумя школами исследователей: вычисли-» телями и символистами. Вычислители стремятся выразить свойства стойкости: с помощью измерения вероятности, а исследование правильности протокола сво-< дится к доказательству определенной теоремы. Довольно часто в доказательствах стойкости используется метод редукции атаки к решению общепринятых трудноразрешимых задач из теории вычислительной сложности (см. главы 14 и 15). Символисты, к которым относятся специалисты по компьютерным наукам, выра-* жают свойства стойкости в виде множества абстрактных символов, допускающих определенные манипуляции, иногда путем применения логических правил, ишн гда — с помощью механического средства для доказательства теорем. Результатом] этих манипуляций должен быть ответ ДА или НЕТ.
В рамках второго подхода считается, что любой протокол аутентификации» выбранный наугад, тщательно разработанный или имеющий математическое дон казательство стойкости, все равно может содержать ошибку. Ведь формально! доказательство правильности демонстрирует лишь, что протокол соответствуем множеству установленных желательных свойств. Вполне возможно, что таком протокол окажется скомпрометированным, если его дефект в процессе доказя тельства правильности не был учтен. Таким образом, этот подход направлен на исчерпывающий анализ всех возможных ошибок. Для формализации протокоЛ представляется в виде системы с конечным множеством состояний, которую ча! сто разбивают на частичные протоколы, выполняемые разными пользователям» (включая Злоумышленника). Ошибку можно описать с помощью терминов общег! характера. Например, при анализе секретности сообщений неправильное состо| яние протокола может возникнуть, если Злоумышленник получает некую ча информации, а при аутентификации сущностей неправильное состояние возника4 ет, если посторонний пользователь получает права, которыми обладает законны, пользователь. Этот подход тесно связан с формальным анализом сложных систем используемым в компьютерных науках. По этой причине для исследования npoi токолов аутентификации часто применяются автоматические средства анализа. \
17.1.1 Структурная схема главы
Техническая часть главы начинается с формализации описания протоколам В разделе 17.2 рассматривается метод последовательного уточнения специфика^ ций протокола аутентификации. Затем от средств формального описания прото| колов аутентификации мы перейдем к методам их анализа. В разделе 17.3 описы! вается метод доказательства, основанный на вычислительной модели, в которое исследование сводится к доказательству определенной математической теоремы. Раздел 17.4 посвящен методам доказательства стойкости протоколов с помощью манипуляции логическими символами. Кроме того, в этом разделе излагается
Глава 17. Формальные методы анализа протоколов аутентификации 635
логический подход и метод анализа стойкости протоколов, основанный на доказательствах теорем. В разделе 17.5 описываются методы формального анализа протоколов с помощью систем с конечным множеством состояний и поиска системных ошибок. Раздел 17.6 содержит обзор недавних работ, образующих мост между вычислительными и логическими методами доказательства правильности протоколов аутентификации.
17.2 Формальное описание протоколов аутентификации
Для начала покажем необходимость формального описания протоколов аутентификации. Спецификация протокола должна стать неотъемлемой частью любого формального метода анализа сложных систем. Если такой системой является протокол аутентификации, необходимо более точное описание применения криптографических преобразований.
Как показано в главах 2 и 11, многие протоколы аутентификации используют исключительно шифрование, и по этой причине стало общепринятым обозначать шифрование в рамках этих протоколов символами {М}к. Это обозначение относится к части зашифрованного текста: чтобы создать его, отправитель должен выполнить шифрование, а, чтобы извлечь сообщение М, получатель должен выполнить расшифровку. Демонстрация этих криптографических возможностей доказывает, что пользователь владеет секретным ключом, т.е. идентифицирует его.
Таким образом, может показаться, что идея аутентификации с помощью шифрования довольно проста.
Однако на самом деле эта простота обманчива. Неверное применение этого механизма выявляет дефекты, присущие многим протоколам. В этом разделе мы продемонстрируем наиболее распространенные ошибки при использовании шифрования для аутентификации, а затем предложим метод разработки протоколов, основанный на последовательном уточнении криптографических преобразований.
17.2.1 Непригодность механизма
шифрования-расшифровки при аутентификации
В разделе 11.4.1.5 были перечислены два "нестандартных" механизма создания протоколов аутентификации, основанных на шифровании. В этих механизмах отправитель порождает зашифрованнный текст {М}к и посылает его по назначению. Подлинный получатель имеет секретный ключ, позволяющий выполнить расшифровку и вернуть отправителю компонент, извлеченный из зашифрованного текста. Возвращенный компонент сообщения, часто содержащий идентификатор
Предыдущая << 1 .. 250 251 252 253 254 255 < 256 > 257 258 259 260 261 262 .. 311 >> Следующая

Реклама

c1c0fc952cf0704ad12d6af2ad3bf47e03017fed

Есть, чем поделиться? Отправьте
материал
нам
Авторские права © 2009 BooksShare.
Все права защищены.
Rambler's Top100

c1c0fc952cf0704ad12d6af2ad3bf47e03017fed