Formal Verification of a Secure Network with End-to-End Encryption

A formal specification and verification of a simple secure communications network using end-to-end encryption is presented. It is shown that all data sent over the network is encrypted and all heats on the network exchange messages only if they are authorized to do so. The network and its hosts are modelled by a set of concurrent processes that communicate via unidirectional buffers. Each process is viewed as a state machine. The specification has been formally verified using the commercially-available VERUS verification system.