Tracking Variable Transformations and Validations in Symmetric Encryption/Decryption Flow

[MarianBaba]

Hello everyone,

I am working on a DSL for defining communication protocols. My DSL has some built-in functions, which users can call in their programs. Some of these functions include encryption and decryption. Right now, I'm focused on writing validation functions that can verify if a symmetric key is used correctly in the symmetric encryption and decryption process.

Here is an example of this process:

principal Alice, Bob // Actors of the protocol

Alice knows {
    const priv_key_a, // Alice's private key
    pub_key_a = PUB_GEN(priv_key_a) // Alice's public key, generated using her private key
}

Bob knows {
	// Same process for Bob
    const priv_key_b,
    pub_key_b = PUB_GEN(priv_key_b)
}

// Alice and Bob exchange their public keys
Alice -> Bob : pub_key_a
Bob -> Alice : pub_key_b

Alice knows {
	// Alice generates a symmetric key
    fresh symmetric_key_a
}

Alice knows {
	// She encrypts it with Bob's public key
    encrypted_key_a = PKE_ENC(symmetric_key_a) with pub_key_b
}

	// And sends the encrypted key to Bob
Alice -> Bob : encrypted_key_a

Bob knows {
	// Bob can decrypt the key using his private key
    decrypted_key_a = PKE_DEC(encrypted_key_a) with priv_key_b
    // Here symmetric_key_a == decrypted_key_a -> THIS IS WHAT I WANT MY VALIDATION FUNCTION TO UNDERSTAND
}

Alice knows {
	// Alice encrypts a message with her symmetric key and sends it to Bob
    const message,
    encrypted_message = ENC(message) with symmetric_key_a 

}

Alice -> Bob : encrypted_message

Bob knows {
	// Bob can decrypt Alice's message because he knows her symmetric key
    decrypted_message = DEC(encrypted_message) with decrypted_key_a
}

Now, here is the problem: I want my validation function to understand that decrypted_key_a refers to the same value as symmetric_key_a and be able to give an error if an incorrect symmetric key is used when calling DEC(). In other words, I want my validation function to keep track of the function invocation flow/communication flow that a variable goes through, and provide relevant errors.

Do you have any idea how this can be done? Alternatively, can anyone point me to a compiler/validator that does something similar so I can understand the logic that goes behind this type of validation?

[msujew]

Hey @MarianBaba,

I haven't written this kind of validation yet, but it should be in theory closely related to the problem of statically computing type information in a (dynamic) programming language. Let's take a look at this from a type system perspective

function PKE_ENC<T, K>(toEncrypt: T, publicKey: Public<K>): EncryptedPK<T, K>
function PKE_DEC<T, K>(toDecrypt: EncryptedPK<T, K>, privateKey: Private<K>): T

encrypted_key_a = PKE_ENC(symmetric_key_a) with pub_key_b // `encrypted_key_a` Typed as `EncryptedPK<symmetric_key_a, pub_key_b>`
decrypted_key_a = PKE_DEC(encrypted_key_a) with priv_key_b // `decrypted_key_a` Typed as `symmetric_key_a` (which is the goal)

Note that there's a (but omitted) relationship between types Public<K> and Private<K>. Anyway, writing type systems that support arguments isn't trivial, but has been done before (see most popular programming languages). This is obviously a very specific case, but the general idea should be the same.

Does that help you in any way?