ProVerif - ProVerif

ProVerif
Разработчики)Бруно Бланше
изначальный выпуск1 июня 2002 г. (2002-06-01)
Стабильный выпуск
2.02p1 / 2 сентября 2020 г. (2020-09-02)
Написано вOCaml
Доступно ванглийский
ЛицензияВ основном, GNU GPL; Двоичные файлы Windows, Лицензии BSD
Интернет сайтпросекко.gforge.inria.fr/ личное/ bblanche/ proverif/

ProVerif это программный инструмент для автоматическое рассуждение о свойствах безопасности, найденных в криптографические протоколы. Инструмент был разработан Бруно Бланше.

Обеспечивается поддержка криптографических примитивов, включая: симметричную и асимметричную криптографию; цифровые подписи; хеш-функции; бит-обязательство; и подписные доказательства знаний. Инструмент способен оценивать свойства достижимости, утверждения соответствия и наблюдательная эквивалентность. Эти возможности рассуждений особенно полезны в области компьютерной безопасности, поскольку они позволяют анализировать секретность и свойства аутентификации. Также можно рассмотреть новые свойства, такие как конфиденциальность, отслеживаемость и проверяемость. Анализ протокола рассматривается в отношении неограниченного количества сеансов и неограниченного пространства сообщений. Инструмент может реконструировать атаку: когда свойство не может быть доказано, строится трассировка выполнения, которая искажает желаемое свойство.

Применимость ProVerif

ProVerif использовался в следующих тематических исследованиях, которые включают анализ безопасности реальных сетевых протоколов:

  • Абади и Бланше[1] использовал утверждения переписки для проверки сертифицированного протокола электронной почты.[2]
  • Абади, Бланше и Фурне[3] проанализировать Just Fast Keying[4] протокол, который был одним из кандидатов на замену Обмен ключами в Интернете (IKE) в качестве протокола обмена ключами в IPsec, путем объединения ручных доказательств с доказательствами соответствия и эквивалентности ProVerif.
  • Бланше и Чаудхури[5] изучил целостность файловой системы Plutus[6] на ненадежном хранилище, используя утверждения соответствия, что приводит к обнаружению и последующему исправлению слабых мест в исходной системе.
  • Бхаргаван и другие.[7][8][9] используйте ProVerif для анализа реализаций криптографических протоколов, написанных в F Sharp (язык программирования); в частности Безопасность транспортного уровня (TLS) протокол был изучен таким образом.
  • Чен и Райан[10] оценили протоколы аутентификации, найденные в Модуль доверенной платформы (TPM), широко распространенный аппаратный чип, и обнаруженные уязвимости.
  • Делон, Кремер и Райан[11][12] и Backes, Hritcu & Maffei[13] формализовать и проанализировать свойства конфиденциальности для электронное голосование с использованием наблюдательной эквивалентности.
  • Делон, Райан и Смит[14] и Backes, Maffei & Unruh[15] анализировать свойства анонимности доверенной вычислительной схемы Прямая анонимная аттестация (DAA) с использованием наблюдательной эквивалентности.
  • Kusters & Truderung[16][17] изучать протоколы с Диффи-Хеллман возведение в степень и XOR.
  • Смит, Райан, Кремер и Курджие[18] формализовать и проанализировать проверяемость для электронного голосования, используя доступность.
  • Google[19] проверил свой протокол транспортного уровня ALTS.

Дополнительные примеры можно найти в Интернете: [1].

Альтернативы

К альтернативным инструментам анализа относятся: AVISPA (для утверждений о достижимости и соответствия), KISS (для статической эквивалентности), YAPA (для статической эквивалентности). CryptoVerif для проверки защищенности от полиномиальное время противники в вычислительной модели. В Тамарин Прувер представляет собой современную альтернативу ProVerif с отличной поддержкой рассуждений по уравнениям Диффи-Хеллмана и проверкой свойств эквивалентности наблюдений.

