Образцы тамарина
 | |
 | |
| Оригинальный автор(ы) | Дэвид Басин, Кас Кремерс , Янник Драйер, Саймон Мейер, Ральф Сасс, Бенедикт Шмидт |
|---|---|
| Разработчик(и) | Кас Кремерс , Янник Драйер, Ральф Сасс |
| Первоначальный выпуск | 24 апреля 2012 г. |
| Стабильная версия | 1.4.1 / 18 января 2019 г. |
| Репозиторий | github |
| Написано в | Хаскелл |
| Операционная система | Линукс , МакОС |
| Доступно в | Английский |
| Тип | Автоматизированное рассуждение |
| Лицензия | Лицензия GNU GPL v3 |
| Веб-сайт | образцы тамарина |
Tamarin Prover — компьютерная программа для формальной проверки криптографических протоколов . [1] Он использовался для проверки безопасности транспортного уровня 1.3, [2] ИСО/МЭК 9798, [3] Безопасная аутентификация DNP3 v5, [4] ВайрГард , [5] [6] [7] [8] и протокол обмена сообщениями PQ3 Apple iMessage . [9]
Tamarin — инструмент с открытым исходным кодом, написанный на Haskell . [10] созданный как преемник более старого инструмента проверки под названием Scyther. [11] Тамарин имеет функции автоматического проверки, но также может управляться самостоятельно. [11] В Тамарине леммы , представляющие свойства безопасности. определены [12] После внесения изменений в протокол Тамарин может проверить, сохраняются ли свойства безопасности. [12] Результатом выполнения Tamarin будет либо доказательство того, что свойство безопасности сохраняется в протоколе, либо пример протокола, запускаемого без свойства безопасности, либо Tamarin потенциально может не остановиться . [12] [10]
См. также
[ редактировать ]Ссылки
[ редактировать ]- ^ Бланше, Б. (2014). Автоматическая проверка протоколов безопасности в символьной модели: Verifier ProVerif. В: Альдини А., Лопес Дж., Мартинелли Ф. (ред.) Основы анализа и проектирования безопасности VII . FOSAD FOSAD 2013 2012. Конспекты лекций по информатике, том 8604. Springer, Cham.
- ^ Кремерс, Кас; Хорват, Марко; Скотт, Сэм; ван дер Мерве, Тайла (2016). «Автоматический анализ и проверка TLS 1.3: 0-RTT, возобновление и отложенная аутентификация» . Симпозиум IEEE по безопасности и конфиденциальности, 2016 г., Сан-Хосе, Калифорния, США, 22–26 мая 2016 г. IEEE S&P 2016. стр. 470–485. дои : 10.1109/СП.2016.35 . ISBN 978-1-5090-0824-7 .
- ^ Басин, Дэвид; Кремерс, Кас; Мейер, Саймон (2013). «Доказуемое восстановление стандарта ISO/IEC 9798 для аутентификации объектов» (PDF) . Журнал компьютерной безопасности . 21 (6): 817–846. дои : 10.3233/JCS-130472 . hdl : 20.500.11850/69793 .
- ^ Кремерс, Кас ; Денель-Вильд, Мартин; Милнер, Кевин (2017). «Безопасная аутентификация в сети: формальный анализ DNP3: SAv5» (PDF) . Компьютерная безопасность — ESORICS 2017 — 22-й Европейский симпозиум по исследованиям в области компьютерной безопасности, Осло, Норвегия, 11-15 сентября 2017 г., Материалы, Часть I. ЭЗОРИКС 2017 . Осло, Норвегия: Springer. стр. 389–407. дои : 10.1007/978-3-319-66402-6_23 . ISBN 978-3-319-66401-9 .
- ^ Доненфельд, Джейсон А.; Милн, Кевин (2018), Формальная проверка протокола WireGuard (PDF) , заархивировано (PDF) из оригинала 28 мая 2023 г. , получено 23 ноября 2023 г .; Доненфельд, Джейсон А., Формальная проверка , заархивировано из оригинала 13 ноября 2023 г. , получено 23 ноября 2023 г.
- ^ Шмидт, Бенедикт; Мейер, Саймон; Кремерс, Кас ; Басин, Дэвид (2012). «Автоматический анализ протоколов Диффи-Хеллмана и расширенных свойств безопасности» (PDF) . 25-й симпозиум IEEE по основам компьютерной безопасности, CSF 2012, Кембридж, Массачусетс, США, 25–27 июня 2012 г. CSF 2012. Кембридж, Массачусетс: Компьютерное общество IEEE. стр. 78–94.
- ^ Шмидт, Бенедикт (2012). Формальный анализ протоколов обмена ключами и физических протоколов (кандидатская диссертация). ETH Цюрих. doi : 10.3929/ethz-a-009898924 . hdl : 20.500.11850/72713 .
- ^ Мейер, Саймон (2012). Развитие автоматизированной проверки протоколов безопасности (кандидатская диссертация). ETH Цюрих. дои : 10.3929/ethz-a-009790675 . hdl : 20.500.11850/66840 .
- ^ Басин, Дэвид; Линкер, Феликс; Сасс, Ральф, Формальный анализ протокола обмена сообщениями iMessage PQ3 (PDF) , заархивировано (PDF) из оригинала 28 февраля 2024 г. , получено 6 марта 2024 г.
- ^ Перейти обратно: а б П. Ремлейн, М. Рогацкий и У. Стаховяк, «Программное обеспечение Tamarin – инструмент для обеспечения безопасности проверки протоколов», Балтийский симпозиум URSI 2020 (URSI), Варшава, Польша, 2020, стр. 118-123, doi: 10.23919/URSI48707. 2020.9254078.
- ^ Перейти обратно: а б Колин Бойд, Аниш Матуриа, Дуглас Стебила. «Протоколы аутентификации и установления ключей», второе издание Springer, 2019 г., стр. 48.
- ^ Перейти обратно: а б с Сели, София, Джонатан Хойланд, Дуглас Стебила и Том Виггерс. «История двух моделей: формальная проверка KEMTLS через Tamarin». На Европейском симпозиуме по исследованиям в области компьютерной безопасности, стр. 63-83. Чам: Springer Nature Switzerland, 2022.
Внешние ссылки
[ редактировать ]- Официальный сайт Тамарина Прувера
- Дэвид Вонг создал вводный видеоролик о прувере Tamarin .