A microscopic model of a Josephson junction between two superconducting plates is proposed and analysed. For this model, the nonequilibrium steady state of the total system is explicitly constructed and its properties are analysed. In particular, the Josephson current is rigorously computed as a function of the phase difference of the two plates and the typical properties of the Josephson current are recovered.