ProVerif
| Разработчик(и) | Бруно Бланше |
|---|---|
| Первоначальный выпуск | 1 июня 2002 г. |
| Стабильная версия | 2.04 / 1 декабря 2021 г. [1] |
| Написано в | OCaml |
| Доступно в | Английский |
| Лицензия | В основном GNU GPL ; Бинарные файлы Windows, лицензии BSD |
| Веб-сайт | просекко |
ProVerif — это программный инструмент для автоматического анализа свойств безопасности криптографических протоколов . Инструмент был разработан Бруно Бланше и другими.
Обеспечивается поддержка криптографических примитивов , включая: симметричную и асимметричную криптографию; цифровые подписи ; хэш-функции; бит-обязательство ; и подписи, подтверждающие знания. Инструмент способен оценивать свойства достижимости, утверждения соответствия и эквивалентность наблюдений . Эти возможности рассуждения особенно полезны для области компьютерной безопасности , поскольку они позволяют анализировать свойства секретности и аутентификации. Также можно учитывать новые свойства, такие как конфиденциальность, отслеживаемость и проверяемость. Анализ протокола рассматривается применительно к неограниченному числу сеансов и неограниченному пространству сообщений. Инструмент способен к реконструкции атаки: если свойство не может быть подтверждено, создается трассировка выполнения, которая фальсифицирует желаемое свойство.
Применимость ProVerif
[ редактировать ]ProVerif использовался в следующих тематических исследованиях, которые включают анализ безопасности реальных сетевых протоколов:
- Абади и Бланше [2] использовали утверждения о переписке для проверки сертифицированного протокола электронной почты. [3]
- Абади, Бланше и Фурне [4] проанализировать Just Fast Keying [5] Протокол, который был одним из кандидатов на замену Internet Key Exchange (IKE) в качестве протокола обмена ключами в IPsec , путем объединения ручных доказательств с доказательствами соответствия и эквивалентности ProVerif.
- Бланше и Чаудхури [6] изучил целостность файловой системы Plutus [7] на ненадежном хранилище с использованием утверждений о соответствии, что приводит к обнаружению и последующему устранению недостатков исходной системы.
- Бхаргаван и др. [8] [9] [10] использовать ProVerif для анализа реализаций криптографических протоколов, написанных на F# ; в частности, Transport Layer Security (TLS). таким образом был изучен протокол
- Чен и Райан [11] оценили протоколы аутентификации, обнаруженные в Trusted Platform Module (TPM), широко распространенном аппаратном чипе, и обнаружили уязвимости .
- Делон, Кремер и Райан [12] [13] и Бэкес, Хритку и Маффеи [14] формализовать и проанализировать свойства конфиденциальности для электронного голосования, используя наблюдательную эквивалентность.
- Делон, Райан и Смит [15] и Бэкес, Маффей и Унру [16] проанализировать свойства анонимности доверенной вычислительной схемы прямой анонимной аттестации (DAA) с использованием эквивалентности наблюдений.
- Кустерс и Трудерунг [17] [18] изучить протоколы с возведением в степень Диффи-Хеллмана и XOR .
- Смит, Райан, Кремер и Курджие [19] формализовать и проанализировать свойства проверяемости электронного голосования с использованием достижимости.
- Google [20] проверил свой протокол транспортного уровня ALTS .
- Сардар и др. [21] [22] проверил протоколы удаленной аттестации в Intel SGX .
Дополнительные примеры можно найти в Интернете: [1] .
Альтернативы
[ редактировать ]Альтернативные инструменты анализа включают: AVISPA (для утверждений достижимости и соответствия), KISS (для статической эквивалентности), YAPA (для статической эквивалентности). CryptoVerif для проверки безопасности против противников с полиномиальным временем в вычислительной модели. Tamarin Prover — это современная альтернатива ProVerif, обеспечивающая отличную поддержку уравнений Диффи-Хеллмана и проверку свойств эквивалентности наблюдений.
Ссылки
[ редактировать ]- ^ Новый выпуск: ProVerif 2.04 — Сообщество — OCaml
- ^ Абади, Мартин; Бланше, Бруно (2005). «Компьютерная проверка протокола сертифицированной электронной почты» . Наука компьютерного программирования . 58 (1–2): 3–27. дои : 10.1016/j.scico.2005.02.002 .
- ^ Абади, Мартин; Глю, Нил (2002). «Сертифицированная электронная почта от доверенной третьей стороны в сети». Материалы 11-й международной конференции по Всемирной паутине . WWW '02. Нью-Йорк, штат Нью-Йорк, США: ACM. стр. 387–395. дои : 10.1145/511446.511497 . ISBN 978-1581134490 . S2CID 9035150 .
- ^ Абади, Мартин; Бланше, Бруно; Фурне, Седрик (июль 2007 г.). «Просто быстрое ввод в исчислении числа Пи». Транзакции ACM по информационной и системной безопасности . 10 (3): 9–с. CiteSeerX 10.1.1.3.3762 . дои : 10.1145/1266977.1266978 . ISSN 1094-9224 . S2CID 2371806 .
- ^ Айелло, Уильям; Белловин, Стивен М.; Блейз, Мэтт; Канетти, Ран; Иоаннидис, Джон; Керомитис, Ангелос Д.; Рейнгольд, Омер (май 2004 г.). «Просто быстрый ввод: ключевое соглашение во враждебном Интернете». Транзакции ACM по информационной и системной безопасности . 7 (2): 242–273. дои : 10.1145/996943.996946 . ISSN 1094-9224 . S2CID 14442788 .
- ^ Бланше, Б.; Чаудхури, А. (май 2008 г.). «Автоматизированный формальный анализ протокола безопасного обмена файлами в ненадежном хранилище». Симпозиум IEEE по безопасности и конфиденциальности 2008 г. (Sp 2008) . стр. 417–431. CiteSeerX 10.1.1.362.4343 . дои : 10.1109/СП.2008.12 . ISBN 978-0-7695-3168-7 . S2CID 6736116 .
- ^ Каллахалла, Махеш; Ридель, Эрик; Сваминатан, Рам; Ван, Цянь; Фу, Кевин (2003). «Plutus: масштабируемый безопасный общий доступ к файлам в ненадежном хранилище» . Материалы 2-й конференции USENIX по файловым технологиям и технологиям хранения данных . БЫСТРО '03: 29–42.
- ^ Бхаргаван, Картикеян; Фурне, Седрик; Гордон, Эндрю Д. (8 сентября 2006 г.). «Проверенные эталонные реализации протоколов WS-Security». Веб-сервисы и формальные методы . Конспекты лекций по информатике. Том. 4184. Шпрингер, Берлин, Гейдельберг. стр. 88–106. CiteSeerX 10.1.1.61.3389 . дои : 10.1007/11841197_6 . ISBN 9783540388623 .
- ^ Бхаргаван, Картикеян; Фурне, Седрик; Гордон, Эндрю Д.; Свами, Нихил (2008). «Проверенные реализации протокола федеративного управления идентификацией информационных карт». Материалы симпозиума ACM 2008 года по информационной, компьютерной и коммуникационной безопасности . АЗИАККС '08. Нью-Йорк, штат Нью-Йорк, США: ACM. стр. 123–135. дои : 10.1145/1368310.1368330 . ISBN 9781595939791 . S2CID 6821014 .
- ^ Бхаргаван, Картикеян; Фурне, Седрик; Гордон, Эндрю Д.; Це, Стивен (декабрь 2008 г.). «Проверенные совместимые реализации протоколов безопасности». Транзакции ACM в языках и системах программирования . 31 (1): 5:1–5:61. CiteSeerX 10.1.1.187.9727 . дои : 10.1145/1452044.1452049 . ISSN 0164-0925 . S2CID 14018835 .
- ^ Чен, Лицюнь; Райан, Марк (5 ноября 2009 г.). «Атака, решение и проверка общих данных авторизации в TPM TCG». Формальные аспекты безопасности и доверия . Конспекты лекций по информатике. Том. 5983. Шпрингер, Берлин, Гейдельберг. стр. 201–216. CiteSeerX 10.1.1.158.2073 . дои : 10.1007/978-3-642-12459-4_15 . ISBN 9783642124587 .
- ^ Делон, Стефани; Кремер, Стив; Райан, Марк (1 января 2009 г.). «Проверка свойств конфиденциальности протоколов электронного голосования». Журнал компьютерной безопасности . 17 (4): 435–487. CiteSeerX 10.1.1.142.1731 . дои : 10.3233/jcs-2009-0340 . ISSN 0926-227X .
- ^ Кремер, Стив; Райан, Марк (4 апреля 2005 г.). «Анализ протокола электронного голосования в прикладном исчислении числа Пи». Языки и системы программирования . Конспекты лекций по информатике. Том. 3444. Шпрингер, Берлин, Гейдельберг. стр. 186–200. дои : 10.1007/978-3-540-31987-0_14 . ISBN 9783540254355 .
- ^ Бэкес, М.; Хритку, К.; Маффей, М. (июнь 2008 г.). «Автоматическая проверка протоколов дистанционного электронного голосования в прикладном пи-исчислении». 2008 г. 21-й симпозиум IEEE по основам компьютерной безопасности . стр. 195–209. CiteSeerX 10.1.1.612.2408 . дои : 10.1109/CSF.2008.26 . ISBN 978-0-7695-3182-3 . S2CID 15189878 .
- ^ Делон, Стефани; Райан, Марк; Смит, Бен (18 июня 2008 г.). «Автоматическая проверка свойств конфиденциальности в прикладном исчислении числа Пи». Доверительное управление II . ИФИП – Международная федерация обработки информации. Том. 263. Спрингер, Бостон, Массачусетс. стр. 263–278. дои : 10.1007/978-0-387-09428-1_17 . ISBN 9780387094274 .
- ^ Бэкес, М.; Маффей, М.; Унру, Д. (май 2008 г.). «Нулевое знание в прикладном пи-исчислении и автоматизированная проверка протокола прямой анонимной аттестации». Симпозиум IEEE по безопасности и конфиденциальности 2008 г. (Sp 2008) . стр. 202–215. CiteSeerX 10.1.1.463.489 . дои : 10.1109/СП.2008.23 . ISBN 978-0-7695-3168-7 . S2CID 651680 .
- ^ Кюстерс, Р.; Трудерунг, Т. (июль 2009 г.). «Использование ProVerif для анализа протоколов с возведением в степень Диффи-Хеллмана». 2009 г. 22-й симпозиум IEEE по основам компьютерной безопасности . стр. 157–171. CiteSeerX 10.1.1.667.7130 . дои : 10.1109/CSF.2009.17 . ISBN 978-0-7695-3712-2 . S2CID 14185888 .
- ^ Кюстерс, Ральф; Трудерунг, Томаш (01 апреля 2011 г.). «Сведение анализа протокола с использованием XOR к случаю без XOR в подходе, основанном на теории рупора». Журнал автоматизированного рассуждения . 46 (3–4): 325–352. arXiv : 0808.0634 . дои : 10.1007/s10817-010-9188-8 . ISSN 0168-7433 . S2CID 7597742 .
- ^ Кремер, Стив; Райан, Марк; Смит, Бен (20 сентября 2010 г.). «Проверяемость выборов в протоколах электронного голосования». Компьютерная безопасность – ESORICS 2010 . Конспекты лекций по информатике. Том. 6345. Шпрингер, Берлин, Гейдельберг. стр. 389–404. CiteSeerX 10.1.1.388.2984 . дои : 10.1007/978-3-642-15497-3_24 . ISBN 9783642154966 .
- ^ «Транспортная безопасность прикладного уровня | Документация» . Гугл облако .
- ^ Сардар, Мухаммад Усама; Куок, До Ле; Фетцер, Кристоф (август 2020 г.). «На пути к формализации удаленной аттестации на основе расширенного идентификатора конфиденциальности (EPID) в Intel SGX» . 2020 23-я конференция Euromicro по проектированию цифровых систем (DSD) . Крань, Словения: IEEE. стр. 604–607. дои : 10.1109/DSD51259.2020.00099 . ISBN 978-1-7281-9535-3 . S2CID 222297511 .
- ^ Сардар, Мухаммад Усама; Факех, Раша; Фетцер, Кристоф (2020). «Формальные основы для примитивов аттестации центров обработки данных Intel SGX» . Ин Линь, Шан-Вэй; Хоу, Чжэ; Махони, Брендан (ред.). Формальные методы и программная инженерия . Конспекты лекций по информатике. Том. 12531. Чам: Springer International Publishing. стр. 268–283. дои : 10.1007/978-3-030-63406-3_16 . ISBN 978-3-030-63406-3 . S2CID 229344923 .