Logic-Based Security Architecture for Systems Providing Multihop Communication

Security is a basic element of distributed systems such as ad hoc and sensor communication networks. Several standards define security requirements and enforcers, such as ITU-T Recommendations X.800 and X.805. It is essential to specify and analyze protocols to know which security requirements they achieve. This paper presents a logic-based security architecture (LBSA). LBSA is a systematic way to test if a protocol is secure by checking what security requirements are achieved. Different rules, actions, and sets which fit into the proposed LBSA are included, new ones are also added to complete the architecture. The key advantage of LBSA is that it enables a security protocol to prove its correctness mathematically. Mathematical proofs provided by LBSA cover more cases that usually cannot be covered exhaustively by simulation tools. This paper also specifies and analyzes several security enforcers and protocols and mathematically proves which security requirements they achieve. Mapping between security requirements and inference rules/actions is also provided to facilitate the use of LBSA. Some enforcers are analyzed using LBSA to demonstrate how they achieve security requirements. Finally, we take Ariadne protocol as a case study and show how to use the proposed LBSA architecture to prove that this protocol is secure.