Инструменты пользователя

Инструменты сайта


examination:mszki:question34

Проблема выделения безопасного сеансового ключа для пары компьютеров (или людей) в сети настолько фундаментальна, что стала причиной многих исследований. Некоторые исследования заключались в разработке протоколов. Это, в свою очередь, привело к появлению более важной и интересной задачи: формальному анализу протоколов проверки подлинности и обмена ключами. Иногда прорехи в протоколах, кажущихся вполне надежными, обнаруживались спустя много лет пoсле их разработки, и разработчикам потребовались средства, позволяющие сразу же проверять безопасность протокола. Хотя большая часть этого инструментария применима и к более общим криптографическим протoколам, особое внимание уделялось проверке подлинности и обмену ключами.

Существует четыре основных подхода к анализу криптографических протоколов:

  1. Моделирование и проверка работы протокола с использованием языков описания и средств проверки, не разработанных специально для анализа криптографических протоколов.
  2. Создание экспертных систем, позволяющих конструктору протокола разрабатывать и исследовать различные сценарии.
  3. Выработка требований к семейству протоколов, используя некую логику для анализа понятий «знание» и «доверие».
  4. Разработка формальных методов, основанных на записи свойств криптографических систем в алгебраическом виде.

Первый из подходов пытается доказать правильность протокола, рассматривая его как обычную компьютеpную программу. Ряд исследователей представляют протокол как конечный автомат, другие используют расширения методов исчисления предиката первого порядка, а третьи для анализа протоколов используют языки описания. Однако, доказательство правильности отнюдь не является доказательством безопасности, и этот подход потерпел неудачу при анализе многих «дырявых» протоколов . И хотя его применение поначалу широко изучалось, с ростом популярности третьего из подходов работы в этой области были пeреориентированы.

Во втором подходе для определения того, может ли протокол перейти в нежелательное состояние (например, потеря ключа), используются экспертные системы. Хотя этот подход дает лучшие результаты при поиске «дыр», он не гарантирует безопасности и не предоставляет методик разработки вскрытий . Он хорош для проверки того, содержит ли протокол конкретную «дыру», но вряд ли способен обнаружить неизвестные «дыры» в протоколе .

Третий подход гораздо популярнее. Он был впервые введен Майклом Бэрроузом, Мартином Абэди и Роджером Неедхэмом. Они разработали формальную логическую модель для анализа знания и доверия, названную БАН-логикой БАН-логика является наиболее широко распространена при анализе протоколов проверки подлинности. Она рассматривает подлинность как функцию от цeлостности и новизны, используя логические правила для отслеживания состояния этих атрибутов на протяжении всего протокола. Хотя были предложены различные варианты и расширения, большинство разработчиков пр o-токолов до сих пор обращаются к оригинальной работе.

БАН-логика не предоставляет доказательство безопасности, она может только рассуждать о проверке подлинности. Она является простой, прямолинейной логикой, легкой в применении и полезной при поиске «дыр» . Вот некоторые предложения БАН-логики:

  • A считает X (A действует, как если бы X являлось истиной )
  • A видит X (Кто-то послал сообщение, содержащее X, А, который может прочитать и снова передать X - возможно после дешифрирования )
  • A сказал X (В некоторый момент времени A послал сообщение, которое содержит предложение X Не известно, как давно было послано сообщение, и было ли оно послано в течении текущего выполнения протокола Известно, что A считал X, когда говорил X )

И так далее. БАН-логика также предоставляет правила для рассуждения о доверии протоколу. Для доказательства чего-либо в протоколе или для ответа на какие-то вопросы к логическим предложениям о протоколе можно применить эти правила. Например, одним из правил является правило о значении сообщения:

Если A считает, что у A и B общий секретный ключ, К, и A видит X, шифрованное К, и A не шифровала Хc помощью К, TO A считает, что B сказал X

Другим является правило подтверждения метки времени:

Если A считает, что X могло быть сказано только недавно, и, что B X когда-то сказал X, TO A считает, что B считает X

БАН-анализ делится на четыре этапа:

  • Преобразуйте протокол к идеальной форме, используя описанные выше предложения.
  • Добавьте все предположения о начальном состоянии протокола.
  • Присоедините логические формулы к предложениям, получая утверждения о состоянии системы после каждого предложения.
  • Примените логические постулаты к утверждениям и предположениям, чтобы раскрыть состояние доверия участников протокола.

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

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

examination/mszki/question34.txt · Последние изменения: 2014/01/15 08:20 (внешнее изменение)