Abstract

Abstract
This work presents a novel machine-checked tight security proof for XMSS-a stateful hash-based signature scheme that is (1) standardized in RFC 8391 and NIST SP 800-208, and (2) employed as a primary building block of SPHINCS+, one of the signature schemes recently selected for standardization as a result of NIST's post-quantum competition. In 2020, Kudinov, Kiktenko, and Fedoro pointed out a flaw affecting the tight security proofs of SPHINCS+ and XMSS. For the case of SPHINCS+, this flaw was fixed in a subsequent tight security proof by Hulsing and Kudinov. Unfortunately, employing the fix from this proof to construct an analogous tight security proof for XMSS would merely demonstrate security with respect to an insufficient notion. At the cost of modeling the message-hashing function as a random oracle, we complete the tight security proof for XMSS and formally verify it using the EasyCrypt proof assistant. (Note that this merely extends the use of the random oracle model, as this model is already required in other parts of the security analysis to justify the currently standardized parameter values). As part of this endeavor, we formally verify the crucial step common to the security proofs of SPHINCS+ and XMSS that was found to be flawed before, thereby confirming that the core of the aforementioned security proof by Hulsing and Kudinov is correct. As this is the first work to formally verify proofs for hash-based signature schemes in EasyCrypt, we develop several novel libraries for the fundamental cryptographic concepts underlying such schemes-e.g., hash functions and digital signature schemes-establishing a common starting point for future formal verification efforts. These libraries will be particularly helpful in formally verifying proofs of other hash-based signature schemes such as LMS or SPHINCS+.

Abstract
CANopen is a truly open protocol that has not been developed by one company alone. Several working groups, consisting of many different device manufacturers and end-users, have co-operated to produce the CANopen standards, now under the supervision of the CAN in Automation organisation. CANopen has been produced as a result of EU funding. This article gives an overview of some of the fundamental concepts of CANopen communication and of CANopen implementation.

Abstract
CANopen is a field level communication protocol for industrial automation distributed applications. The acceptance of CANopen is already widespread and continues growing, because it offers not only all the well known features of CAN for real-time communication, but also a powerful set of higher level Application Layer services. These services implement an object-oriented distributed environment for simplified system integration, but still they allow for a very high level of communication efficiency. Often, sensors and actuators have to be placed at geographically remote locations, at considerable distances from the processor(s) running a control application. When this is the case, a possible solution, that is gaining increasing popularity, is to use an autonomous I/O module, located close to the sensors and actuators, that provides the application with an interface to these devices. For this to be possible, the application must be distributed between the remote I/O module and the local processor(s) using a communication network to allow the different parts to cooperate. This work is centred on the development of an I/O module of the type previously described, based on the SAB-C167CR-LM chip from SIEMENS. The device is able, on one hand, to interface with sensors and actuators using digital signals and, on the other hand, to communicate using the CANopen protocol. In other words, the I/O module makes sensors and actuators accessible via the CAN bus, using the CANopen protocol. The objective is to show that CANopen can be implemented over new hardware platforms, in minimum time, with satisfactory results. It is shown that CANopen provides a systems-integrator-friendly object-oriented environment and that for this reason, the CANopen Communication Profile greatly simplifies the implementation of distributed applications in CAN based systems. Furthermore, CANopen also provides flexible realtime data transfer mechanisms that are able to meet time-critical constraints and, therefore,make CANopen a good solution for distributed control environments.

Abstract

Abstract