Astract: Mobility creates new challenges for dynamic systems, which need a new conceptional treatment: systems, that deal for example with mobile agents, need extended security concepts to handle the risks, induced by foreign, untrusted agents. In this work we present the paradigm of “nets within nets”, which is well suited to express the dynamics of open, mobile systems. It is furthermore capable of formalising security aspects and analysing the correctness of a given system in terms of the security speci.cation. This approach is attractive since it combines a modelling-oriented view with an exact formalism.
Astract: We present a novel equivalence for cryptographic expressions that overcomes two limitations of classical security models: perfect cryptography and nondeterministic adversary. The uncertainty concerning the robustness of cryptographic primitives against breaking attacks is estimated through probabilistic information. We also define an approximated relation that allows cryptographic expressions (leading the same information) that can be broken with similar probabilities to be indistinguishable from the adversary viewpoint. Finally, we show that the equivalence is preserved when passing to the usual Dolev-Yao model.
Astract: In this paper we first define a formal availability model for avionic data bus protocols. Our model includes an availability policy and some security properties that such protocols should enforce. Then, we consider a particular data bus protocol for avionic system: ARINC 629 BP [AR629]. We use Stochastic Timed Petri Nets to test whether ARINC 629 BP conforms to our security policy and we show that it does not violate the security properties.
Abstract: In this paper we will give an overview of the state-of-the-art methods for automatic proof of correctness of security protocols. The classification we propose is based on three paradigmsL symbolic state exploration, in which infinite set of states are finitely represented via some assertional language, abstractions, in which the protocol behavior is abstracted or approximated in order to obatin conservative correctness proofs and invariant generation, in which a invariant is extracted from a protocol model and proved to imply the desired property.
Abstract: We show that team automata (TA) are well suited to model secure multicast/broadcast communication with possible packet loss. This is a consequence of the natural way in which one-to-many (one-to-all) transmissions typical of multicast (broadcast) sessions can be modelled as communications between the component automata (CA) constituting a TA. In addition, we investigate a formulation of the Generalized Non-Deducibility on Compositions (GNDC) schema in terms of TA with the aim to embed TA in this well-established analysis framework. We intend to use this new setting for the formal verification of security properties for stream signature protocols. Finally, we use TA to model an instance of the EMSS multicast protocol family.
Abstract: Mobile agents believed to be playing an important role in future e-commerce systems, offering great flexibility and improved performances. Mobile agents are processes which can autonomously migrate from host to host. The migration path followed by an agent can be abstracted for programming convenience into an itinerary. A flexible structure of itinerary is used in ``Concordia`` or ``Ajanta`` Agent Systems, using sequence, alternative and set entries. On the other hand, security is a fundamental precondition for the acceptance of mobile agent systems, In order to protect mobile agents, several itinerary protection protocols have been presented for each kind of entry. This papers improves the previous solutions proposing a unique general protocol using Petri nets modeling, providing a minimum route information to visit hosts, and strong protection against tampering and itinerary analysis attack.