A security property of a protocol is composable if it remains intact even when the protocol runs alongside other protocols in the same system. We describe a method for asserting composable security properties, and demonstrate its usefulness. In particular, we show how this method can be used to provide security analysis that is formal, relatively simple, and still does not make unjustified abstractions of the underlying cryptographic algorithms in use. It can also greatly enhance the feasibility of automated security analysis of systems of realistic size.
展开▼
