🔒 Encrypted 🔒

🔒 Encrypted 🔒 is an esolang which can reliably send data over an unreliable network.
== Overview ==
There are three servers: Input server, Main server and Output server.
Input server can read data from stdin. Data is array of bits. Input server can only communicate (send and receive messages) with the Main server.
Main server should be the one that performs the computation. It receives the input bits from the Input server, processes them, computes the output and then sends the output to the Output server. Main server can communicate both with the Input and with the Output server. Main server cannot access stdin or stdout.
Output server can communicate only with the main server. Output server receives data from the Main server and then outputs the data (array of bits) to the stdout. Only Output server can access stdout.
This language is a pure functional language. Function cannot have side effects. Not even reading a stdin or writing to stdout has side effects.
== Builtins ==
There are built-in data types and functions. User can also define new functions, but not new data types. Functions cannot be shared accross servers (one server cannot call a function from another server).
=== Data types ===
* Pair - Pair of two elements
* Bit0 - Bit 0
* Bit1 - Bit 1
* Nonce - Unique nonce value
* Encrypted - Encrypted data
* Hash - Hash value
* Key - Symmetric or asymmetric key
* Integer - Nonnegative integer
* Input - Input stream
* Output - Output stream
* Server - Server instance
* Generator - Random data generator (used for generating nonce values)
* Invalid - Invalid data
* * - Can be any of the above
=== Functions ===
Explained in the form: func(Param1Type, Param2Type, ...) -> ReturnValueType
* pair(*, *) -> Pair(*, *) - Creates a new pair
* fst(Pair) -> * - Returns the first element of a pair
* snd(Pair) -> * - Returns the second element of a pair
* bit0() -> Bit0 - Returns bit 0 (all bits 0 are identical)
* bit1() -> Bit1 - Returns bit 1 (all bits 1 are identical)
* nonce(Generator) -> Pair(Generator, Nonce) - Creates a pair of an updated generator and a nonce value
* encrypt(*, Key) -> Encrypted - Encrypts data using the given key
* decrypt(Encrypted, Key) -> * - Decrypts data using the given key
* hash(*) -> Hash - Computes hash of the given argument
* createKey(*) -> Key - Creates a symmetric key based on the given argument
* createKeyPair(*, *) -> Pair(Key, Key) - Creates a pair of asymmetric keys based on the given parameters
* zero() -> Integer - Returns integer 0
* inc(Integer) -> Integer - Increments the given integer
* dec(Integer) -> Integer - Decrements the given integer
* in(Input) -> Pair(Input, Bit0|Bit1) - Reads a bit and returns a pair of updated input stream and the read bit
* out(Output, Bit0|Bit1) -> Output - Outputs a bit and returns the updated output
* send(Server, *) -> Server - Synchronously sends data to the given server and returns the updated server
* receive(Server) -> Pair(Server, *) - Synchronously receives a data from the given server
* generator() -> Generator - Creates a new generator. Note: all generators are identical, until updated. However, each server has unique generator
* input() -> Input - Returns the untouched input stream (accessible only from the Input server)
* output() -> Output - Returns the untouched output stream (accessible only from the Output server)
* inputServer() -> Server - Returns the untouched Input server (inaccessible from the Output server)
* mainServer() -> Server - Returns the untouched Main server
* outputServer() -> Server - Returns the untouched Output server (inaccessible from the Input server)
* cmp(*, *) -> Bit0|Bit1 - Compares two values and returns Bit1 iff the values are equal
If number of arguments does not match, it is a syntax error. If types of arguments do not match, or any error occurs (for example, decrypting something with a wrong key, or decrementing the integer zero) it results in an Invalid value. All Invalid values are identical.
As said, this programming language is a pure functional language. No function can have side effects. For example, if we output something to the output stream, we receive the updated output stream. However, if we decide to undo that, we can simply dismiss the updated output stream and use the original output stream, which does not have that data.
Note: all crypto functions are perfect. It means that there are no collisions. In other words, if we have some values A and B, then cmp(A, B) is equivalent to cmp(hash(A), hash(B)).
== Network ==
The network which is used for the server communication is unreliable. It means that any message can be intercepted, modified by an attacker, lost, repeated, etc. However, it is guaranteed that every message will receive the destination unchanged after a finite number of attempts. Servers must implement some message integrity check mechanism for detecting whether the message has been modified.
The first message that is sent/received between any two servers cannot be modified by an attacker (the first for one direction and also the first for the other direction). Attacker can still see the message. If attacker can reconstruct the output based on the messages they observe, then the program is considered insecure.
== Syntax ==
Source code consists of three different sections - one for each of the three servers. Each section contains one or more functions and must contain main function.
=== Signature of the main function ===
The singature of the main function differes between servers:
* Input server: main() -> Server
* Main server: main() -> Pair(Server, Server)
* Output server: main() -> Pair(Server, Output)
== Examples ==
=== Flip the first input bit ===
We explain syntax on the following example that aims to flip the first input bit and output that:
 // Input server
 Input{
 main(): send(mainServer(), readBit())
 readBit(): snd(in(input()))
 }
 
 // Main Server
 Main{
 main(): Pair(
 fst(receive(inputServer())),
 send(outputServer(), flip(snd(receive(inputServer()))))
 )
 // Function overloading
 flip(Bit0 bit): bit1()
 flip(Bit1 bit): bit0()
 }
 
 // Output server
 Output{
 main(): Pair(
 fst(receive(mainServer())),
 out(output(), snd(receive(mainServer())))
 )
 }
Explanation: in this example we read a single bit from the stdin (that is done in the Input server), then we send to the Main server, the Main server then flips the bit, then from the Main server we send to the Output server and finally we output to stdout. Some parts may seem weird. For example, one may think that in the Main server we receive two messages from the Input server, because receive(inputServer()) appears two times. However, remember that functions do not have side effects. We actually receive it once, but each time from the untouched Input server, so it is the same data (only one message is received). Similarly, in the Output server we only receive one message from the Main server. Since there is only one message between servers, it cannot be modified by an attacker, so it is safe. However, given that there is an algorithm for an attacker to reconstruct the output for any input, this program is insecure and bad.
== Secure programs ==
We explain how to write secure programs, such that attacker cannot influence our computation, nor can they recounstruct our output.
First, in the Input server, we generate asymmetric key pair using two different nonce values. Then we send one of the keys to the Main server. This is the first message and it cannot be modified by an attacker. Then the Main server also generates a key pair using its own nonce generator and sends one of the keys to the Input server. This message also cannot be modified. From that point on, Input server and Main server can communicate in the following way: Input server reads data from stdin, then encrypts the data using Main server's public key and sends over the network, then the Main server can decrypt the data using Main server's private key. Similarly, it can be done in the other direction. Also, given that messages can be modified by an attacker, some hash value can be appended to the actual data (using pair function) and then encrypted, to enable data verification. However, attacker may reorder messages and repeat messages, so servers can use some counter to enumerate each message and ensure that the order is preserved.
== Computational class ==
It should be Turing-complete, except if the language is paradoxical in its definition, which does not seem trivial to tell.
== Interpreters ==
Unimplemented.
Category:Languages
Category:Turing_complete
Category:Unimplemented
Category:2020