Формализация криптографических протоколов.
Кто-нибудь занимается описанием криптографических протоколов с помощью зависимых типов? Это было бы полезно, например, для верификации смартконтарктов.
Там возникают сложности, как описать знание/незнание ключа. Похоже, полноценного описания требуется использовать модальную логику - такие логики могут отображаться в системы типов?
Пока получается что-то вроде:
То есть значение хеш-функции однозначно идентифицирует аргемент, но обратной к ней не существует.
С электронной подписью пока не разобрался.
Там возникают сложности, как описать знание/незнание ключа. Похоже, полноценного описания требуется использовать модальную логику - такие логики могут отображаться в системы типов?
Пока получается что-то вроде:
Хеш-функция
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)
С электронной подписью пока не разобрался.