SPECIFICATION AND ANALYSIS OF A COMPOSITION OF PROTOCOLS

被引:0
|
作者
LUNDY, GM
机构
[1] Department of Computer Science, Naval Postgraduate School, Monterey
关键词
D O I
10.1016/0020-0255(93)90079-2
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
A composite protocol constructed from two smaller protocols is formally specified, and a proof of correctness is given. The formal specification of the composite protocol is constructed from the formal specification of the two protocols from which it is composed, and the proof of the composite protocol is an expansion of the correctness proofs of the two smaller protocols. The composite protocol is a data-compression protocol which combines two well-known data-compression protocols, achieving further compression. The protocol processes are specified as a set of actions, each of which has a guard, or Boolean expression. An action may take place only if its guard is true and is an atomic event. Verification is accomplished by proving that the set of states satisfying an invariant is closed.
引用
收藏
页码:221 / 239
页数:19
相关论文
共 50 条
  • [31] Modular composition of redundancy management protocols in distributed systems: An outlook on simplifying protocol level formal specification & verification
    Sinha, P
    Suri, N
    [J]. 21ST INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING SYSTEMS, PROCEEDINGS, 2001, : 255 - 263
  • [32] HIERARCHY COMPOSITION OF PROTOCOLS
    ANISIMOV, NA
    [J]. AVTOMATIKA I VYCHISLITELNAYA TEKHNIKA, 1990, (01): : 3 - 10
  • [33] Secure Composition of Protocols
    Cortier, Veronique
    [J]. THEORY OF SECURITY AND APPLICATIONS, 2012, 6993 : 29 - 32
  • [34] MuFASA: A Tool for High-level Specification and Analysis of Multi-factor Authentication Protocols
    Sinigaglia, Federico
    Carbone, Roberto
    Costa, Gabriele
    Ranise, Silvio
    [J]. EMERGING TECHNOLOGIES FOR AUTHORIZATION AND AUTHENTICATION, ETAA 2019, 2020, 11967 : 138 - 155
  • [35] USE OF A FORMAL DESCRIPTION TECHNIQUE IN THE SPECIFICATION OF AUTHENTICATION PROTOCOLS
    VARADHARAJAN, V
    [J]. COMPUTER STANDARDS & INTERFACES, 1990, 9 (03) : 203 - 215
  • [36] Exploring fair exchange protocols using specification animation
    Boyd, C
    Kearney, P
    [J]. INFORMATION SECURITY, PROCEEDINGS, 2001, 1975 : 209 - 223
  • [37] Towards an Adaptive Grid Scheduling: Architecture and Protocols Specification
    Thabet, Ines
    Hanachi, Chihab
    Ghedira, Khaled
    [J]. AGENT AND MULTI-AGENT SYSTEMS: TECHNOLOGIES AND APPLICATIONS, PROCEEDINGS, 2009, 5559 : 599 - 608
  • [38] PETRI NET BASED MODELS FOR THE SPECIFICATION AND VALIDATION OF PROTOCOLS
    DIAZ, M
    AZEMA, P
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1985, 188 : 101 - 121
  • [39] Specification of timed authentication protocols with colored Petri nets
    Jakubowska, G
    Srebrny, M
    [J]. ADVANCED COMPUTER SYSTEMS, PROCEEDINGS, 2002, 664 : 383 - 392
  • [40] A Formal Specification and Verification Framework for Timed Security Protocols
    Li, Li
    Sun, Jun
    Liu, Yang
    Sun, Meng
    Dong, Jin-Song
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2018, 44 (08) : 725 - 746