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.