We study proof-search in the propositional BI-logic that can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic with its underlying sharing interpretation. BI is the basis of new foundations for Computer Science applications (logic programming, reasoning about mutable data structures). We propose a labelled tableau calculus for BI, the use of labels making it possible to generate countermodels. We show that from a given formula A, a non-redundant tableau construction procedure terminates and yields either a tableau proof of A or a finite countermodel of A in terms of the Kripke resource monoid semantics. Moreover, we prove the finite model property for BI with respect to this semantics.