Next: The intruder Up: Abstract data types Previous: Principles

### Public-key encryption and signature

The following ACT ONE definition models the public-key encryption operation. It does not rely on any particular implementation (e.g. RSA) nor on any particular mathematical concept. For simplicity, we assume the previous definition of the public and the private keys as base values and the existence of an operation `match(public key, private key)` that returns true if the public key corresponds to the private key.

```type EncryptedMessage is Message, PublicKey, PrivateKey
sorts EncryptedMessage
opns
E (*! constructor *) : PublicKey, Message -> EncryptedMessage
D : PrivateKey, EncryptedMessage -> Message
eqns
forall msg : Message,
pubkey : PublicKey
prvkey : PrivateKey
ofsort Message
Match(pubkey,prvkey) => D(prvkey,E(pubkey,msg)) = msg;
not(Match(pubkey,prvkey)) => D(prvkey,E(pubkey,msg)) = Message_Junk;
endtype```

The encryption function `E` and the decryption function `D` are defined as abstract operations that are the reverse of each other. Decryption with a bad key is handled explicitly and produces a distinguished value `Message_Junk` without any meaning. Once encrypted, the only way to access the message is through the decryption function called with the right private key. Obviously, no operation allows to read the private key.

The signature operation is defined in the same way with a verification function `V` that returns true if the signature is correct (i.e. the verification is performed with the right public key). We consider that a signed message is the message in clear and an encrypted hash of it. Thus our model needs the `GetMessage` operation to access the message without any key.

```type SignedMessage is Message, PublicKey, PrivateKey
sorts SignedMessage
opns
S (*! constructor *) : PrivateKey, Message -> SignedMessage
V : PublicKey, SignedMessage -> Message
GetMessage : SignedMessage -> Message
eqns
forall msg : Message,
pubkey : PublicKey
prvkey : PrivateKey
ofsort Message
V(pubkey,S(prvkey,msg)) = Match(pubkey,prvkey);
GetMessage(S(prvkey,msg)) = msg;
endtype```

We assume with these definitions that no one can break the public key cryptosystem by getting the message in clear from the encryted message and the public key, or forging a signed message from the message in clear and the public key. Note that LOTOS easily provides processes that transgress this rule, and thus break any cryptosystem. Great care must be taken to avoid this kind of unrealistic behaviours.