In my opinion, the paper is poorly worded and misleading. Admittedly, I have only glanced at the following statement and nearby regions.
The above template expresses a safety property type. A typical vulnerabilityis that currency withdrawal functions, e.g.,transfer, allow an attacker to with-draw currency again before updating her balance.
First, I feel I should collapse some confusion that arises from the misuse of common terms. The attack described is not "Denial of Service." It's "Re-entrance." The former generally means denying access to other users in some way, such as sabotage. The latter is a method of making the contract behave in an unintended (by the creator) way such as sending more money than the requester is entitled to.
Can we use: withdrawals[msg.sender].amount = 0;
after 'transfer'
You shouldn't. A best practice is to use the "Checks, Effects, Interactions" pattern that basically means validate, set the state optimistically, then interact with other contracts and addresses.
The reason you do it like that is to ensure that the contract is in a consistent state with everything accounted for before another contract receives flow control. In the vulnerable configuration, a hostile contract can make a call back to the naive contract where it will find that the accounting has not happened yet. In the simplest conception of the attack, they can withdraw money again.
The attack works because the receiving contract (Attacker) has a fallback function that runs when funds are received and that can be coded to attack the naive victim.
To protect itself, the victim should first get its house in order and perform the accounting as though a successful transfer in the next step is assured. That way, the attacker will see that their entitlement is already reduced and they cannot withdraw the same money again. If the accounting comes after the transfer then their balance will be unchanged every time and that can trick the victim into releasing more funds.
When a contract reverts after a failed transfer (usually the right thing to do), that reverses the optimistic accounting performed earlier, so you can safely use the counter-intuitive order of events.
There is a partial re-entrance guard known as the gas stipend but it is bad practice to rely on it exclusively when the Checks, Effects, Interactions can be followed religiously.
Hope it helps.