Partial Known Message Pre-Image Attack on SHA-1 If the last 448 bits of a sha1 block input are known (only the first 64 bits are unknown). Is it possible to do a preimage attack using SAT solvers or something else? Or do I have to brute force all $2^{64}$ possibilities? Is this a kind of reduced sha1?
If you know the last 448 bits, we can assume that this part actually the padding part with length at the end, then you will have 64-bit unknown data for the input to pre-image attack. Since you know the output hash value you can set up a system of equations. In this case, the hash function can be considered as

$$\operatorname{F}:\{0,1\}^{64}\times\{0,1\}^{448} \to \{0,1\}^{160}$$

Now, for every output bit, set up an equation by algebraic evaluation of SHA-1. You will have 160 equations and 64 unknowns.

This type of system is called over-defined when there are more equations than unknowns. However, keep in mind that the system may be inconsistent that means there is a collision there an that has an expected negligible probability.

According to Bard, Courtois, and Jefferson paper;


  if the system of equations is sparse or over-defined, then the SAT-solver technique works faster than brute-force exhaustive search. If the system is both sparse and over-defined, then the systems can be solved quite effectively.


The only problem that we can't see, immediately, the degree of the equations. If they are low degree then the SAT solvers, as Mini-SAT, can be faster than brute-force, according to the result of the paper.