Following 1 and some modern notations, I aim to describe a formal definition of a $3$-step interactive $\Sigma$-protocol with formal proofs. So:
For an NP relation $\mathcal{R}$ a $\Sigma$-protocol is a $3$-step protocol between the Prover and the Verifier consisting of three algorithms $\sigma_{com}, \sigma_{resp}, \sigma_{ver}$ with respect to the security parameter $\lambda$ and with the following definition:
$\sigma_{com}^\lambda(x, w) \rightarrow (t, i)$: for the public input $x$, and witness $w$ it generates a commitment $t$ and some side information $i$;
$\sigma_{resp}^\lambda(x,w,i,c) \rightarrow s$: for the public input $x$, witness $w$, and side information $i$ it generates a response $s$ for the challenge $c \in {0,1}^\lambda$;
$\sigma_{ver}^\lambda(t,c,x,s) \rightarrow {0, 1}$: for the public input $x$, the response $s$, the challenge $c$, and the commitment $t$ it outputs bit $b \in {0,1}$ assuming $(x, w) \in \mathcal{R}$ if $b = 1$ and $(x, w) \notin \mathcal{R}$ otherwise.
A $\Sigma$-protocol has the following properties:
Completeness
A $\Sigma$-protocol is said to be complete if for any pair $(x,w)$, such that $(x,w) \in \mathcal{R}$, and any challenge $c\in {0,1}^\lambda$:
\[Pr\Big[\sigma_{ver}^\lambda(t,c,x,s) = 1\Big] \geq 1 - \mathsf{negl}(\lambda).\]Special Soundness
A $\Sigma$-protocol is said to be special sound if there exists a special polynomial-time extractor function $\mathcal{E}$ such that for any two given transcripts $(t,c,x,s)$ and $(t,\hat{c},x,\hat{s})$ where $c \neq \hat{c}$ and $\sigma_{ver}^\lambda(t,c,x,s) = \sigma_{ver}^\lambda(t,\hat{c},x,\hat{s}) = 1$:
\[Pr\Big[(x,w) \in \mathcal{R} \;\Big|\; w = \mathcal{E}(t,x,c,s,\hat{c},\hat{s})\Big] \geq 1 - \mathsf{negl}(\lambda).\]More precisely, it means that for any two random, distinct challenges, the knowledge of the responses for the same commitment allows the verifier to recover the witness by a polynomial-time algorithm.
It is also said that a $\Sigma$-protocol is $k$-special sound if the above property achieved using $k$ different challenges.
Special Honest-Verifier Zero-Knowledge
A $\Sigma$-protocol is said to be special honest-verifier zero-knowledge if there exists a special polynomial-time simulator function $\mathcal{S}$ that enables the generation of an accepting transcript by the verifier using selected uniformly and independently a challenge $c \leftarrow \mathbb{F}$ and a response $s \leftarrow \mathbb{F}$:
\[Pr\Big[\sigma_{ver}^\lambda(t,c,x,s) = 1\;\Big|\; t = \mathcal{S}(x,c,s) \Big] \geq 1 - \mathsf{negl}(\lambda).\]Transcripts ${(t, c, s)}$ generated by this process are assumed to be indistinguishable from real transcripts that appear during the protocol walkthrough between the honest prover and the honest verifier.