PROBABILITY TIMED AUTOMATA FOR INVESTIGATING COMMUNICATION PROCESSES

被引:2
作者
Piech, Henryk [1 ]
Grodzki, Grzegorz [1 ]
机构
[1] Czestochowa Tech Univ, Inst Comp & Informat Sci, PL-42201 Czestochowa, Poland
关键词
protocol logic; probabilistic timed automata; communication security; SECURITY; VERIFICATION; LOGIC;
D O I
10.1515/amcs-2015-0031
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
Exploitation characteristics behaves as a decreasing valors factor (DVF) which can be connected with degradation processes. It is a structure that consists of independent attributes which represent situations generally connected with a given exploitation factor. The multi-attribute structure contains attributes directly and indirectly referring to the main factor. Attribute states, by definition, can only maintain or decrease their values. Such situations are met in security, reliability, exploitation, fatigues and many complex one-directed or irreversible processes. The main goal refers to protocol security analysis during the realization of the communication run that specifies the assessment of the level of current and oncoming threats connected with cryptography authentication. In the communication run, the operations of different protocols mutually interleave. Our concept is based on the algorithm of attributes correction during exploitation process realization (Blanchet et al., 2008). The monitoring and correcting procedures make it possible to provide forecast information about possible threats on the basis of the structure of the current attribute values.
引用
收藏
页码:403 / 414
页数:12
相关论文
共 17 条
[1]   SeVe: automatic tool for verification of security protocols [J].
Anh Tuan Luu ;
Sun, Jun ;
Liu, Yang ;
Dong, Jin Song ;
Li, Xiaohong ;
Thanh Tho Quan .
FRONTIERS OF COMPUTER SCIENCE, 2012, 6 (01) :57-75
[2]   An intruder model with message inspection for model checking security protocols [J].
Basagiannis, Stylianos ;
Katsaros, Panagiotis ;
Pombortsis, Andrew .
COMPUTERS & SECURITY, 2010, 29 (01) :16-34
[3]   Distributed temporal logic for the analysis of security protocol models [J].
Basin, David ;
Caleiro, Carlos ;
Ramos, Jaime ;
Vigano, Luca .
THEORETICAL COMPUTER SCIENCE, 2011, 412 (31) :4007-4043
[4]   Automated verification of selected equivalences for security protocols [J].
Blanchet, Bruno ;
Abadi, Martin ;
Fournet, Cedric .
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2008, 75 (01) :3-51
[5]   Logic of authentication [J].
Burrows, Michael ;
Abadi, Martin ;
Needham, Roger .
Operating Systems Review (ACM), 1989, 23 (05) :1-13
[6]   Computing Knowledge in Security Protocols Under Convergent Equational Theories [J].
Ciobaca, Stefan ;
Delaune, Stephanie ;
Kremer, Steve .
JOURNAL OF AUTOMATED REASONING, 2012, 48 (02) :219-262
[7]   To know or not to know: epistemic approaches to security protocol verification [J].
Dechesne, Francien ;
Wang, Yanjing .
SYNTHESE, 2010, 177 :51-76
[8]   FSM encoding for BDD representations [J].
Gosti, Wilsin ;
Villa, Tiziano ;
Saldanha, Alex ;
Sangiovanni-Vincentelli, Alberto L. .
INTERNATIONAL JOURNAL OF APPLIED MATHEMATICS AND COMPUTER SCIENCE, 2007, 17 (01) :113-128
[9]  
Gu TL, 2005, INT J AP MAT COM-POL, V15, P141
[10]  
Kwiatkowska M, 2004, INT CONF QUANT EVAL, P322