Using a simple example we demonstrate the necessity of a formal modelling of security. We explain the established notion of simulatable security (e.g. reactive simulatability by Backes, Pfitzmann, Waidner, or universal composability by Canetti) and show how this model can be extended to encompass quantum security (cf. also the work of Ben-Or, Mayers). We conclude with a Quantum Embedding Theorem that allows to securely use quantum protocols as sub-protocols in classically secure protocols.