mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-16 11:22:33 +03:00
81 lines
2.0 KiB
Plaintext
81 lines
2.0 KiB
Plaintext
// WORK IN PROGRESS
|
|
|
|
/*
|
|
Implementation of the algorithms from the paper
|
|
"Automated Analysis and Synthesis of Authenticated Encryption Schemes"
|
|
by Viet Tung Hoang, Jonathan Katz, and Alex J. Malozemoff
|
|
*/
|
|
|
|
parameter
|
|
type A : * // State type
|
|
type K : * // Key type
|
|
type n : # // Block size
|
|
type p : # // Number of blocks to process at once
|
|
type tagAmount : #
|
|
|
|
type constraint (fin p, fin n, n >= tagAmount)
|
|
|
|
// Process a single block using this key and tweak
|
|
tweak_cipher : K -> Tweak -> [n] -> [n]
|
|
|
|
// Cost for using the tweak
|
|
Cost : Integer
|
|
|
|
Enc : K -> Tweak -> Node -> Node
|
|
Dec : K -> Tweak -> Node -> Node
|
|
Tag : K -> Tweak -> State -> [n]
|
|
|
|
// The unit at which `Enc` operates
|
|
type Node = { message : WorkBlock, state : State }
|
|
|
|
// Some encryption schemes process multiple blocks at once
|
|
type WorkBlock = [p*n]
|
|
|
|
type State = [p*n] // The state for `p` blocks
|
|
|
|
type Tweak = { nonce : Nonce, state : A, z : Integer }
|
|
type Nonce = [n]
|
|
|
|
/*
|
|
property
|
|
|
|
// The tweak in the `i`th query to the tweak_cipher
|
|
tweak_prop i { nonce = n, state = a, z = v } =
|
|
{ nonce = n, state = a, z = v + i - 1 }
|
|
|
|
|
|
// Property of decrypt
|
|
Dec_prop : Tweak -> Node -> Bit
|
|
Dec_prop t { message = m, state = x } =
|
|
Dec t { message = c, state = x } == { message = m, state = y }
|
|
where { message = c, state = y } = Enc t x m
|
|
*/
|
|
|
|
type Integer = [64]
|
|
|
|
encrypt :
|
|
{m} fin m => K -> Nonce -> A -> [m * (p * n)] -> [m * (p * n) + tagAmount]
|
|
encrypt key nonce state inputMsg = encMsg # tag
|
|
|
|
where
|
|
encMsg = join rest.0.message
|
|
|
|
tag = take (Tag key (tweak (1 - final.1)) final.0.state)
|
|
|
|
final = steps ! 0
|
|
|
|
steps = [ ({ message = undefined, state = zero }, 1) ] # rest
|
|
rest = [ (Enc key (tweak v) { message = m, state = prev.state }, v + Cost)
|
|
| (prev,v) <- steps
|
|
| m <- chunks
|
|
]
|
|
|
|
// XXX: isn't v i just 1 + i * Cost
|
|
|
|
chunks : [m] [p * n]
|
|
chunks = split inputMsg
|
|
|
|
tweak : Integer -> Tweak
|
|
tweak v = { nonce = nonce, state = state, z = v }
|
|
|