What does well-typed mean?

Question

I am currently studying Cryptography and I don't really understand what does 'well-typed' mean when talking about secure cryptographic protocols. I can't find any reasonable explanation on the internet either.

It would be great if someone could give definition and maybe example.

For example quote from “prosecco.gforge.inria.fr”:

The basic soundness theorem for the type system states that well-typed process do not reveal their secrets." So what is 'well-typed'?

Answer 1

When they write “well-typed”, they’re simply stating that the process $P$ is well-typed in context, or type environment. (Where the type environment contains a set of type assumptions occurring in $P$.)

Keeping it simple: you can think of the term as a kind of classification. The term origins in Type Theory and is (more-or-less frequently) used in relation to programming languages, mathematical foundations, proof assistants, linguistics, social sciences, etc.

In cryptography, the term can be used when describing things like – for example – “well-typed attacks” (example paper), or to claim and prove – for example – that well-typed protocols are robustly safe under certain, defined conditions (example paper). There are ample other uses in crypto, where “well-typed” always depends on the individual context.

Let me try to (roughly) generalize it for your convenience: the context (better: type environment) always defines if something is “well-typed” in that individual context (better: type environment), or if it fails to fit the rules and/or assumptions of the type environment in one or more aspects. So, whenever something fits (better: complies to) the rules and assumptions of the type environment, it can be called “well-typed”.

In the case you’re quoting, that means that the process they are describing does not reveal its secrets due to the fact that the basic soundness theorem for the type system they are using states that well-typed process do not reveal their secrets. In novice words: we’ve got this type system that allows us to prove that processes do not reveal their secrets when they follow certain rules defined by that type system. If we build something new and ensure our thingy follows the same rules of that type system, we can assume we are building something that does not reveal its secrets either… because it is “well-typed” within that system. In the end, this makes it easier to prove certain characteristics (like security aspects).

Answer 2

“Well-typed” relates to a type system. This is a general concept in computer science, the usage here is an example of the general concept and is not specific to cryptography. “Well-typed” does not refer to a cryptographic protocol, but to a theory (model) in which a protocol is described.

A type system is a way to assign properties (called types) to components of programs. For example, a type system might make stipulations like the following:

• The program fragment int x; declares a variable called x whose type is “integer”.
• Integer literals such as 3 and 42 are expressions of the type “integer”.
• String literals such as "hello" and "42" are expressions of the type “string”.
• If x is a variable with the type “integer”, then x is an expression of the type “integer”.
• If E_1 and E_2 are expressions of the type “integer”, then E_1 + E_2 is an expression of the type “integer”.
• If x is a variable which has the type “integer” and E is an expression of the type “integer”, then x := E is a valid (well-typed) program. If E does not have the type “integer”, then x := E is an invalid (ill-typed) program.

The ultimate goal of most type systems is to declare that certain programs are well-typed, i.e. that they're correct (with respect to this type system). They achieve this by assigning types to program fragments, to variables, to functions, etc. and detecting conflicts (e.g. trying to assign a string value to an integer variable, trying to apply a function to an argument which is not of a type that it can handle). Most programming languages have a type system, such that ill-typed programs are rejected, either at run time (dynamic typing) or at compile time (static typing).

Type systems can encompass a wide variety of properties. The most common class of property has to do with the structure of data, such as:

• “this is an integer“
• “this is an integer modulo $2^{32}$ using the smallest nonnegative representative”
• “this is a list of integers”
• “this is a function that takes an integer as argument and returns an integer”

But type systems can describe arbitrarily complex properties. That makes it harder to decide whether a program has a correct type, but makes the type system provide more useful information. Here are some example properties that a sufficiently sophisticated type system might model:

• “this is a prime integer”
• “this is a list of integers whose length is the value of the expression x + y”
• “this is a terminating function that takes an integer as argument and returns an integer”
• “this function $f$ takes two arguments $(p,s)$ and returns two values $(p',s')$, such that the value of $p'$ depends only on $p$ and not on $s$”

In that last example, you can see a security property emerging: if we think of $p$ and $p'$ as public values and $s$ and $s'$ as secret values, the property states that public values do not depend on secret values. In other words, the function $f$ preserves the confidentiality of secret values.

Soundness relates a type system with execution rules (an execution semantics) for the programming language. It is a formal property that states that if a program is well-typed, then all runtime states of the program (as modeled in the semantics) are also well-typed. Most type systems are designed to be sound for the usual semantics of the language. This way, information given by the type system about the program translates into information about the program's execution.

The paper that you're reading defines a type system for processes (describing communication protocols) that classifies messages according to which principals know their content. The execution rules describe the propagation of messages. The soundness of the type system means that the initial classification of who knows what is preserved during the execution of the protocol. This holds for well-typed processes, i.e. processes for which the classification (typing) rules give a result. Thus processes that are classified as valid by the type system will not reveal secret data during their execution.