Formally evaluating the strengths of a given cryptosystem will ensure that no flaws have crept into the application. During our investigation, we adopted Armknecht and Krause's approach to model the E0 encryption function, which does not depend on memory bits and will hold for every clock tick. We devised a polynomial of degree four consisting of 20 variables, 16 considered unknown and four known. We then created an automated tool in the Maple 12 environment (www. maplesoft.com) that finds all the maxterms and their corresponding linear-coefficient superpolys for the E0 encryption function.