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.