The goal of this paper is to give a group-theoretic proof of the congruence
subgroup property for $Aut(F_2)$, the group of automorphisms of a free group on
two generators. This result was first proved by Asada using techniques from
anabelian geometry, and our proof is, to a large extent, a translation of
Asada's proof into group-theoretic language. This translation enables us to
simplify many parts of Asada's original argument and prove a quantitative
version of the congruence subgroup property for $Aut(F_2)$.
It is known from work by H. Abels and P. Abramenko that for a classical
Fq-group G of rank n the arithemetic lattice G(Fq[t]) of Fq[t]-rational points
is of type Fn-1 provided that q is large enough. We show that the statement is
true without any assumption on q and for any isotropic, absolutely almost
simple group G defined over Fq.