Equational Approach to Formal Analysis of TLS

Author

Ogata, Kazuhiro ; Futatsugi, Kokichi

Author_Institution

NEC Software Hokuriku, Ltd.

fYear

2005

fDate

10-10 June 2005

Firstpage

795

Lastpage

804

Abstract

TLS has been formally analyzed with the OTS/CafeOBJ method. In the method, distributed systems are modeled as transition systems, which are written in terms of equations, and it is verified that the models have properties by means of equational reasoning. TLS is the latest version, or the successor of SSL, which is probably the most widely deployed security protocol. Among the results of the analysis are that pre-master secrets cannot be leaked, when a client has negotiated a cipher suite and security parameters with a server, the server has really agreed on them, and client cannot be identified if they do not send their certificates to servers

Keywords

algebraic specification; formal verification; protocols; rewriting systems; security of data; theorem proving; OTS/CafeOBJ method; algebraic specification; cipher suite; distributed systems; equational reasoning; interactive theorem proving; observational transition systems; secure sockets layer; security protocol; transport layer security; Data security; Equations; Information analysis; Information science; Information security; National electric code; Protection; Specification languages; Transport protocols; Web server; algebraic specification; interactive theorem proving; rewriting; security; verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Distributed Computing Systems, 2005. ICDCS 2005. Proceedings. 25th IEEE International Conference on

Conference_Location

Columbus, OH

ISSN

1063-6927

Print_ISBN

0-7695-2331-5

Type

conf

DOI

10.1109/ICDCS.2005.32

Filename

1437139