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 shown that all data sent over the encrypted heats on exchange messages only if they are authorized to do so. The its hosts modelled by set concurrent processes communicate via unidirectional buffers. Each process viewed as state machine. has been formally verified commercially-available VERUS system.