Розглянуто проблематику застосування засобів автоматичного доведення теорем для дослідження моделей контролю доступу на базі ролей. Запропоновано шляхи представлення моделей
стандарту ANSI-INCITS 359-2004 Role Based Access Control як теорій першого порядку, дослідження
їх властивостей та генерації авторизаційних рішень за допомогою ПЗ EProver.