2. Аналіз протоколу з використанням ban–логіки

2. 1. Постулати ban–логіки

Логіка Берроуза-Абаді-Нидхема (BAN-логіка) – це формальна логічна модель для аналізу знання і довіри, широко використовувана при аналізі протоколів автентифікації.

Основна ідея BAN-логіки в тому, що при аналізі подібних протоколів в першу чергу слідує звернути увагу на те, як сторони, які беруть участь в процесі автентифікації, сприймають інформацію – що вони приймають на довіру, а що до певного часу їм відомо або може бути виведено логічним шляхом з доступних для них фактів[6].

Зазвичай протоколи автентифікації описуються шляхом послідовного перерахування повідомлень, що передаються між учасниками протоколу. На кожному кроці описується вміст повідомлень, а також вказується його відправник та отримувач. BAN-логіка розглядає справжність повідомлення як функцію від його цілісності і новизни, використовуючи логічні правила для відслідковування стану цих атрибутів на протязі всього протоколу.

У BAN-логіки існує три типи об'єктів: учасники, ключі шифрування і формули, їх зв'язують. При формальному аналізі протоколу кожне повідомлення перетвориться в логічну формулу; потім логічні формули зв'язуються твердженнями. Тим самим, BAN-логіка в чому схожа з логікою Хо’ара. Єдиною логічною операцією, яка застосовується в даній логіці, являється кон'юнкція. Також вводяться різні предикати, наприклад, що встановлюють відносини між учасниками і висловлювати (відношення довіри, юрисдикції і т.д.) або виражають будь-які властивості висловлювань (таких, як свіжість, тобто твердження, що висловлювання отримано недавно).

Як і будь-яка формальна логіка, BAN-логіка забезпечена аксіомами і правилами виведення. Формальний аналіз протоколу полягає в доказі деякого набору тверджень, вираженого формулами BAN-логіки, за допомогою правил виводу. Наприклад, мінімальна вимога добудь-якого протоколу автентифікації полягає в наступному:обидва учасники повинні повірити в те, що вони знайшли секретний ключ для обміну інформацією один з одним.

Постулати, що застосовуються в BAN-логіці:

1. P |≡ X – Р вірить у те, що Х – істинно;

1. P sees X – хто-небудь послав Р повідомлення, що містить Х і Р може прочитати і повторити Х (можливо після розшифрування);

2. P said X – Р коли-набудь посилав повідомлення, що містить Х і при цьому Р довіряв Х, в момент його передавання;

3. P |=>X – Р має права на Х;

4. #X – Х не було використано в попередніх кроках протоколу;

5. – P i Q розділяють між собою ключ К і відповідно P i Q довіряють один одному;

6. – Р має відкритий ключ К, що відповідає секретному ключу К-1, який ніколи не буде розкритий іншими учасниками криптопротоколу;

7. – секретна формула Х відома тільки P i Q і вони можуть використовувати її для ідентифікації один одного;

8. {X}_Kfrom P – формула Х зашифрована на ключі К, що належить Р.

2. Аналіз протоколу Wide-mouthed Frog

Розглядається простий протокол автентифікації – Wide-mouthedFrog (протокол широкоротої жаби) – який дозволяє двум сторонам, Алісі і Бобу встановити захищене зєднання, використовуючи сервер Тренд, якому вони обоє довіряють.

Сторони Аліса і Боб володіють ключами K_as і K_bs, для захищеного звязку з сервером Тренд, що на мові BAN-логіки може бути виражено як:

Аліса|≡Аліса←K_as →Тренд

Тренд|≡Аліса←K_as →Тренд

Боб|≡ Боб←K_bs →Тренд

Тренд|≡ Боб←K_bs →Тренд

Також є ще псевдо випадкове число:

Боб|≡R_В

Крім цього є кілька пропозицій, що до ключів шифрування:

• Боб покладається на Алісу в виборі стійкого ключа:

Боб|≡Аліса|=>(Аліса←K_ab →Боб)

• Боб довіряє Тренду передати ключ від Аліси:

Боб|≡Тренд|=>(Аліса|≡Аліса←K_ab →Боб)

• Аліса вірить, що сеансовий ключ прийнятий:

Аліса|≡(Аліса←K_ab →Боб)

Аналізу протоколу[7]:

• Тренд отримує перше повідомлення від Боба з згенерованим псевдовипадковим числом R_В. Після чого відправляє це число Алісі.

Тренд|≡Боб|≡(Боб← R_В →Аліса).

• Аліса отримує повідомлення від Тренда з даним числом генерує сеансовий ключ і відправляє повідомлення Тренду додавши це число у кінець свого повідомлення.

• Тренд отримує повідомлення від Аліси, яке потім розшифровує за допомогою сумісного з нею ключа. Тренд бачачи повідомлення зашифроване ключем K_as робить висновок, що повідомлення відправлене Алісою(правило про значення повідомлення). Наявність випадкового числа, яке було відправлене Бобом, свідчить про те, що Аліса вірить що одержувач Боб(правило перевірки унікальності числових вставок). З цього слідує, Тренд|≡Аліса|≡(Аліса←K_ab →Боб).

• Боб отримує повідомлення від Тренда, яке він розшифровує за допомогою сумісного з ним ключа. Випадкове число згенероване Бобом доказує, що повідомлення адресоване йому. Побачивши повідомлення Боб робить висновок, що Тренд довіряє свому відправнику. Боб вірить в те, що Тренд довіряє другій частині повідомлення, тому Боб довіряє Алісі генерування ключа.

З цього можна зробити наступні висновки:

Боб|≡(Аліса←K_ab →Боб)

Боб|≡Аліса|≡(Аліса←K_ab →Боб)

В випадку початкової догадки про те, що Аліса|≡(Аліса←K_ab →Боб), отримуєм, що проаналізований протокол коректний. Єдине чого не можна стверджувати:

Аліса |≡Боб|≡(Аліса←K_ab →Боб)

Тобто Аліса не добилася підтвердження того, що Боб отримав потрібний ключ.