Abstract machines for communication security
Pierre Bieber, N. Boulahia-Cuppens, Todd C. Lehmann, E. van Wickeren · 2002
An existing formal software development method called B is used to build and verify specifications of a communication channel, cryptographic functions and security properties. The authors show on an example how these basic specifications may be combined in order to write abstract specifications of cryptographic protocols and to verify their security.>