?

Log in

No account? Create an account
Формализация криптографических протоколов. - Программирование с зависимыми типами [entries|archive|friends|userinfo]
Программирование с зависимыми типами

[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Формализация криптографических протоколов. [May. 23rd, 2018|01:51 pm]
Программирование с зависимыми типами

ru_deptypes

[potan]
[Tags|]

Кто-нибудь занимается описанием криптографических протоколов с помощью зависимых типов? Это было бы полезно, например, для верификации смартконтарктов.
Там возникают сложности, как описать знание/незнание ключа. Похоже, полноценного описания требуется использовать модальную логику - такие логики могут отображаться в системы типов?
Пока получается что-то вроде:

Хеш-функция

hash: Data -> CheckSum
hashProp1: (x:Data) -> (y:Data) -> (hash x = hash y) -> (x = y)
hashProp2: (rev: CheckSum -> Data) -> (p: (d: Data -> rev (hash d) = d)) -> Void

То есть значение хеш-функции однозначно идентифицирует аргемент, но обратной к ней не существует.

Симметричное шифрование

encode: Key -> Data -> Encrypted
decode: Key -> Encrypted -> Data
cryptProp1: (k: Key) -> (d: Encrypted) -> (encode k (decode k d)) = d
cryptProp2: (k: Key) -> (d: Data) -> (decode k (encode k d)) = d
cryptProt3: ((d:Data, e:Encrypt) -> (k: Key ** (encode k d = e))) -> Void
cryptProp4: (((d1:Data, e1:Encrypt) -> (d2:Data, e2:Encrypt) -> Either (k: Key -> encode k d1 = e1 -> encode k d2 = e2) (k: Key -> encode k d1 = e1 -> encode k d2 = e2 -> Void)

С электронной подписью пока не разобрался.
LinkReply

Comments:
[User Picture]From: thesz
2018-05-23 12:11 pm (UTC)
Если линейная логика может служить примером модальной (а она может), то она моделируется с помощью окружения (environment).

Вывод с использованием факта, соответственно, это проверка наличия факта в окружении (был выведен и не использован), обычный вывод и удаление факта из окружения. Функции a -> b становятся поднятыми в (Env, a) -> (Env, b).

Для фактов определённого типа можно заводить разные окружения.

Протоколы вида "достаточно знания n фактов из m" это телескопы. И т.п.

Никаких ракетных хирургий или нейронных наук не требуется.
(Reply) (Thread)