Formal Verification of the Security for Dual Connectivity in LTE

被引：1

作者：

Ben Henda, Noomene ^{[1
]}

Norrman, Karl ^{[1
]}

Pfeffer, Katharina ^{[1
]}

机构：

[1] Ericsson Res, Farogatan 6, S-16480 Stockholm, Sweden

来源：

2015 IEEE/ACM 3RD FME WORKSHOP ON FORMAL METHODS IN SOFTWARE ENGINEERING | 2015年

关键词：

PROTOCOL; TOOL;

D O I：

10.1109/FormaliSE.2015.10

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We describe our experiences from using formal verification tools during the standardization process of Dual Connectivity, a new feature in LTE developed by 3GPP. To the best of our knowledge, this is the first report of its kind in the telecom industry. We present a model for key establishment of this feature and provide a detailed account on its formal analysis using three popular academic tools in order to automatically prove the security properties of secrecy, agreement and key freshness. The main purpose of using the tools during standardization is to evaluate their suitability for modelling a rapidly changing system as it is developed and in the same time raising the assurance level before the system is deployed.

引用

页码：13 / 19

页数：7

共 30 条

[1]

Abadi M, 2004, LECT NOTES COMPUT SC, V2986, P340

[2] Mobile values, new names, and secure communication [J].

Abadi, M ;

Fournet, C .

ACM SIGPLAN NOTICES, 2001, 36 (03) :104-115

[3]

Arapinis M., 2012, Proceedings of the 2012 ACM Conference on Computer and Communications Security, DOI 10.1145/2382196.2382221

[4]

Armando A, 2005, LECT NOTES COMPUT SC, V3576, P281

[5]

Basin D., 2015, IEEE SECURI IN PRESS

[6] An efficient cryptographic protocol verifier based on prolog rules [J].

Blanchet, B .

14TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2001, :82-96

[7]

Blanchet B., AUTOMATIC VERIFICATI

[8]

Blanchet B., PROVERIF 1 88 AUTOMA

[9] Automated formal analysis of a protocol for secure file sharing on untrusted storage [J].

Blanchet, Bruno ;

Chaudhuri, Avik .

PROCEEDINGS OF THE 2008 IEEE SYMPOSIUM ON SECURITY AND PRIVACY, 2008, :417-+

[10] Logic of authentication [J].

Burrows, Michael ;

Abadi, Martin ;

Needham, Roger .

Operating Systems Review (ACM), 1989, 23 (05) :1-13

← 1 2 3 →