%0 Conference Paper %1 Datta:2003:SPC:1035429.1035431 %A Datta, Anupam %A Derek, Ante %A Mitchell, John C. %A Pavlovic, Dusko %B Proceedings of the 2003 ACM workshop on Formal methods in security engineering %C New York, NY, USA %D 2003 %I ACM %K composition crypto %P 11--23 %R 10.1145/1035429.1035431 %T Secure protocol composition %U http://doi.acm.org/10.1145/1035429.1035431 %X Modular composition of security mechanisms is complicated by the way that one mechanism may reveal information that interferes with the security of another. We develop methods for modular reasoning about security protocols, using before-after assertions and protocol invariants. The before-after assertions allow us to prove properties of a sequential composition of protocol steps and therefore enable construction of complex protocols from smaller sub-protocols. Invariants provide a mechanism for ensuring that sub-protocols which are individually secure do not interact insecurely when they are composed to construct a bigger protocol. The application of the method is demonstrated by giving modular formal proofs involving two standard protocols. %@ 1-58113-781-8

@inproceedings{Datta:2003:SPC:1035429.1035431, abstract = {Modular composition of security mechanisms is complicated by the way that one mechanism may reveal information that interferes with the security of another. We develop methods for modular reasoning about security protocols, using before-after assertions and protocol invariants. The before-after assertions allow us to prove properties of a sequential composition of protocol steps and therefore enable construction of complex protocols from smaller sub-protocols. Invariants provide a mechanism for ensuring that sub-protocols which are individually secure do not interact insecurely when they are composed to construct a bigger protocol. The application of the method is demonstrated by giving modular formal proofs involving two standard protocols.}, acmid = {1035431}, added-at = {2012-03-31T16:21:53.000+0200}, address = {New York, NY, USA}, author = {Datta, Anupam and Derek, Ante and Mitchell, John C. and Pavlovic, Dusko}, biburl = {https://www.bibsonomy.org/bibtex/2d7e60a48a75a5ff2dd66c78f342c50a5/giuliano.losa}, booktitle = {Proceedings of the 2003 ACM workshop on Formal methods in security engineering}, description = {Secure protocol composition}, doi = {10.1145/1035429.1035431}, interhash = {0af7769b713efbcadbbfcf61d9152657}, intrahash = {d7e60a48a75a5ff2dd66c78f342c50a5}, isbn = {1-58113-781-8}, keywords = {composition crypto}, location = {Washington, D.C.}, numpages = {13}, pages = {11--23}, publisher = {ACM}, series = {FMSE '03}, timestamp = {2012-03-31T16:21:53.000+0200}, title = {Secure protocol composition}, url = {http://doi.acm.org/10.1145/1035429.1035431}, year = 2003 }