Рекомендации

  1. ^ Абади, Мартин; Бланше, Бруно (2005). «Компьютерная проверка протокола сертифицированной электронной почты». Наука компьютерного программирования. 58 (1–2): 3–27. Дои:10.1016 / j.scico.2005.02.002.
  2. ^ Абади, Мартин; Глю, Нил (2002). Сертифицированная электронная почта с легким он-лайн надежным сторонним поставщиком: разработка и внедрение. Материалы 11-й Международной конференции по всемирной паутине. WWW '02. Нью-Йорк, Нью-Йорк, США: ACM. С. 387–395. Дои:10.1145/511446.511497. ISBN  978-1581134490.
  3. ^ Абади, Мартин; Бланше, Бруно; Фурне, Седрик (июль 2007 г.). «Просто быстрая клавиша в исчислении числа пи». ACM-транзакции по информационной и системной безопасности. 10 (3): 9 – es. CiteSeerX  10.1.1.3.3762. Дои:10.1145/1266977.1266978. ISSN  1094-9224.
  4. ^ Айелло, Уильям; Белловин, Стивен М .; Blaze, Мэтт; Канетти, Ран; Иоаннидис, Джон; Keromytis, Angelos D .; Рейнгольд, Омер (май 2004 г.). «Просто быстрый ключ: ключевое соглашение во враждебном Интернете». ACM-транзакции по информационной и системной безопасности. 7 (2): 242–273. Дои:10.1145/996943.996946. ISSN  1094-9224.
  5. ^ Blanchet, B .; Чаудхури, А. (май 2008 г.). Автоматический формальный анализ протокола безопасного обмена файлами в ненадежном хранилище. Симпозиум IEEE по безопасности и конфиденциальности 2008 г. (Sp 2008). С. 417–431. CiteSeerX  10.1.1.362.4343. Дои:10.1109 / SP.2008.12. ISBN  978-0-7695-3168-7.
  6. ^ Каллахалла, Махеш; Ридель, Эрик; Сваминатан, Рам; Ван, Цянь; Фу, Кевин (2003). «Plutus: масштабируемый безопасный обмен файлами в ненадежном хранилище». Материалы 2-й конференции USENIX по файловым технологиям и технологиям хранения. FAST '03: 29–42.
  7. ^ Бхаргаван, Картикеян; Фурне, Седрик; Гордон, Эндрю Д. (2006-09-08). Проверенные эталонные реализации протоколов WS-Security. Веб-службы и формальные методы. Конспект лекций по информатике. Шпрингер, Берлин, Гейдельберг. С. 88–106. CiteSeerX  10.1.1.61.3389. Дои:10.1007/11841197_6. ISBN  9783540388623.
  8. ^ Бхаргаван, Картикеян; Фурне, Седрик; Гордон, Эндрю Д .; Свами, Нихил (2008). Проверенные реализации протокола управления идентификационной информацией информационных карт. Материалы Симпозиума ACM по информационной, компьютерной и коммуникационной безопасности 2008 г.. ASIACCS '08. Нью-Йорк, Нью-Йорк, США: ACM. С. 123–135. Дои:10.1145/1368310.1368330. ISBN  9781595939791.
  9. ^ Бхаргаван, Картикеян; Фурне, Седрик; Гордон, Эндрю Д .; Це, Стивен (декабрь 2008 г.). «Проверенные совместимые реализации протоколов безопасности». Транзакции ACM по языкам и системам программирования. 31 (1): 5:1–5:61. CiteSeerX  10.1.1.187.9727. Дои:10.1145/1452044.1452049. ISSN  0164-0925.
  10. ^ Чен, Лицюнь; Райан, Марк (2009-11-05). Атака, решение и проверка общих данных авторизации в TCG TPM. Формальные аспекты безопасности и доверия. Конспект лекций по информатике. Шпрингер, Берлин, Гейдельберг. С. 201–216. CiteSeerX  10.1.1.158.2073. Дои:10.1007/978-3-642-12459-4_15. ISBN  9783642124587.
  11. ^ Делон, Стефани; Кремер, Стив; Райан, Марк (01.01.2009). «Проверка свойств типа конфиденциальности протоколов электронного голосования». Журнал компьютерной безопасности. 17 (4): 435–487. CiteSeerX  10.1.1.142.1731. Дои:10.3233 / jcs-2009-0340. ISSN  0926-227X.
  12. ^ Кремер, Стив; Райан, Марк (4 апреля 2005 г.). Анализ электронного протокола голосования в прикладном исчислении числа пи. Языки и системы программирования. Конспект лекций по информатике. Шпрингер, Берлин, Гейдельберг. С. 186–200. Дои:10.1007/978-3-540-31987-0_14. ISBN  9783540254355.
  13. ^ Бэкес, М .; Hritcu, C .; Маффеи, М. (июнь 2008 г.). Автоматическая проверка протоколов дистанционного электронного голосования в прикладном исчислении числа пи. 2008 21-й симпозиум по основам компьютерной безопасности IEEE. С. 195–209. CiteSeerX  10.1.1.612.2408. Дои:10.1109 / CSF.2008.26. ISBN  978-0-7695-3182-3.
  14. ^ Делон, Стефани; Райан, Марк; Смит, Бен (18.06.2008). Автоматическая проверка свойств конфиденциальности в прикладном исчислении Пи. Доверительное управление II. IFIP - Международная федерация обработки информации. Спрингер, Бостон, Массачусетс. С. 263–278. Дои:10.1007/978-0-387-09428-1_17. ISBN  9780387094274.
  15. ^ Бэкес, М .; Maffei, M .; Унру, Д. (май 2008 г.). Отсутствие знаний в прикладном исчислении Пи и автоматическая проверка протокола прямой анонимной аттестации. Симпозиум IEEE по безопасности и конфиденциальности 2008 г. (Sp 2008). С. 202–215. CiteSeerX  10.1.1.463.489. Дои:10.1109 / SP.2008.23. ISBN  978-0-7695-3168-7.
  16. ^ Küsters, R .; Truderung, T. (июль 2009 г.). Использование ProVerif для анализа протоколов с использованием возведения в степень Диффи-Хеллмана. 2009 22-й симпозиум по основам компьютерной безопасности IEEE. С. 157–171. CiteSeerX  10.1.1.667.7130. Дои:10.1109 / CSF.2009.17. ISBN  978-0-7695-3712-2.
  17. ^ Кюстерс, Ральф; Truderung, Томаш (01.04.2011). «Сведение анализа протокола с помощью XOR к случаю без XOR в подходе, основанном на теории Горна». Журнал автоматизированных рассуждений. 46 (3–4): 325–352. arXiv:0808.0634. Дои:10.1007 / s10817-010-9188-8. ISSN  0168-7433.
  18. ^ Кремер, Стив; Райан, Марк; Смит, Бен (20 сентября 2010 г.). Возможность проверки выборов в электронных протоколах голосования. Компьютерная безопасность - ESORICS 2010. Конспект лекций по информатике. Шпрингер, Берлин, Гейдельберг. С. 389–404. CiteSeerX  10.1.1.388.2984. Дои:10.1007/978-3-642-15497-3_24. ISBN  9783642154966.
  19. ^ «Безопасность транспорта на уровне приложений | Документация». Google Cloud.

внешняя ссылка