This paper introduces a new logic-based technique for detecting security protocol weaknesses that are exploitable by freshness and interleaving session attacks. This technique is realised as a special purpose logic to be used throughout the protocol design stage, where a draft of the protocol is subjected to formal analysis prior to its publication or deployment. For any detected failures the analysis also reveals their cause, facilitating design corrections. The proposed Attack Detection Logic is introduced and its details, including the language, predicates, axioms, rules, semantics as well as soundness and completeness are presented. The effectiveness of the logic is evaluated in a case study, where it is demonstrated how to use the Attack Detection Logic as part of the design process of security protocols. Further, the logic is applied to a range of security protocols, including protocols with known weaknesses and protocols that are known to be secure. The logic's ability to detect various attacks is established by demonstrating that for protocols with known weaknesses, at least one detection rule is activated and no detection rule is activated for protocols without weaknesses. This case study confirms the logic's ability to detect design weaknesses exploitable by freshness and interleaving session attacks.

In the emerging IoT ecosystem in which the internetworking will reach a totally new dimension the crucial role of efficient security solutions for embedded devices will be without controversy. Typically IoT-enabled devices are equipped with integrated circuits, such as ASICs or FPGAs to achieve highly specific tasks. Such devices must have cryptographic layers implemented and must be able to access cryptographic functions for encrypting/decrypting and signing/verifying data using various algorithms and generate true random numbers, random primes, and cryptographic keys. In the context of a limited amount of resources that typical IoT devices will exhibit, due to energy efficiency requirements, efficient hardware structures in terms of time, area, and power consumption must be deployed. In this paper, we describe a scalable word-based multivendor-capable cryptographic core, being able to perform arithmetic operations in prime and binary extension finite fields based on Montgomery Arithmetic. The functional range comprises the calculation of modular additions and subtractions, the determination of the Montgomery Parameters, and the execution of Montgomery Multiplications and Montgomery Exponentiations. A prototype implementation of the adaptable arithmetic core is detailed. Furthermore, the decomposition of cryptographic algorithms to be used together with the proposed core is stated and a performance analysis is given.

This work is concerned with the possible exploitation of weaknesses in security protocols by attackers using parallel session attacks and discovering ways of eliminating these weaknesses. A new analysis is presented on the reasons why security protocols, with certain weaknesses in their design, are vulnerable to parallel session attacks. Building on this analysis a new set of design requirements is proposed, whose aim is to eliminate these vulnerabilities. The proposed set of design requirements is evaluated by applying them to a range of security protocols with known weaknesses as well as protocols known to be free of these weaknesses. The results of the evaluation indicate that the set of design requirements are effective as: protocols with known weaknesses violate some of the rules, while protocols without weaknesses do not violate any of the rules.

This paper is concerned with detection and prevention of weaknesses in the design of security protocols. These weaknesses can be exploited by an attacker mounting attacks that compromise the security of the protocol. A novel theory defining weaknesses caused by the symmetry of cryptographic messages in protocols is introduced. This theory incorporates new rules describing the cases when the symmetry of messages has a structural weakness that is exploitable by parallel session attacks. Further, the rationale behind the Symmetry rules is presented and the structures of detected generic attacks for each rule are provided. Additionally, the Symmetry rules are applied to a protocol that is vulnerable to a parallel session attack. It is demonstrated that the proposed theory successfully detects the weaknesses caused by the symmetry of protocol messages, which lead to parallel session attacks.

Many peer-to-peer security protocols proposed for wireless communications use one-time shared secrets for authentication purposes. This paper analyses online update mechanisms for one-time shared secrets. A new type of attack against update mechanisms, called desynchronisation attack, is introduced. This type of attack may lead to a permanent denial of service condition. A case study demonstrates the effectiveness of desynchronisation attacks against a security protocol for mobile satellite communications. A new mutual authentication protocol for satellite communications, incorporating a resynchronisation capability, is proposed to counter the disruptive effects of desynchronisation attacks. The new protocol has an esynchronisation phase that is initiated whenever desynchronisation is suspected. Thus, the possibility of causing permanent denial of service conditions by mounting desynchronisation attacks is eliminated. A security analysis of the proposed protocol establishes its resistance against attacks like replay attacks, dictionary attacks, and desynchronisation attacks.

Security is a primary problem in wireless electronic communications. However, the limitations of Wireless Sensor Networks (small size, low battery capacity and exposed communication media) often turn the focus to power consumption rather than security. However, insufficient security protection can leave a WSN application open to attack, rendering the supplied service not trustworthy or unavailable. This paper presents a formal verification of a cluster based key management protocol for Wireless Sensor Networks. A number of weaknesses are identified in the verified protocol that can be exploited by an intruder. These weaknesses allow various attacks, such as impersonating the base station to the network, impersonating a cluster head to sensor nodes or to disrupt the network configuration. A detailed discussion on these weaknesses is presented and modifications to the protocol are proposed to fix these weaknesses. Successful verification of the proposed fixed protocol demonstrates its correctness.

The use of security protocols to protect sensitive information is critical. However, flaws in the design of security protocols can make them ineffective. This paper discusses various attacks against security protocols that exploit weaknesses in their design and a key-distribution protocol is analysed using a model checker. The analysis reveals weaknesses in the protocol, which can be exploited in a parallel session attack that allows an attacker to impersonate a legitimate principal. Correction to the protocol are proposed and a formal analysis of the fix is presented. The results of this analysis provide confidence in the correctness and effectiveness of the proposed corrected protocol.

Security protocols are one of the most critical elements in enabling the secure communication and processing of information. The presence of flaws in published protocols highlights the complexity of security protocol design. Only formal verification can provide strong confidence in the correctness of security protocols and is considered an imperative step in their design. This paper presents a new theoretical concept, called Layered Proving Trees, for automatically applying logical postulates in logic-based security protocol verification.An algorithm for the new concept is introduced and the soundness and completeness of the technique is proved. Empirical results on the performance of the algorithm are presented. The presented proofs and empirical results demonstrate the feasibility and effectiveness of the Layered Proving Tree approach.