Dataset Information

Formal analysis of signal protocol based on logic of events theory.

ABSTRACT: The Signal is an end-to-end encrypted communication protocol composed of a double ratchet (DR) protocol and an extended triple Diffie-Hellman (X3DH) protocol. Its complex ratchet structure and the characteristics of protocol composition make it challenging to realize formal analysis. A formal analysis method based on logic of events theory (LoET) is proposed to conduct a security analysis of the Signal protocol. The method includes inference rules with key relation and key chain as the core to realize the formal analysis of ratchet structure, and the inference relation between sub-protocols is established by putting forward the composition theorem. The proposed method achieves a formal analysis of Signal, revealing that it does not satisfy a strong authentication property during the X3DH phase. The results show that the LoET-based method can be effectively applied in the formal analysis of Signal protocols, thus promoting the application and development of these protocols with ratchet structure and composition properties.

SUBMITTER: Li Z

PROVIDER: S-EPMC11375095 | biostudies-literature | 2024 Sep

REPOSITORIES: biostudies-literature

ACCESS DATA

Publications

Formal analysis of signal protocol based on logic of events theory.

Li Zehuan Z Xiao Meihua M Xu Ruihan R

Scientific reports 20240904 1

The Signal is an end-to-end encrypted communication protocol composed of a double ratchet (DR) protocol and an extended triple Diffie-Hellman (X3DH) protocol. Its complex ratchet structure and the characteristics of protocol composition make it challenging to realize formal analysis. A formal analysis method based on logic of events theory (LoET) is proposed to conduct a security analysis of the Signal protocol. The method includes inference rules with key relation and key chain as the core to r ...[more]

PMID: 39232203

Similar Datasets

Project description:Among the 13 TLRs in the vertebrate systems, only TLR4 utilizes both Myeloid differentiation factor 88 (MyD88) and Toll/Interleukin-1 receptor (TIR)-domain-containing adapter interferon-β-inducing Factor (TRIF) adaptors to transduce signals triggering host-protective immune responses. Earlier studies on the pathway combined various experimental data in the form of one comprehensive map of TLR signaling. But in the absence of adequate kinetic parameters quantitative mathematical models that reveal emerging systems level properties and dynamic inter-regulation among the kinases/phosphatases of the TLR4 network are not yet available. So, here we used reaction stoichiometry-based and parameter independent logical modeling formalism to build the TLR4 signaling network model that captured the feedback regulations, interdependencies between signaling kinases and phosphatases and the outcome of simulated infections. The analyses of the TLR4 signaling network revealed 360 feedback loops, 157 negative and 203 positive; of which, 334 loops had the phosphatase PP1 as an essential component. The network elements' interdependency (positive or negative dependencies) in perturbation conditions such as the phosphatase knockout conditions revealed interdependencies between the dual-specific phosphatases MKP-1 and MKP-3 and the kinases in MAPK modules and the role of PP2A in the auto-regulation of Calmodulin kinase-II. Our simulations under the specific kinase or phosphatase gene-deficiency or inhibition conditions corroborated with several previously reported experimental data. The simulations to mimic Yersinia pestis and E. coli infections identified the key perturbation in the network and potential drug targets. Thus, our analyses of TLR4 signaling highlights the role of phosphatases as key regulatory factors in determining the global interdependencies among the network elements; uncovers novel signaling connections; identifies potential drug targets for infections.

Dataset Information

Formal analysis of signal protocol based on logic of events theory.

Publications

Formal analysis of signal protocol based on logic of events theory.

Similar Datasets

OmicsDI is part of the ELIXIR infrastructure

Tweets