PROPOSAL: a tool for propagation of charged leptons. The search for astrophysical high-energy neutrinos is one of the most important approaches to pin-point the sources of cosmic rays. The advantage of using these neutral and only weakly-interacting particles as messengers in order to look deep into the sources themselves is at the same time the main challenge, as extremely large detectors are needed to measure a significant signal. With the finalization of the large underground detectors IceCube and ANTARES, the quantity and the quality of the recorded data are now at a stage where many analyses have a sensitivity limited by the systematic error rather than statistical uncertainties. Such an error source is the Monte Carlo description of the lepton energy losses before a lepton reaches the detector and of all leptons within the detector. A very accurate simulation of the propagation of muons through large amount of matter is needed because a muon may sustain hundreds of interactions before it is detected by the experiment. Requirements on the precision of the muon propagation code are very stringent. A stochastical correct description of the series of lepton interactions within the detector is needed for a correct conclusion from the measured signature to the lepton energy respectively neutrino energy. In this paper, the Monte Carlo code PROPOSAL (Propagator with optimal precision and optimized speed for all leptons) is presented as a public tool for muon propagation through transparent media. Up-to-date cross sections for ionization, bremsstrahlung, photonuclear interactions, electron pair production, Landau-Pomeranchuk-Migdal and Ter-Mikaelian effects, muon and tau decay, as well as Moli`ere scattering are implemented for different parametrizations. Thus, a full study of the systematic uncertainties is possible from the theoretical description of lepton energy loss in the context of high-energy neutrino analyses and other astroparticle physics experiments that rely on the proper description of lepton propagation. A numerical precision of better than 10-6 is achieved, setting the systematic error for high-energy neutrino analyses to a minimum from the numerical prospective.