ВИЯВЛЕННЯ ВРАЗЛИВОСТЕЙ ІНФОРМАЦІЙНИХ СИСТЕМ НА ОСНОВІ ПРОЦЕДУР ІДЕНТИФІКАЦІЇ ТА АВТЕНТИФІКАЦІЇ

Анотація

У статті досліджено проблему логічних помилок у процесах автентифікації, що можуть призвести до критичних вразливостей у системах контролю доступу. Запропоновано формальну модель, яка демонструє типову помилку логіки перевірки облікових даних, коли автентифікація дозволяється за умови виконання хоча б однієї з умов: наявності правильного пароля або відсутності ідентифікатора користувача. Для верифікації моделі використано інструмент ProVerif, що дозволяє автоматично перевірити властивості безпеки протоколу. Результати моделювання підтверджують можливість обходу автентифікації, що свідчить про необхідність застосування формальних методів аналізу на етапі проєктування систем безпеки.