What does this mean, exactly?
The purpose of the environment is to model "everything else happening in the universe" besides the protocol execution. In the UC model, the adversary is allowed to talk to the environment during the execution of the protocol. So UC security means "security no matter what else is going on in the world, even if other things are going on in the world during the protocol execution." For instance, the adversary could be running instances of other protocols (or the same protocol), against the honest parties, who could be using related inputs, etc.
There are several flavors of standalone security definitions, not all equivalent. But for the purposes of this question, think of standalone security as exactly the same as UC security, except that but the adversary is not allowed to talk to the environment during the protocol execution. They can talk only before and after the execution. In this model we cannot use the environment to capture an adversary who is doing "other things" during the execution of our protocol. We can model adversaries who run other protocols with honest parties on related inputs after or before our execution, but not during.
A protocol supports sequential composition if it is secure when many instances are executed sequentially, possibly on related inputs. It's easy to express this in both standalone and UC model. You can capture sequential composition by just having the adversary pass along its state between executions. Pre/post-execution communication with the environment is enough to do this, so it's fine in the standalone model.
A protocol supports concurrent composition if it is secure when many instances are executed concurrently, possibly on related inputs. It is not possible to express this in standalone -- only in UC. So standalone security does not guarantee this property, and there are indeed counterexamples of standalone-secure protocols that are insecure when run concurrently.
This restriction of standalone security (i.e., not talking to the environment during the protocol execution) is actually used in security proofs in the standalone model. A common technique for the simulator is to "rewind" the adversary, meaning to revert his internal state back to a previous time in the protocol. This is safe in the standalone model, because the adversary is detached from the environment. But it's not valid in the UC model because if you're trying to rewind the adversary back to round $r$ of the protocol, the adversary might have already spoken to the environment at round $r+1$. The environment cannot be rewound, so this would cause the environment to notice the difference between real & simulated --- this technique cannot be used in a UC security proof.
A UC proof works if you show that the environment can not tell if it is interacting with the real adversary and the real protocol, or the simulator/ideal adversary and ideal functionality.
Yes.
To this end, for the proof one must define, for each real adversary, a simulator.
Yes, but there is a shortcut. Take any environment and adversary that you wish to consider, and imagine logically moving the adversary into the environment so that all that is left as a syntactic "dummy adversary". The dummy adversary just says whatever the logical adversary (living inside the environment) tells it, and also reports back all the messages it sees as they are received. This doesn't change the interaction, it only repackages the parts. So every UC interaction can be expressed in terms of an equivalent interaction where the adversary is such a dummy adversary. Since UC security quantifies over all environments, it just suffices to prove security with respect to a dummy adversary.
My (other) question is, how do we define this simulator? In proofs, I only ever see the simulator being defined by how it behaves when it receives a message from the ideal functionality and how it behaves when it receives a message from the adversary? But why is it never described by how it behaves when it receives a message from the environment? The environment wants a two-way interaction with the real adversary/simulator right? So do we have to define the simulator so it knows how to respond and interact with the environment?
Perhaps this question is cleared up with the understanding of dummy adversaries. When you imagine an interaction with a dummy adversary, you lose the distinction between the environment and the logical adversary embedded in the environment. So the receiving a message from the [logical] adversary / receiving a message from the environment really refer to the same thing. We just know without loss of generality that all communication with the environment will be of the dummy-adversary form: environment says "here is a message to send in the protocol", dummy adversary / simulator has to report back all [simulated] protocol messages that are seen.
Also, I would be most grateful if you should show me example proofs in the UC framework. The shorter/easier the better, just so I can get my head around it.
Nothing comes immediately to mind. You might want to search for "UC security" + "lecture notes". Also you may be interested in the following recent paper that presents a simplified model of UC that nevertheless is sufficient for 99% of use cases:
