Dynamic Secure-Emulation

We present probabilistic dynamic I/O automata, a framework to model dynamic probabilistic systems. Our work extends dynamic I/O Automata formalism from Attie & Lynch to  probabilistic setting. The original dynamic I/O Automata formalism included operators for parallel composition, action hiding, action renaming, automaton creation, and behavioral sub-typing by means of trace inclusion.  They can model mobility by using signature modification. They are also hierarchical: a dynamically changing system of interacting automata is itself modeled as a single automaton.

Our work extends to probabilistic settings all these features.  Furthermore, we prove sufficient (weak) conditions to obtain the implementation monotonicity with respect to automata creation and destruction. Secondly, we extends composable secure-emulation  from Canetti & al. to dynamic settings, an important tool towards the formal verification of protocols combining  probabilistic distributed systems and cryptography in dynamic settings (e.g. blockchains, secure distributed computation, cybersecure distributed protocols etc). Here again, we prove sufficient (weak) conditions to obtain the secure-emulation monotonicity with respect to automata creation and destruction.