A model for secure protocols and their compositions

Author

Heintze, Nevin ; Tygar, J.D.

Author_Institution

AT&T Bell Labs., Murray Hill, NJ, USA

Volume

22

Issue

1

fYear

1996

fDate

1/1/1996 12:00:00 AM

Firstpage

16

Lastpage

30

Abstract

The paper develops a foundation for reasoning about protocol security. We adopt a model-based approach for defining protocol security properties. This allows us to describe security properties in greater detail and precision than previous frameworks. Our model allows us to reason about the security of protocols, and considers issues of beliefs of agents, time, and secrecy. We prove a composition theorem which allows us to state sufficient conditions on two secure protocols A and B such that they may be combined to form a new secure protocol C. Moreover, we give counter-examples to show that when the conditions are not met, the protocol C may not be secure

Keywords

belief maintenance; cryptography; distributed processing; inference mechanisms; knowledge based systems; message authentication; protocols; software agents; theorem proving; agent beliefs; composition theorem proving; protocol security properties; protocol security reasoning; secrecy; secure protocol compositions; secure protocol model; time; Authentication; Clocks; Computer science; Computer security; Concatenated codes; Concrete; Cryptographic protocols; Cryptography; Logic; Sufficient conditions;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.481514

Filename

481514