Whether you go with option 1 or 2 from your list really has to do with whether you want the selection to be persistent for any reason as well as other factors. Below I'll list a few things you may want to take into consideration when choosing which methodology to follow.
If you want to allow drag-n-drop reordering of items, using checkboxes may make it simpler for a user not to lose selection state in the processes. If you are not allowing drag-n-drop reordering or don't care if selection state is lost during the processes if it is allowed then using multi-selection via the Ctrl key may be an option.
Long Term Persistence
If the selection being made is to be saved for later and recalled again during a subsequent session or run of the application then consider using a checkbox or the double listbox paradigm because showing highlighted items is generally reserved for transient selection state.
Multi-Selection as Advanced Feature
If multi-selection is expected to be a rare necessity to your users then perhaps burdening the users with check boxes is not the best option since they are not likely to use them the majority of the time. In these cases it may be better to show the checkboxes by entering into a special multi-select mode or to just stick with the Ctrl key method of advanced multi selection. In the edge case where a user needs very fine grain control over selection and ordering and screen real-estate isn't much of a concern then using the method that Bevan proposed in his answer with two separate lists is a decent option as well.
Note that Windows Explorer generally follows the Ctrl key method for advanced multi-selection of files/folders but it can be configured to use checkboxes to represent selection. I've tried it once and switched back and have found most people are not even aware of that feature.