stringtranslate.com

Тамарин Провер

Tamarin Prover — это компьютерная программа для формальной проверки криптографических протоколов . [1] Она использовалась для проверки Transport Layer Security 1.3, [2] ISO/IEC 9798, [3] DNP3 Secure Authentication v5, [4] WireGuard , [5] [6] [7] [8] и протокола обмена сообщениями PQ3 Apple iMessage . [9]

Tamarin — это инструмент с открытым исходным кодом, написанный на языке Haskell , [10], созданный как преемник более старого инструмента проверки под названием Scyther. [11] Tamarin имеет автоматические функции доказательства, но также может быть самоуправляемым. [11] В леммах Tamarin определены представляющие свойства безопасности. [12] После внесения изменений в протокол Tamarin может проверить, поддерживаются ли свойства безопасности. [12] Результатом выполнения Tamarin будет либо доказательство того, что свойство безопасности сохраняется в протоколе, пример запуска протокола, в котором свойство безопасности не сохраняется, либо Tamarin может потенциально не остановиться . [12] [10]

Смотрите также

Ссылки

  1. ^ Бланше, Б. (2014). Автоматическая проверка протоколов безопасности в символической модели: верификатор ProVerif. В: Aldini, A., Lopez, J., Martinelli, F. (ред.) Основы анализа и проектирования безопасности VII. FOSAD FOSAD 2013 2012. Конспект лекций по информатике, том 8604. Springer, Cham.
  2. ^ Cremers, Cas; Horvat, Marko; Scott, Sam; van der Merwe, Thyla (2016). «Автоматизированный анализ и проверка TLS 1.3: 0-RTT, возобновление и отложенная аутентификация». Симпозиум IEEE по безопасности и конфиденциальности, 2016, Сан-Хосе, Калифорния, США, 22–26 мая 2016 г. IEEE S&P 2016. стр. 470–485. doi :10.1109/SP.2016.35. ISBN 978-1-5090-0824-7.
  3. ^ Basin, David; Cremers, Cas; Meier, Simon (2013). «Доказуемое исправление стандарта ISO/IEC 9798 для аутентификации сущностей» (PDF) . Journal of Computer Security . 21 (6): 817–846. doi :10.3233/JCS-130472. hdl :20.500.11850/69793.
  4. ^ Кремерс, Кас ; Денел-Уайлд, Мартин; Милнер, Кевин (2017). «Безопасная аутентификация в сетке: формальный анализ DNP3: SAv5» (PDF) . Компьютерная безопасность — ESORICS 2017 — 22-й Европейский симпозиум по исследованиям в области компьютерной безопасности, Осло, Норвегия, 11–15 сентября 2017 г., Труды, часть I. ESORICS 2017. Осло, Норвегия: Springer. стр. 389–407. doi :10.1007/978-3-319-66402-6_23. ISBN 978-3-319-66401-9.
  5. ^ Доненфельд, Джейсон А.; Милн, Кевин (2018), Формальная проверка протокола WireGuard (PDF) , заархивировано (PDF) из оригинала 28.05.2023 , извлечено 23.11.2023; Доненфельд, Джейсон А., Формальная проверка, заархивировано из оригинала 2023-11-13 , извлечено 2023-11-23
  6. ^ Шмидт, Бенедикт; Мейер, Саймон; Кремерс, Кас ; Басин, Дэвид (2012). «Автоматизированный анализ протоколов Диффи-Хеллмана и расширенных свойств безопасности» (PDF) . 25-й симпозиум IEEE Computer Security Foundations, CSF 2012, Кембридж, Массачусетс, США, 25–27 июня 2012 г. CSF 2012. Кембридж, Массачусетс: IEEE Computer Society. стр. 78–94.
  7. ^ Шмидт, Бенедикт (2012). Формальный анализ протоколов обмена ключами и физических протоколов (диссертация на соискание степени доктора философии). ETH Zurich. doi :10.3929/ethz-a-009898924. hdl :20.500.11850/72713.
  8. ^ Мейер, Саймон (2012). Развитие автоматизированной проверки протоколов безопасности (диссертация). ETH Zurich. doi :10.3929/ethz-a-009790675. hdl :20.500.11850/66840.
  9. ^ Basin, David; Linker, Felix; Sasse, Ralf, Формальный анализ протокола обмена сообщениями iMessage PQ3 (PDF) , заархивировано (PDF) из оригинала 2024-02-28 , извлечено 2024-03-06
  10. ^ аб П. Ремлейн, М. Рогацкий и У. Стаховяк, «Программное обеспечение Tamarin – инструмент для обеспечения безопасности проверки протоколов», Балтийский симпозиум URSI 2020 (URSI), Варшава, Польша, 2020, стр. 118-123, doi: 10.23919/ УРСИ48707.2020.9254078.
  11. ^ ab Колин Бойд, Аниш Матурия, Дуглас Стебила. «Протоколы аутентификации и установления ключей», Второе издание Springer, 2019. стр. 48
  12. ^ abc Celi, Sofía, Jonathan Hoyland, Douglas Stebila и Thom Wiggers. «Рассказ о двух моделях: формальная проверка KEMTLS через Tamarin». В European Symposium on Research in Computer Security, стр. 63-83. Cham: Springer Nature Switzerland, 2022.

Внешние ссылки