You have far more freedom in modeling intuitionistic logic than you think. :) In this case, the point is that in a logic for cryptography, you would have a typ

You have far more freedom in modeling intuitionistic logic than you think. :) In this case, the point is that in a logic for cryptography, you would have a type "S" of "bit strings of arbitrary but unknown length" which is restricted in such a way that you cannot eliminate into discrete types (such as the natural numbers). In particular, there would be no way of proving "x != y" for x, y in S at all unless you assume that there was some function which established this. One way to get a model for such a logic is to interpret types as (reflexive) graphs and functions as graph homomorphisms. The resulting category is a topos and hence gives you a model of type theory. There is such a wealth of knowledge about building models for intuitionistic logic that it is difficult to say what can and cannot be done without a thorough literature review.