Generation of ProVerif typed pi calculus, modification of Avatar model for easing translation to ProVerif